Publications and Scientific Work by Clemens Grabmayer (and co-authors)

Overview

• Publications and Technical Reports
• Posters
• Ph.D. Thesis
• Master's Theses
• Talks
• (picture taken on the top of Pizzo Cefalone)
• References to software tools developed by Jan Rochel for joint work in the NWO-project ROS

---

Publications and Technical Reports

2024

1. Clemens Grabmayer: Closing the Image of the Process Interpretation of 1-Free Regular Expressions under Bisimulation Collapse, Extended Abstract for the Workshop TERMGRAPH 2024, Satellite event of ETAPS 2024, 7 April 2024, Luxembourg City, Luxembourg (pdf).
2. Clemens Grabmayer: From Compactifying Lambda-Letrec Terms to Recognizing Regular-Expression Processes (Extended Abstract and Literature), submitted to the Proceedings of the Workshop DCM 2023 (Developments in Computational Models), Sapienza Università, Rome, July 2, 2023 (pdf).

2023

1. Clemens Grabmayer: A Coinductive Reformulation of Milner's Proof System for Regular Expressions Modulo Bisimilarity:
   • Logical Methods in Computer Science, Volume 19, Issue 2, June, 2023 (paper's page at LMCS, pdf at LMCS, pdf local copy).
   • the same version on arxiv.org (arXiv:2203.09501v5, pdf at arXiv pdf local copy).
2. Clemens Grabmayer (editor): Proceedings of the Twelfth International Workshop on Computing with Terms and Graphs, Electronic Proceedings in Theoretical Computer Science 377, March 2023 (EPTCS 377, arXiv:2303.14219).
3. Clemens Grabmayer: The Image of the Process Interpretation of Regular Expressions is Not Closed under Bisimulation Collapse, Report (14 pages, 9 pages appendix) arxiv.org report (arXiv:2303.08553, pdf) concerning the crucial observation underlying the crystallization process described in arXiv:2209.12188.

2022

1. Clemens Grabmayer: Milner's Proof System for Regular Expressions Modulo Bisimilarity is Complete (Crystallization: Near-Collapsing Process Interpretations of Regular Expressions), LICS 2022, Technion, Haifa, Israel, August 2—5, 2022 (article after rebuttal [pdf], report version [arXiv:2209.12188, pdf], presentation slides [pdf, Easychair smart slides], poster ).
2. Clemens Grabmayer: A Coinductive Reformulation of Milner's Proof System for Regular Expressions Modulo Bisimilarity, substantial extension (50 pages) of the CALCO 2021 article as an arxiv.org report (arXiv:2203.09501, pdf).

2021

1. Clemens Grabmayer: Bisimulation Slices and Transfer Functions, Technical report, Reykjavik University, Abstract for the 32nd Nordic Workshop on Programming Theory (NWPT 2021) (pdf, pdf (local copy), presentation slides [pdf, Easychair smart slides]).
2. Clemens Grabmayer: A Coinductive Version of Milner’s Proof System for Regular Expressions Modulo Bisimilarity,
   • proceedings of CALCO 2021, Salzburg, Austria, August 31—September 3, 2021, (article's page on DROPS, pdf on DROPS, presentation slides [pdf, Easychair smart slides]),
   • extended report of CALCO 2021 article on arxiv.org (arXiv:2108.13104, pdf).
3. Clemens Grabmayer: Structure-Constrained Process Graphs for the Process Semantics of Regular Expressions, (Post-)Proceedings of the 11th International Workshop of Computing with Terms and Graphs, Online 5th July 2020, Electronic Proceedings in Theoretical Computer Science, volume 334, Open Publishing Association, pages 29—45, 2021 (paper's page, pdf).

2020

1. Clemens Grabmayer: Structure-Constrained Process Graphs for the Process Semantics of Regular Expressions:
   • extended-report version (arXiv:2012.10869, pdf), published on arxiv.org, December 2020, of the article in the EPTCS post-proceedings of the workshop TERMGRAPH 2020.
   • final version for the workshop (direct link, local copy) published on the website of TERMGRAPH 2020, June 2020.
2. Clemens Grabmayer and Wan Fokkink: A Complete Proof System for 1-Free Regular Expressions Modulo Bisimilarity,
   • proceedings of LICS 2020 (article (local copy), presentation slides, video on youtube).
   • extended report of LICS 2020 article on arxiv.org (arXiv:2004.12740, pdf).

2019

1. Clemens Grabmayer: Linear Depth Increase of Lambda Terms in Leftmost-Outermost Beta-Reduction Rewrite Sequences, substantial extension of the 2016 article (Liber Alberti, and arXiv:1604.07030v1 (version v1)), report on arxiv.org (report's page arXiv:1604.07030v2 (version v2), pdf report via arxiv).

2018

1. Clemens Grabmayer: Modeling Terms by Graphs with Structure Constraints (Two Illustrations), Invited Talk (pdf) at TERMGRAPH 2018, Oxford, UK, July 7, 2018.
   • Extended abstract (pdf) for the invited talf.
   • Article for the (Post-)Proceedings in EPTCS, volume 288, pages 1—13, 2019 (arXiv:1902.02010, EPTCS 288, pdf via arXiv).

2016

1. Clemens Grabmayer: Linear Depth Increase of Lambda Terms in Leftmost-Outermost Beta-Reduction Rewrite Sequences,
   • Liber Amicorum Alberti (A Tribute to Albert Visser), pages 46—60, Jan van Eijck and Rosalie Iemhoff and Joost J. Joosten (eds.), College Publications ( book's page at College Publications, pdf article), Tributes series, April 2016,
   • report on arxiv.org (report's page arXiv:1604.07030, pdf report via arxiv).

2015

1. Jörg Endrullis, Clemens Grabmayer, Dimitri Hendriks: Regularity Preserving but not Reflecting Encodings,
   • report on arxiv.org, (report's page arXiv:1501.04835, pdf report via arxiv).
   • Proceedings of LICS 2015, Kyoto, 7—10 July 2015 (pdf (local copy)).
2. Clemens Grabmayer and Vincent 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. Clemens Grabmayer and Jan 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), presentation slides [pdf, Easychair smart slides]).
2. Clemens Grabmayer and Vincent van Oostrom: Nested Term Graphs, in:
   • proceedings of TERMGRAPH 2014, July 13, 2014, Vienna Summer of Logic, Vienna Institute of Technology (TU-Wien), Austria (pdf, slides talk at the workshop).
   • report on arxiv.org, May 25, 2014 (report's page arXiv:1401.1460, pdf report via arxiv).
3. Clemens Grabmayer and Dimitri Hendriks: Co-Reflexivity = Symmetry + Anti-Symmetry, note, March 22, 2014.
4. Clemens Grabmayer and Jan 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. Clemens Grabmayer and Jan 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. Clemens Grabmayer and Jan 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. Jan Rochel and Clemens 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. Clemens Grabmayer and Jan Rochel: Expressibility in the Lambda Calculus with Mu, 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. Clemens Grabmayer and Jan 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 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örg Endrullis, Clemens Grabmayer, Dimitri 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. Clemens Grabmayer and Jan Rochel: Expressibility in the Lambda Calculus with Letrec. Submitted on arXiv computer science, August 14, 2012 (paper's page arXiv:1208.2383, article (pdf) via arxiv.org).
2. Clemens Grabmayer, Jörg Endrullis, Dimitri Hendriks, Jan Willem Klop, L.S. Moss: Automatic Sequences and Zip-Specifications, versions:
   • Paper at LICS 2012, Proceedings of LICS 2012, pages 335—344 (pdf (local copy))
   • Submitted on arXiv computer science, 16 Jan 2012 (paper's page arXiv:1201.3251).
   • Logic Preprint 294, Logic Preprint Series, Theoretical Philosophy group, Department of Philosophy, Utrecht University, April 2012 (pdf at UU, reports page UU).

2011

1. Jörg Endrullis, Clemens Grabmayer, Jan Willem Klop, Vincent 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. Clemens Grabmayer, Joop Leo, Vincent van Oostrom, Albert 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. Marc Bezem, Clemens Grabmayer, and Michal 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. Jan Rochel and Clemens 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. Michal Wałicki, Clemens Grabmayer, Marc Bezem: Expressive Power of Digraph Solvability, Logic Group Preprint 286, Universiteit Utrecht, Oktober 2010 (pdf at UU, reports page at UU).
2. Clemens Grabmayer, Joop Leo, Vincent van Oostrom, Albert Visser: On the termination of Russell's description elimination algorithm, to appear in The Review of Symbolic Logic. (pdf).
3. Jörg Endrullis, Clemens Grabmayer, Dimitri Hendriks, Jan Willem Klop, Vincent 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. Clemens Grabmayer, Joop Leo, Vincent van Oostrom, Albert Visser: On the termination of Russell's description elimination algorithm, Logic Group Preprint 280, Universiteit Utrecht, November 2009 (pdf at UU, reports page UU).
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. Clemens 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örg Endrullis, Clemens Grabmayer, Dimitri Hendriks, Ariya Isihara, and Jan Willem 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örg Endrullis, Clemens Grabmayer, Dimitri Hendriks: Complexity of Fractran and Productivity, proceedings of CADE-22 (pdf, talk at CADE-22 (pdf)).
6. Jörg Endrullis, Clemens Grabmayer, Dimitri Hendriks: Complexity of Fractran and Productivity, technical report (pdf, arXiv:0903.4366).
7. Jörg Endrullis, Clemens Grabmayer, Dimitri Hendriks, Jan Willem Klop, and R. de Vrijer: Proving Infinitary Normalization, TYPES'08 Post-Proceedings, to appear (pdf).
8. Jörg Endrullis, Clemens Grabmayer, Dimitri Hendriks, and Jan Willem Klop: Infinite Streams, NVTI-Nieuwsbrief, Maart 2009 (pdf).

2008

1. Jörg Endrullis, Clemens Grabmayer, Dimitri Hendriks, Ariya Isihara, and Jan Willem Klop: Productivity of Stream Definitions, Logic Group Preprint 268, Universiteit Utrecht, November 2008 (pdf at UU, report's page at UU).
2. Jörg Endrullis, Clemens Grabmayer, Dimitri 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örg Endrullis, Clemens Grabmayer, Dimitri Hendriks: Data-Oblivious Stream Productivity, technical report (pdf, arXiv:0806.2680).

2007

1. Clemens Grabmayer: Productiviteit van Streamspecificaties (doc), Faculteitsblad De Filosoof, Nummer 36, Afdeling Wijsbegeerte, Universiteit Utrecht, September 2007.
2. Jörg Endrullis, Clemens Grabmayer, Dimitri Hendriks, Ariya Isihara, Jan Willem 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. Clemens 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, Flavio Corradini, and Clemens 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. Clemens Grabmayer: A Coinductive Axiomatisation of Regular Expressions under Bisimulation (pdf, and pdf early easier version), extended abstract for the Short Contributions to CMCS 2006 (March 25—27, 2006, Vienna Institute of Technology, Austria), University of Nottingham technical report, 2006.
2. Clemens Grabmayer, Jan Willem Klop, and Bas 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, Flavio Corradini, and Clemens Grabmayer: A Characterisation of Regular Expressions under Bisimulation (pdf, pdf via TUE-archive, pdf local copy report). Research Report, Technical University of Eindhoven. October 2005.
2. Clemens Grabmayer, Jan Willem Klop, and Bas 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, 1—5 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. Clemens 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. Clemens Grabmayer: Derivability and Admissibility of Inference Rules in Abstract Hilbert Systems (pdf). Collegium Logicum, Vol. VIII, Kurt Gödel Society, Vienna, 2004.

2003

1. Clemens 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. Clemens 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. Clemens Grabmayer: A Duality in Proof Systems for Recursive Type Equality and for Bisimulation Equivalence on Cyclic Term Graphs (pdf, ps). Technical Report, Vrije Universiteit Amsterdam Report, Faculteit der Exacte Wetenschapen, Divisie Wiskunde & Informatica, Rapportnr IR-499, juli 2002.

---

---

Poster Presentations

1. Clemens Grabmayer: Milner's Proof System for Regular Expressions Modulo Bisimilarity is Complete (Crystallization: Near-Collapsing Process Graph Interpretations of Regular Expressions) (pdf), Poster Presentation at LICS 2022, Technion, Haifa, Israel, August 5, 2022.
   
   
2. Clemens Kupke, Dimitri Hendriks, Clemens Grabmayer: Infinity: Modelling, Computing, and Reasoning with Infinite Objects (pdf), Siren Meeting, NWO BRICKS, October 30, 2007.
   
   
3. Clemens Grabmayer: Derivability and Admissibility of Inference Rules in Abstract Hilbert Systems, Poster Presentation at CSL03/8th KGC, Vienna, August 25—30, 2003.

---

---

PhD Thesis

Clemens Grabmayer: Relating Proof Systems for Recursive Types (pdf (locally), thesis page/pdf (on VU-Amsterdam Research Portal)). PhD thesis, Vrije Universiteit Amsterdam, 2005.

---

---

Master's Theses

1. Clemens Grabmayer: "Die Entscheidungskomplexität logischer Theoreme - eine Studie anhand der Presburger Arithmetik" (pdf) (title translation in English: "Decision Complexity of Logical Theories - a study at the example of Presburger Arithmetic"), ``Diplomarbeit'' at the Institute of Mathematics of the Johannes Kepler Universität, Linz, Austria, August 1997.
   
   
2. Clemens Grabmayer: "Cut-Elimination in the Implicative Fragment of a G3mi-Gentzen-system and its Computational Content" (pdf), master's-thesis at the ILLC (Institute for Logic, Language and Computation) of the Universiteit van Amsterdam, September 1999.

---

---

Talks and Miscellaneous Work

1. Slides (pdf) for the talk Closing the Image of the Process Interpretation of 1-Free Regular Expressions under Bisimulation Collapse at the ETAPS 2024 satellite workshop TERMGRAPH 2024, Luxembourg, April 7, 2024.
   
   
2. Slides (pdf, pdf (fewer overlays)) and abstract (txt) for the invited talk: From Compactifying Lambda-Letrec Terms to Recognizing Regular-Expression Processes at the DCM-2023 Workshop, (affiliated with the conference FSCD 2023) July 2, 2023.
   
   
3. Slides (pdf, ubz) for the talk Forms of Sharing, and Expressibility of Process Graphs by Regular Expressions at the Formal Methods Reading Group, CS@GSSI, December 14, 2022.
   
   
4. Slides (pdf, Easychair smart slides) for the talk Milner's Proof System for Regular Expressions Modulo Bisimilarity is Complete at the conference LICS 2022, Technion, Haifa, Israel, August 4, 2022.
   
   
5. Slides (pdf) and abstract (txt) for the talk Milner's Proof System for Regular Expressions Modulo Bisimilarity is Complete at the CS@GSSI Seminar, July 27, 2022.
   
   
6. Slides (pdf, Easychair smart slides) for the talk Bisimulation Slices and Transfer Functions at the 32nd Nordic Workshop on Programming Theory NWPT 2021, Rejkjavik University, Iceland, and online, November 6, 2021.
   
   
7. Slides (pdf, Easychair smart slides) for the talk A Coinductive Version of Milner's Proof System for Regular Expressions Modulo Bisimilarity at the conference CALCO 2021, September 2, 2021.
   
   
8. Slides (pdf) for the talk Structure-Constrained Process Graphs for the Process Semantics of Regular Expressions at the workshop TERMGRAPH 2020, July 5, 2020.
   
   
9. Slides (pdf) for the talk A Complete Proof System for 1-Free Regular Expressions Modulo Bisimilarity at the conference LICS 2020, Saarbrücken and online, July 8—11, 2020.
   
   
10. Slides (pdf) for the invited talk: Modeling Terms in the Lambda-Calculus with Letrec (by Term Graphs and Finite-State Automata) at the workshop Computational Logic and Applications (CLA 2019), Université de Versailles, France, July 2, 2019.
    
    
11. Slides (pdf) of the talk: The Process Semantics of Regular Expressions at the Postdoc Seminar of the Gran Sasso Science Institute, L'Aquila, Italy, November 19, 2018.
    
    
12. Slides (pdf) of the talk: Modeling Terms by Graphs with Structure Constraints (An Illustration with Background) at the Seminar of the Theoretical Computer Science group of VU Amsterdam, Amsterdam, the Netherlands, October 19, 2018.
    
    
13. Slides (pdf) of the talk: Modeling Terms by Graphs with Structure Constraints (Two Illustrations) at the Computer Science Seminar of Gran Sasso Science Institute, L'Aquila, Italy, August 30, 2018.
    
    
14. Slides (pdf) abstract (html), and extended abstract (pdf) for the invited talk: Modeling Terms by Graphs with Structure Constraints (Two Illustrations) at the workshop TERMGRAPH 2018, Oxford, England, UK, July 7, 2018.
    
    
15. Slides (pdf) for the talk Maximal Sharing in the Lambda Calculus with Letrec in the Seminar Theoretical Computer Science, Department of Computer Science, Vrije Universiteit Amsterdam, October 6, 2016.
    
    
16. Slides (pdf) for the talk Regularity Preserving but not Reflecting Encodings at the conference LICS 2015, Kyoto, Japan, July 9, 2015.
    
    
17. Slides (pdf, Easychair smart slides) 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.
    
    
18. 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.
    
    
19. 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, July 2, 2014.
    
    
20. 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.
    
    
21. 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.
    
    
22. Slides (pdf) for the talk Automatic Sequences and Zip-Specifications at LICS 2012 (25—28 June), Dubrovnik, Croatia, June 26, 2012.
    
    
23. Slides (pdf) for the talk Zip-Specifications and Automatic Sequences at the COiN Meeting, Radboud Universiteit, Nijmegen June 4, 2012.
    
    
24. Slides (pdf) for the talk Expressibility in the λ-calculus with Letrec presented by Jan Rochel at TeReSe Meeting, RWTH, Aachen, March 28, 2012.
    
    
25. 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.
    
    
26. 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.
    
    
27. Slides (pdf) for the talk Unique Normal Forms in Infinitary Weakly Orthogonal Term Rewriting at RTA 2010, Edinburgh, UK, July 13, 2010.
    
    
28. 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:
    • extended formats (pdf), July 7, 2010,
    • data-oblivious productivity (pdf), July 8, 2010,
    • complexity of productivity (pdf), July 8, 2010.
    
    
29. Slides (pdf) for the talk Unique Normal Forms in Infinitary Weakly Orthogonal Term Rewriting at the TeReSe Meeting, RWTH, Aachen, Germany, May 28, 2010.
    
    
30. 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.
    
    
31. Slides (pdf) for the talk Proving Productivity (Part 2) at the Symposium The End of Infinity, VU Amsterdam, December 15, 2009.
    
    
32. Slides (pdf) for the talk Graph Kernels, Logic, and Choice Axioms at the Symposium Tbilissi 2009, Bakuriani, Georgia, September 21, 2009.
    
    
33. Slides (pdf) for the talk Complexity of Fractran and Productivity at CADE 2009, McGill University, Montreal, Canada, August 6, 2009.
    
    
34. Slides (pdf) for the talk Data-Oblivious Stream Productivity at LPAR 2008, Carnegie Mellon Qatar Campus, Doha, Qatar, Nov 23, 2008.
    
    
35. Slides (pdf) for a talk Data-Oblivious Stream Productivity at PAM (Process Algebra Meeting), CWI, Amsterdam, May 7, 2008.
    
    
36. Slides (pdf) for a talk Watching Streams Grow: The Pebbleflow Method at the TF-Lunch Meeting of our department, Universiteit Utrecht, November 6, 2007.
    
    
37. Slides (pdf) for a talk Productivity of Stream Definitions at the TeReSe Meeting, TU/e, Eindhoven, NL, May 24, 2007.
    
    
38. 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.
    
    
39. Slides (pdf) and Extended Abstract (pdf) for a talk On the Star Height of Regular Expressions under Bisimulation at the Express'06 Workshop, Bonn, August 26, 2006.
    
    
40. Slides (pdf) for the talk A Coinductive Axiomatisation of Regular Expressions under Bisimulation, March 27, 2006, Short Contribution to CMCS 2006, March 25—27, Vienna Institute of Technology, Austria. Also available here is the Extended Abstract (pdf, and pdf early easier version) for this short contribution.
    
    Corrigendum: For two process graphs on the slides of this talk (see slides 8 and 20) that are indicated as 2-exit-iterations it was claimed there that they are not in the image of the process interpretation. While these statements are irrelevant to the results reported in this talk, they are both wrong: Each of these graphs satisfies the Loop Existence and Elimination Condition LEE (see LICS 2020 article above), and each of them is the process interpretations of a (under-star-1-free) regular expression. Hereby expressibility by (1-free) regular expressions is implied by the result reported at TERMGRAPH 2024 (see above) which states that the image of (under-star-1-free) regular expressions of a compact form of the process interpretation is closed under bisimulation collapse. From the proof of that more recent result it namely follows that all collapsed process graphs with the property LEE that consist of only a single connected component are not only compact process interpretations, but indeed process interpretations of (under-star-1-free) regular expressions. This fact entails that the process graph on slide 8 is the process interpretation of a regular expression, and it can be used to show that also the process graph on slide 20 is the process interpretation of a regular expression.
    
    
41. Slides (pdf) for a talk about the paper Using Proofs by Coinduction to Find `Traditional' Proofs given at CALCO 2005, on September 5, 2005, University of Wales Swansea, UK.
    
    
42. 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 March 22, 2005, 13.45—13.55.
    
    
43. Slides (pdf) for the talk H. Hüttel, C. Sterling: "Actions Speak Louder Than Words—Proving Bisimilarity for Context-Free Processes" given in TCS Seminar at Vrije Universiteit Amsterdam on December 26, 2004.
    
    
44. 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 June 22, 2004.
    
    
45. Slides (ps.gz) for a talk about A Duality in Proof Systems for Recursive Type Equality and for Bisimulation Equivalence on Cyclic Term Graphs at the TERMGRAPH 2002 Workshop, Barcelona, October 7, 2002.
    
    
46. Slides (ps.gz) for the talk Proving Equality for Recursive Types—A Duality Between `Syntactic-Matching' Tableaux and Brandt-Henglein derivations at PAM (Process Algebra Meeting), CWI, Amsterdam, May 8, 2002.
    
    
47. The note (ps.gz, pdf) Remarks about an Exercise by Detlef Plump April, 2002.
    
    
48. Slides (ps.gz) for the talk A Duality between Derivations and Consistency-Unfoldings in two different known Proof-System for Recursive Type Equality at OzsL-Accolade, Hotel Dennehoeve, Nunspeet, October 21, 2001.
    
    
49. Slides (ps.gz, 144K) for the talk A Duality between Derivations and Consistency-Unfoldings in two different known Proof-System for Recursive Type Equality in the TCS Seminar (Theoretical Computer Science Seminar) at Vrije Universiteit Amsterdam, September 14 and 21, 2001.
    
    
50. Slides (ps.gz) abstract (link html file), and handout (ps.gz) for the talk Proof-Theoretic Interconnections between Know Axiom- and Inference-Systems for the Equality and Subtype Relations on Recursive Types in the Lambda-Seminar of the Computer Science Department at KUN (Katholieke Universiteit Nijmegen), January 12, 2001.
    
    
51. Slides (ps.gz, ps), abstract (link html file), and handout (ps.gz) for the talk Proof-Theoretic Interconnections between Known Axiom- and Inference-Systems for Recursive Type Equality at OzsL-Accolade, Hotel Dennehoeve, Nunspeet, October 27, 2000.

---

---

Gran Sasso d'Italia, from Pizzo Cefalone (August 20, 2020): Pizzo Intermesoli, Corno Piccolo, and Corno Grande

---

---

References to software tools developed by Jan Rochel for joint work in the NWO-project ROS

During our joint work on the NWO-project Realising Optimal Sharing (ROS) (2009-2014) Jan Rochel developed the following very useful software tools:

• Maximal sharing implementation, and illustration (available via this link on Hackage):

  This tool is a prototype implementation of the maximal-sharing operation for functional programs in the λ-calculus with letrec as defined in our ICFP 2014 paper. Following the definition of maximally shared representations of such functional programs via a ‘representation pipeline’, the tool transforms a given functional program in the Core language of the λ-calculus with letrec into a term graph, and subsequently into a deterministic finite-state automaton (DFA). It prints intermediate representations, and graphically displays the obtained DFA. This DFA is then minimized, and finally a maximally shared representation of the original program is computed as the result.

• Port graph rewriting in Haskell (see explanatory technical report, suite available Hackage please find links on Jan Rochel's webpage):

  This is an animation tool for displaying and transforming port graphs (a general framework for graph transformations), and for carrying out rewrite-rule based transformations on these graphs per mouse-click. It produces beautifully rendered graphs that slowly float over the screen like bacteria in a liquid under a microscope.

For more information on these tools and our joint work, please visit Jan Rochel's webpage.

---