Read more ...

Originally, I am from Linz, Austria, where I studied technical mathematics at the Johannes Kepler University and graduated in 1997 with a thesis on the decision complexity of Presburger Arithmetic (supervised by Alexander Leitsch). I came to the Netherlands in 1998, following my enthusiasm for the Dutch tradition of Intuitionism in the foundations of mathematics. I joined a graduate program in logic at the ILLC of the Universiteit of Amsterdam, at the end of which I wrote a master's thesis (under the supervision of Anne Sjerp Troelstra) on cut-elimination and its computational content in a variation of Gentzen's sequent calculus for predicate logic. Subsequently I was Ph.D. student at the theory section of the Department of Computer Science of the Vrije Universiteit Amsterdam, working on interpretational proof theory, and classical as well as coinductive proof systems. In 2005 I obtained a Ph.D. (promotor: J.W. Klop, see also J.W.K.'s personal page) with a thesis on proof theoretic connections between proof systems for recursive type equivalence. Subsequently for two-and-a-half years I was postdoc in the same group, employed for the NWO-project "GeoProc", which was concerned with investigating geometrical, as well as topological, proofs in process theory. Also, I worked on Robin Milner's process interpretation of regular expressions.

In February I joined the Department of Philosophy in the framework of the NWO-BRICKS Project Infinity, which links our department (Albert Visser and Vincent van Oostrom are part of the research team) with two research groups in Amsterdam (Theor. Computer Science, VU, SEN-3, CWI) and which brings together three different fields: term rewriting, coalgebra, and proof theory. In this project we are interested in the precise formal treatment of infinite mathematical objects such as streams (infinite sequences) and infinite trees. Starting already last year, I have collaborated with four colleagues from the VU in work concerning the question of `productivity': How can it be recognised whether a given (finitary) stream definition does indeed evaluate to an infinite stream? This is an undecidable problem. But for a rich subclass we have found and also implemented a substantially new decision algorithm that we expect to be a useful tool for functional programming practice. Currently we work on a number of extensions of this result. As another goal I want to investigate, together with Vincent van Oostrom, ideas used for the result on productivity with the aim of developing statements clarifying the precise extent to which term graph rewriting systems can be viewed as a semantics for (finitary or infinitary) term rewriting systems.


Poster Pitch for our `Infinity' Poster given at the BRICKS-Midterm Symposium, CWI, Amsterdam, March 13, 2007

Clemens Grabmayer for project `Infinity': We are interested in infinite mathematical objects such as infinite sequences and infinite trees. An example you can see right on top: the famous Thue Morse sequence, a stream of zeros and ones that is aperiodic, full of symmetries, and can be visualised as a beautiful mosaic.

The project links together three research groups in Amsterdam and Utrecht as well as three different fields: term rewriting, coalgebra, and proof theory.

To mention only one result: we just submitted a paper concerning the question of `productivity': How can it be recognised whether a given stream definition evaluates to a unique infinite stream? This is an undecidable problem. But for a rich subclass we have found and implemented a substantially new decision algorithm that can be useful for functional programming practice.

For more information, search "BRICKS Infinity Project".


Productiviteit van Streamspecificaties

The text in Dutch called Productiviteit van Streamspecificaties, which gives an overview about our research concerning productivity of stream definitions, and which has been written for the periodical ``De Filosoof'' of the association of philosophy students of Utrecht University is available as a (doc)[MS-Word]-file.
(My thanks for helping with corrections of my Dutch sentences in this text go to Dimitri Hendriks and Vincent van Oostrom.)


[Back to my homepage]


Clemens Grabmayer / Universiteit Utrecht / clemens one at phil one dot uu one dot nl / Last modified: Thu Sep 27 12:07:25 MET DST 2007