Publications and Scientific Work by Clemens Grabmayer

Publications and Technical Reports

2018

  1. C. Grabmayer: Modeling Terms by Graphs with Structure Constraints (Two Illustrations), extended abstract for an invited talk at TERMGRAPH 2018, July 8, 2018 (pdf).

2016

  1. C. Grabmayer: Linear Depth Increase of Lambda Terms in Leftmost-Outermost Beta-Reduction Rewrite Sequences,

2015

  1. J. Endrullis, C. Grabmayer, D. Hendriks: Regularity Preserving but not Reflecting Encodings,
  2. C. Grabmayer, and V. van Oostrom: Nested Term Graphs (Work In Progress), post-proceedings of the workshop TERMGRAPH 2014, Electronic Proceedings in Theoretical Computer Science (EPTCS) (EPTCS proceedings page (doi:10.4204/EPTCS.183), pdf via EPTCS, pdf (local copy)).

2014

  1. C. Grabmayer, and J. Rochel: Maximal Sharing in the Lambda Calculus with letrec, Proceedings of ICFP 2014, 1-3 September 2014, Gothenburg, Sweden (paper's page in ACM digital library, paper via ACM digital library, pdf (local copy).
  2. C. Grabmayer, and V. van Oostrom: Nested Term Graphs, in:
  3. C. Grabmayer, and D. Hendriks: Co-Reflexivity = Symmetry + Anti-Symmetry, note, 22 March 2014.
  4. C. Grabmayer, and J. Rochel: Maximal Sharing in the Lambda Calculus with letrec, submitted on arxiv.org, January 7, 2014 (report's page arXiv:1401.1460, pdf report via arxiv).

2013

  1. C. Grabmayer, and J. Rochel: Term Graph Representations for Cyclic Lambda-Terms, report extending (proofs of main results added) the article in the proceedings of TERMGRAPH 2013, submitted on arxiv.org, August 5, 2013 (report's page arXiv:1308.1034, pdf report via arxiv).
  2. C. Grabmayer, and J. Rochel Confluent Let-Floating, Proceedings of IWC 2013, the 2nd International Workshop on Confluence, June 28, 2013, Eindhoven, NL (pdf, slides talk at the workshop).
  3. J. Rochel, and C. Grabmayer Confluent Unfolding in the Lambda Calculus with Letrec, Proceedings of IWC 2013, the 2nd International Workshop on Confluence, June 28, 2013, Eindhoven, NL (pdf, slides talk at the conference).
  4. C. Grabmayer, and J. Rochel: Expressibility in the Lambda Calculus with Letrec, Proceedings of RTA 2013 (proceedings available at LIPCIS, Vol. 21). Links article: (article in LIPICS proceedings, extending report (page on arxiv.org), extending report on arxiv.org (pdf), slides talk at the conference).
  5. C. Grabmayer, and J. Rochel: Term Graph Representations for Cyclic Lambda-Terms, in R. Echahed and D. Plump (editors): Proceedings of the 7th International Workshop on Computing with Terms and Graphs, TERMGRAPH 2013, Rome, Italy, 23rd March 2013, EPTCS 110, (proceedings page on arxiv.org, article's page on arxiv.org, article (pdf) via arxiv.org, pdf (local copy)). (These versions are now superseded by the extended report on arxiv: arXiv:1308.1034.) Talk (pdf) by Jan Rochel at the workshop.
  6. J. Endrullis, C. Grabmayer, D. Hendriks: Mix-Automatic Sequences, Paper at LATA 2013, Proceedings of LATA 2013, April 2-5, Bilbao, Spain, LNCS 7810, (proceedings page at Springer Link, (local copy article (pdf)).

2012

  1. C. Grabmayer, and J. Rochel: Expressibility in the Lambda Calculus with Letrec. Submitted on arXiv computer science, 14 Aug 2012 (paper's page arXiv:1208.2383, article (pdf) via arxiv.org).
  2. C. Grabmayer, J. Endrullis, D. Hendriks, J.W. Klop, L.S. Moss: Automatic Sequences and Zip-Specifications, versions:

2011

  1. J. Endrullis, C. Grabmayer, J.W. Klop, V. van Oostrom: On Equal μ-Terms, in: Festschrift In Honour of Jan Bergstra, (special issue of) Theoretical Computer Science, volume 412, number 28, pages 3175-3202 (doi:10.1016/j.tcs.2011.04.011, pdf [local copy]).
  2. C. Grabmayer, J. Leo, V. van Oostrom, A. Visser: On the Termination of Russell's Description Elimination Algorithms, The Review of Symbolic Logic, Volume 4, Number 3, September 2011, pages 367-393, doi:10.1017/S1755020310000286, © Cambridge University Press, (pdf [local copy]).
  3. M. Bezem, C. Grabmayer, and M. Wałicki: Expressive power of digraph solvability, Annals of Pure and Applied Logic, in Press (doi:10.1016/j.apal.2011.08.004, pdf [local copy]).
  4. J. Rochel, C. Grabmayer: Avoiding Repetitive Evaluation Patterns in Lambda Calculus with Letrec (Work in Progress), presented at the workshop TERMGRAPH 2011, 2 April 2011, Saarbrücken, Electronic Proceedings in Theoretical Computer Science (EPTCS 48, doi:10.4204/EPTCS.48), (arXiv-ed at: http://dx.doi.org/10.4204/EPTCS.48.9, pdf [local copy]) .

2010

  1. M. Wałicki, C. Grabmayer, M. Bezem: Expressive Power of Digraph Solvability, Logic Group Preprint 286, Universiteit Utrecht, Oktober 2010 (pdf, Logic Group Preprint Series).
  2. C. Grabmayer, J. Leo, V. van Oostrom, A. Visser: On the termination of Russell's description elimination algorithm, to appear in The Review of Symbolic Logic. (pdf).
  3. J. Endrullis, C. Grabmayer, D. Hendriks, J.W. Klop, V. van Oostrom: Unique Normal Forms in Infinitary Weakly Orthogonal Term Rewriting, proceedings of RTA-2010 (pdf), link to RTA-2010 Proceedings at LIPIcs.

2009

  1. C. Grabmayer, J. Leo, V. van Oostrom, A. Visser: On the termination of Russell's description elimination algorithm, Logic Group Preprint 280, Universiteit Utrecht, November 2009 (pdf, Logic Group Preprint Series).
  2. Joerg Endrullis, Clemens Grabmayer, Dimitri Hendriks, and Jan Willem Klop: Unique Normal Forms in Infinitary Weakly Orthogonal Term Rewriting, Liber Amicorum for Roel de Vrijer on the occasion of his 60th birthday (arXiv:0911.1009).
  3. C. Grabmayer: From Abstract Rewriting Systems to Abstract Proof Systems, Liber Amicorum for Roel de Vrijer on the occasion of his 60th birthday (pdf, arXiv:0911.1412).
  4. J. Endrullis, C. Grabmayer, D. Hendriks, A. Isihara, and J.W. Klop: Productivity of Stream Definitions, Special issue of TCS devoted to selected papers from FCT'07 (link at ScienceDirect, pdf article in press (local copy), pdf submitted).
  5. J. Endrullis, C. Grabmayer, D. Hendriks: Complexity of Fractran and Productivity, proceedings of CADE-22 (pdf, talk at CADE-22 (pdf)).
  6. J. Endrullis, C. Grabmayer, D. Hendriks: Complexity of Fractran and Productivity, technical report (pdf, arXiv:0903.4366).
  7. J. Endrullis, C. Grabmayer, D. Hendriks, J.W. Klop, and R. de Vrijer: Proving Infinitary Normalization, TYPES'08 Post-Proceedings, to appear (pdf).
  8. J. Endrullis, C. Grabmayer, D. Hendriks, and J.W. Klop: Infinite Streams, NVTI-Nieuwsbrief, Maart 2009 (pdf).

2008

  1. J. Endrullis, C. Grabmayer, D. Hendriks, A. Isihara, and J.W. Klop: Productivity of Stream Definitions, Logic Group Preprint 268, Universiteit Utrecht, November 2008 (pdf, Logic Group Preprint Series).
  2. J. Endrullis, C. Grabmayer, D. Hendriks: Data-Oblivious Stream Productivity, Proceedings of LPAR 2008, LNCS 5330, pages 79-96, Springer Verlag 2008 (pdf (local copy), paper's page at SpringerLink.com, talk at LPAR 2008 (pdf)).
  3. J. Endrullis, C. Grabmayer, D. Hendriks: Data-Oblivious Stream Productivity, technical report (pdf, arXiv:0806.2680).

2007

  1. C. Grabmayer: Productiviteit van Streamspecificaties (doc), Faculteitsblad De Filosoof, Nummer 36, Afdeling Wijsbegeerte, Universiteit Utrecht, September 2007.
  2. J. Endrullis, C. Grabmayer, D. Hendriks, A. Isihara, J.W. Klop: Productivity of Stream Definitions, to appear in: Proceedings of FCT 2007, LNCS 4639, pages 274-287, Springer Verlag, 2007 (paper's page at Springerlink, pdf (via Springerlink), pdf (local copy), BibTeX-entry).
  3. C. Grabmayer: A Duality Between Proof Systems for Cyclic Term Graphs, (paper's page, link to pdf-file at the Cambridge Journal portal; local copy of pdf-file, BibTeX-entry), Mathematical Structures in Computer Science, volume 17, issue 3, pages 439-484, 2007.
  4. J.C.M. Baeten, F. Corradini, and C. Grabmayer: A Characterization of Regular Expressions under Bisimulation, (paper's page, link to pdf-file at ACM's portal, local copy of pdf-file BibTeX-entry), Journal of the ACM, volume 54, issue 2, pages 2-28, April 2007.

2006

  1. C. Grabmayer, J.W. Klop, and B. Luttik: Some Remarks on Definability of Process Graphs (pdf, BibTeX-entry). In Christel Baier, Holger Hermanns [eds.]: Proceedings of CONCUR 2006, LNCS 4137, pages 16-36, Springer Verlag, 2006.

2005

  1. J.C.M. Baeten, F. Corradini, and C. Grabmayer: A Characterisation of Regular Expressions under Bisimulation (pdf). Research Report, Technical University of Eindhoven. October 2005.
  2. C. Grabmayer, J.W. Klop, and B. Luttik: Reflections on a Geometry of Processes (pdf). In Luca Aceto and Andrew Gordon (editors), Short Contributions from the Workshop "Algebraic Process Calculi: The First Twenty Five Years and Beyond" (PA'05), BRICS Notes Series NS-05-3 (link to pdf-file), pages 118-123, 2005. Also in: L. Aceto and A.D. Gordon (editors), Proceedings of the Workshop "Essays on Algebraic Process Calculi" (APC 25), Bertinoro, Italy, 01-05 August 2005, ENTCS, Volume 162, Pages 183-190 (29 September 2006) (link to pdf-file at Elsevier's Science Direct, local copy of pdf-file).
  3. C. Grabmayer: Using Proofs by Coinduction to Find ``Traditional'' Proofs (pdf, BibTeX-entry). In José Luiz Fiadeiro (ed.): Proceedings of CALCO 2005, LNCS 3629, 2005. Here also an extended version (pdf) including a technical appendix with proofs is available.

2004

  1. C. Grabmayer: Derivability and Admissibility of Inference Rules in Abstract Hilbert Systems (pdf). Collegium Logicum, Vol. VIII, Kurt Gödel Society, Vienna, 2004.

2003

  1. C. Grabmayer: Derivability and Admissibility of Inference Rules in Abstract Hilbert Systems (pdf, ps). Technical Report, Faculteit der Exacte Wetenschapen, Divisie Wiskunde & Informatica, August 2003. There are also two pages of Extended Abstract (pdf) for this report available.

2002

  1. C. Grabmayer: A Duality in Proof Systems for Recursive Type Equality and for Bisimulation Equivalence on Cyclic Term Graphs (pdf local copy, pdf at Elsevier's Science Direct). Proceedings of the Workshop TERMGRAPH 2002, Barcelona, October 7, 2002, Electronic Notes in Computer Science, Vol. 72, No.1.
  2. C. Grabmayer: A Duality in Proof Systems for Recursive Type Equality and for Bisimulation Equivalence on Cyclic Term Graphs ( ps.gz, pdf). Technical Report, Vrije Universiteit Amsterdam Report, Faculteit der Exacte Wetenschapen, Divisie Wiskunde & Informatica, Rapportnr IR-499, juli 2002.

[ Back to my homepage]

List of BibTeX Entries

Here you find a preliminary list of BibTeX-Entries of my publications.

[ Back to my homepage]

Poster Presentations

  1. C. Grabmayer: Derivability and Admissibility of Inference Rules in Abstract Hilbert Systems Poster Presentation at CSL03/8th KGC, Vienna, 25-30 august 2003.

  2. C. Kupke, D. Hendriks, C. Grabmayer: Infinity: Modelling, Computing, and Reasoning with Infinite Objects (pdf) Siren Meeting, NWO BRICKS, 30 october 2007.

[ Back to my homepage]

PhD Thesis

C. Grabmayer: Relating Proof Systems for Recursive Types (pdf). PhD thesis, Vrije Universiteit Amsterdam, 2005. An abstract is available at Clemens Grabmayer's Thesis Page that is part of the PhD thesis' pages maintained by the computer science department of the VU Amsterdam.

[ Back to my homepage]

Master's Theses

  1. C. Grabmayer: "Die Entscheidungskomplexität logischer Theoreme - eine Studie anhand der Presburger Arithmetik" ("Decision Complexity of Logical Theories - a study at the example of Presburger Arithmetic"), ``Diplomarbeit'' at the Johannes Kepler Universität Linz, Austria, August 1997. This diploma-thesis [ps.gz, 1016K] is available here.

  2. C. Grabmayer: "Cut-Elimination in the Implicative Fragment of a G3mi-Gentzen-system and its Computational Content", master's-thesis at the ILLC (Institute for Logic, Language and Computation) of the Universiteit van Amsterdam, September 1999. This master's thesis [ps.gz, 240K] is available via this link. There is also an abstract in ps.gz form [38K] and (basically the same) abstract in ascii-text format available for this thesis.

[ Back to my homepage]

Talks and Miscellaneous Work

  1. Slides (pdf) for the talk Maximal Sharing in the Lambda Calculus with Letrec in the VU Theoretical Computer Science seminar, Vrije Universiteit, Amsterdam October 6, 2018.

  2. Slides (pdf) for the talk Regularity Preserving but not Reflecting Encodings at the conference LICS 2015, Kyoto, Japan, July 9, 2015.

  3. Slides (pdf) and video (link youtube) for the talk Maximal Sharing in the Lambda Calculus with Letrec at the conference ICFP 2014, Gothenburg, Sweden, September 1, 2014.

  4. Slides (pdf) for the talk Nested Term Graphs (work in progress) at the workshop TERMGRAPH 2014, Vienna Summer of Logic, TU Wien, Austria, July 13, 2014.

  5. Slides (pdf) for the talk hogere orde en erste orde (ter ere van het afscheid van Vincent van Oostrom van de Universiteit Utrecht), afscheidsbijeenkomst georganiseerd door de studenten CKI/CAI en de disciplinegroep Theoretische Filosofie, Sweelinckzaal, Drift 21, Universiteit Utrecht, 2 juli 2014.

  6. Slides (pdf) for the talk Confluent Let-Floating at the International Workshop on Confluence (IWC 2013) (28 June 2013), Technical University Eindhoven, June 28, 2013.

  7. Slides (pdf) for the talk Expressibility in the Lambda-Calculus with Mu at RTA 2013 (24-26 June), Technical University Eindhoven, Netherlands, June 25, 2012.

  8. Slides (pdf) for the talk Automatic Sequences and Zip-Specifications at LICS 2012 (25-28 June), Dubrovnik, Croatia, June 26, 2012.

  9. Slides (pdf) for the talk Zip-Specifications and Automatic Sequences at the COiN Meeting, Radboud Universiteit, Nijmegen June 4, 2012.

  10. Slides (pdf) for the talk Expressibility in the λ-calculus with Letrec presented by Jan Rochel at TeReSe Meeting, RWTH, Aachen, March 28, 2012.

  11. Slides (pdf) for the talk Avoiding Repetitive Reduction Behaviours in Lambda Calculus with Letrec (together with Jan Rochel) at TERMGRAPH 2011, Saarbrücken, Germany, April 2, 2011.

  12. Slides (pdf) for the talk On Equal μ-Terms (together with Vincent van Oostrom and Joerg Endrullis, about joint work with also Jan Willem Klop) at the TeReSe Meeting, Vrije Universiteit, Amsterdam, November 18, 2010.

  13. Slides (pdf) for the talk Unique Normal Forms in Infinitary Weakly Orthogonal Term Rewriting at RTA 2010, Edinburgh, UK, July 13, 2010.

  14. Slides used in the course on productivity given together with Dimitri Hendriks and Jörg Endrullis in the framework of the 5th International School on Rewriting, 3 – 8 July 2010, Drift 21, Utrecht, The Netherlands:
  15. Slides (pdf) for the talk Unique Normal Forms in Infinitary Weakly Orthogonal Term Rewriting at the TeReSe Meeting, RWTH, Aachen, Germany, May 28, 2010.

  16. Slides (pdf) for the talk Equivalence of Stream Specifications at the Workshop on Proof Theory and Rewriting, Universitätszentrum Obergurgl, March 28--31, 2010, March 28, 2010.

  17. Slides (pdf) for the talk Proving Productivity (Part 2) at the Symposium The End of Infinity, VU Amsterdam, Dec 15, 2009.

  18. Slides (pdf) for the talk Graph Kernels, Logic, and Choice Axioms at the Symposium Tbilissi 2009, Bakuriani, Georgia, September 21, 2009.

  19. Slides (pdf) for the talk Complexity of Fractran and Productivity at CADE 2009, McGill University, Montreal, Canada, Aug 6, 2009.

  20. Slides (pdf) for the talk Data-Oblivious Stream Productivity at LPAR 2008, Carnegie Mellon Qatar Campus, Doha, Qatar, Nov 23, 2008.

  21. Slides (pdf) for a talk Data-Oblivious Stream Productivity at PAM (Process Algebra Meeting), CWI, Amsterdam, May 7, 2008.

  22. Slides (pdf) for a talk Watching Streams Grow: The Pebbleflow Method at the TF-Lunch Meeting of our department, Universiteit Utrecht, November 6, 2007.

  23. Slides (pdf) for a talk Productivity of Stream Definitions at the TeReSe Meeting, TU/e, Eindhoven, NL, May 24, 2007.

  24. Slides (pdf) for a talk Regular Expressions Under the Process Interpretation at the Workshop on Proof Theory and Rewriting 2006 , Obergurgl, Austria, September 5--9, 2006.

  25. Slides (pdf) and Extended Abstract (pdf) for a talk On the Star Height of Regular Expressions under Bisimulation at the Express'06 Workshop, Bonn, 26th of August, 2006.

  26. Slides (pdf) for the talk A Coinductive Axiomatisation of Regular Expressions under Bisimulation, 27th of March, 2006, Short Contribution to CMCS 2006, March 25-27, Vienna Institute of Technology, Austria. Also available here is the Extended Abstract (pdf) for this short contribution.

  27. Slides (pdf) for a talk about the paper Using Proofs by Coinduction to Find `Traditional' Proofs given at CALCO 2005, on 5th of September, 2005, University of Wales Swansea, UK.

  28. Slides (pdf) for the talk at my PhD-defense about my thesis Relating Proof Systems for Recursive Types given at the aula of the Vrije Universiteit Amsterdam on 22nd of March, 2005, 13.45 -- 13.55.

  29. Slides (pdf) for the talk Derivability and Admissibility of Inference Rules in Abstract Hilbert Systems given in the seminar Zuidelijk Interuniversitair Colloquium (ZIC) at the TU Eindhoven on 22nd of June, 2004.

  30. Slides [ps.gz, 449K] for a talk about A Duality in Proof Systems for Recursive Type Equality and for Bisimulation Equivalence on Cyclic Term Graphs at 7th of October, 2002, at the TERMGRAPH 2002 Workshop, Barcelona.

  31. A talk on ``Proving Equality for Recursive Types - A Duality Between `Syntactic-Matching' Tableaux and Brandt-Henglein derivations'', held on the 8th of May, 2002, at the PAM (Process Algebra Meeting), CWI, Amsterdam. The slides for this talk are available here in the form of a [ps.gz, 210K].

  32. Some Remarks about an Exercise by Detlef Plump, April 2002, see this [ps.gz, 45K], [pdf, 4.1M].

  33. A talk on A Duality between Derivations and Consistency-Unfoldings in two different known Proof-System for Recursive Type Equality held at the OzsL-Accolade on October 21st, 2001 at Hotel Dennehoeve, Nunspeet. The LATEX-ed slides for this talk are available here in the form of a [ps.gz, 124K].

  34. A talk on A Duality between Derivations and Consistency-Unfoldings in two different known Proof-System for Recursive Type Equality in the seminar of our Theoretical Computer Science group on September 14th and 21st, 2001. The LATEX-ed slides for this talk are available here in the form of a [ps.gz, 144K].

  35. An extended talk on Proof-Theoretic Interconnections between Know Axiom- and Inference-Systems for the Equality and Subtype Relations on Recursive Types given in the Lambda-Seminar of the Computer Science Department at the KUN (Katholieke Universiteit Nijmegen) at January 12th, 2001, 10:30-12:15. Confer here for a short abstract [link to a local html-file] of this talk. Colour slides [as ps.gz, 172K], that (to be precise: at about half of which:) I did present there as well as a handout [ ps.gz, 102K] for this talk are available here. (NOTE: A couple of further handwritten and -drawn slides are naturally not included in the .ps.gz -file here, but the locations of most of the handwritten slides are indicated as notes included in this file.)

  36. A talk on Proof-Theoretic Interconnections between Known Axiom- and Inference-Systems for Recursive Type Equality given at the OzsL-Accolade, Nunspeet, 27th October 2000. Confer here for a short abstract [link to a local html-file] of this talk. Furthermore also the slides [as ps.gz, 106K, or as plain ps, 272K] presented in Nunspeet (indeed a few ones more than I was able to present there, since time was short then also for me) and a handout-version (of the slides) [ps.gz, 106K] prepared for the Accolade (but which I unfortunately have forgotten to advertise properly) are available here.

[ Back to my homepage]

Clemens Grabmayer / VU University Amsterdam / c dot a dot grabmayer at vu one dot nl / Last modified: Tue Jul 11 12:24:07 CET 2018