Publications and Scientific Work by Clemens Grabmayer
Not all versions given here are identical to the
the associated published one. The technical
contents are the same.
The documents distributed by this server have been provided as a
means to ensure timely dissemination of scholarly and technical
work on a noncommercial basis. Copyright and all rights therein
are maintained by the authors or by other copyright holders,
notwithstanding that they have offered their works here
electronically. It is understood that all persons copying this
information will adhere to the terms and constraints invoked by
each author's copyright. These works may not be reposted without
the explicit permission of the copyright holder.
Publications and Technical Reports
2014
 C. Grabmayer, and D. Hendriks:
CoReflexivity = Symmetry + AntiSymmetry,
note, 22 March 2014.
 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
 C. Grabmayer, and J. Rochel:
Term Graph Representations for Cyclic LambdaTerms,
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).
 C. Grabmayer, and J. Rochel
Confluent LetFloating,
Proceedings of IWC 2013,
the 2nd International Workshop on Confluence,
June 28, 2013, Eindhoven, NL
(pdf,
slides talk at the workshop).
 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).
 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)).
 C. Grabmayer, and J. Rochel:
Term Graph Representations for Cyclic LambdaTerms,
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.
 J. Endrullis, C. Grabmayer, D. Hendriks:
MixAutomatic Sequences,
Paper at LATA 2013,
Proceedings of LATA 2013, April 25, Bilbao, Spain, LNCS 7810,
(proceedings page at Springer Link,
(local copy article (pdf)).
2012
 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).
 C. Grabmayer, J. Endrullis, D. Hendriks, J.W. Klop, L.S. Moss:
Automatic Sequences and ZipSpecifications, versions:
2011
 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 31753202
(doi:10.1016/j.tcs.2011.04.011,
pdf [local copy]).
 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 367393, doi:10.1017/S1755020310000286,
© Cambridge University Press,
(pdf [local copy]).
 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]).
 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),
(arXived at: http://dx.doi.org/10.4204/EPTCS.48.9,
pdf [local copy]) .
2010
 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).
 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).
 J. Endrullis, C. Grabmayer, D. Hendriks, J.W. Klop, V. van Oostrom:
Unique Normal Forms in Infinitary Weakly Orthogonal Term Rewriting,
proceedings of RTA2010
(pdf),
link to RTA2010 Proceedings
at LIPIcs.
2009
 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).
 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).
 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).
 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).
 J. Endrullis, C. Grabmayer, D. Hendriks:
Complexity of Fractran and Productivity,
proceedings of CADE22
(pdf,
talk at CADE22 (pdf)).
 J. Endrullis, C. Grabmayer, D. Hendriks:
Complexity of Fractran and Productivity,
technical report
(pdf,
arXiv:0903.4366).
 J. Endrullis, C. Grabmayer, D. Hendriks, J.W. Klop, and R. de Vrijer:
Proving Infinitary Normalization, TYPES'08 PostProceedings, to appear
(pdf).
 J. Endrullis, C. Grabmayer, D. Hendriks, and J.W. Klop:
Infinite Streams, NVTINieuwsbrief, Maart 2009
(pdf).
2008

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).
 J. Endrullis, C. Grabmayer, D. Hendriks:
DataOblivious Stream Productivity,
Proceedings of LPAR 2008, LNCS 5330, pages 7996, Springer Verlag 2008
(pdf (local copy),
paper's page
at SpringerLink.com,
talk at LPAR 2008 (pdf)).
 J. Endrullis, C. Grabmayer, D. Hendriks:
DataOblivious Stream Productivity,
technical report
(pdf,
arXiv:0806.2680).
2007

C. Grabmayer:
Productiviteit van Streamspecificaties
(doc),
Faculteitsblad De Filosoof,
Nummer 36,
Afdeling Wijsbegeerte, Universiteit Utrecht, September 2007.

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 274287, Springer Verlag, 2007
(paper's page at Springerlink,
pdf (via Springerlink),
pdf (local copy),
BibTeXentry).

C. Grabmayer:
A Duality Between Proof Systems for Cyclic Term Graphs,
(paper's page,
link to pdffile at the Cambridge Journal portal;
local copy of pdffile,
BibTeXentry),
Mathematical Structures in Computer Science, volume 17, issue 3, pages 439484,
2007.

J.C.M. Baeten, F. Corradini, and C. Grabmayer:
A Characterization of Regular Expressions under Bisimulation,
(paper's page,
link to pdffile at ACM's portal,
local copy of pdffile
BibTeXentry),
Journal of the ACM, volume 54, issue 2, pages 228, April 2007.
2006

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

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.

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 NS053
(link to pdffile),
pages 118123, 2005.
Also in: L. Aceto and A.D. Gordon (editors),
Proceedings of the Workshop
"Essays on Algebraic Process Calculi" (APC 25),
Bertinoro, Italy, 0105 August 2005,
ENTCS, Volume 162, Pages 183190 (29 September 2006)
(link to pdffile at Elsevier's Science Direct,
local copy of pdffile).

C. Grabmayer: Using Proofs by Coinduction to Find ``Traditional'' Proofs
(pdf,
BibTeXentry).
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

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

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

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.

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 IR499, juli 2002.
[
Back to my homepage]
List of BibTeX Entries
Here you find a
preliminary list
of BibTeXEntries of my publications.
[
Back to my homepage]
Poster Presentations

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

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
 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 diplomathesis
[ps.gz, 1016K]
is available here.
 C. Grabmayer:
"CutElimination in the Implicative Fragment of a G3miGentzensystem
and its Computational Content",
master'sthesis 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 asciitext format
available for this thesis.
[
Back to my homepage]
Talks and Miscellaneous Work
 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.
 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.
 Slides
(pdf)
for the talk
Confluent LetFloating
at the
International Workshop on Confluence (IWC 2013) (28 June 2013),
Technical University Eindhoven,
June 28, 2013.
 Slides
(pdf)
for the talk
Expressibility in the LambdaCalculus with Mu
at
RTA 2013 (2426 June),
Technical University Eindhoven, Netherlands,
June 25, 2012.
 Slides
(pdf)
for the talk
Automatic Sequences and ZipSpecifications
at
LICS 2012 (2528 June),
Dubrovnik, Croatia,
June 26, 2012.
 Slides
(pdf)
for the talk
ZipSpecifications and Automatic Sequences
at the
COiN Meeting,
Radboud Universiteit, Nijmegen
June 4, 2012.
 Slides
(pdf)
for the talk
Expressibility in the λcalculus with Letrec
presented by Jan Rochel
at
TeReSe Meeting,
RWTH, Aachen,
March 28, 2012.
 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.
 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.
 Slides
(pdf)
for the talk
Unique Normal Forms in Infinitary Weakly Orthogonal Term Rewriting
at RTA 2010, Edinburgh, UK,
July 13, 2010.
 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,
 dataoblivious productivity (pdf),
July 8, 2010,
 complexity of productivity (pdf),
July 8, 2010.
 Slides
(pdf)
for the talk
Unique Normal Forms in Infinitary Weakly Orthogonal Term Rewriting
at the
TeReSe Meeting,
RWTH, Aachen, Germany,
May 28, 2010.
 Slides
(pdf)
for the talk
Equivalence of Stream Specifications
at the
Workshop on Proof Theory and Rewriting,
Universitätszentrum Obergurgl, March 2831, 2010,
March 28, 2010.
 Slides
(pdf)
for the talk
Proving Productivity (Part 2)
at the Symposium The End of Infinity,
VU Amsterdam, Dec 15, 2009.
 Slides
(pdf)
for the talk
Graph Kernels, Logic, and Choice Axioms
at the Symposium Tbilissi 2009,
Bakuriani, Georgia, September 21, 2009.
 Slides
(pdf)
for the talk
Complexity of Fractran and Productivity
at CADE 2009, McGill University, Montreal, Canada,
Aug 6, 2009.
 Slides
(pdf)
for the talk
DataOblivious Stream Productivity
at LPAR 2008, Carnegie Mellon Qatar Campus, Doha, Qatar,
Nov 23, 2008.
 Slides
(pdf)
for a talk
DataOblivious Stream Productivity
at PAM (Process Algebra Meeting), CWI, Amsterdam,
May 7, 2008.
 Slides
(pdf)
for a talk
Watching Streams Grow: The Pebbleflow Method
at the TFLunch Meeting of our department, Universiteit Utrecht,
November 6, 2007.
 Slides
(pdf)
for a talk
Productivity of Stream Definitions
at the
TeReSe Meeting,
TU/e, Eindhoven, NL,
May 24, 2007.
 Slides
(pdf)
for a talk
Regular Expressions Under the Process Interpretation
at the
Workshop on Proof Theory and Rewriting 2006
,
Obergurgl, Austria,
September 59, 2006.
 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.

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

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.

Slides
(pdf)
for the talk at my PhDdefense 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.

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.

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.

A talk on
``Proving Equality for Recursive Types  A Duality Between
`SyntacticMatching' Tableaux and BrandtHenglein 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].

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

A talk on
A Duality between Derivations and ConsistencyUnfoldings in
two different known ProofSystem for Recursive Type Equality
held at the OzsLAccolade on
October 21st, 2001 at
Hotel Dennehoeve, Nunspeet.
The LATEXed slides for this talk are available here in the form of a
[ps.gz, 124K].

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

An extended talk on
ProofTheoretic Interconnections between Know Axiom and InferenceSystems
for the Equality and Subtype Relations on Recursive Types
given in the
LambdaSeminar of the Computer Science Department
at the KUN (Katholieke Universiteit Nijmegen) at
January 12th, 2001,
10:3012:15.
Confer here for a short
abstract [link to a local htmlfile]
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.)

A talk on
ProofTheoretic Interconnections between Known Axiom and InferenceSystems
for Recursive Type Equality given at
the OzsLAccolade, Nunspeet,
27th October 2000.
Confer here for a short abstract [link to a local htmlfile]
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 handoutversion (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 / Universiteit Utrecht /
clemens one at
phil one dot
uu one dot
nl
/
Last modified: Fri Aug 1 18:46:55 CEST 2014
/