Research

Currently I'm working as a Ph.D. at the Department of Information and Computing Sciences at the University of Utrecht on the NWO project Realising Optimal Sharing, which is a collaboration between the Center for Software Technology and the Department of Philosophy. The project is lead by Doaitse Swierstra and Vincent van Oostrom. Most of my research is due to joint efforts with Clemens Grabmayer. Here are some of my contributions.

Very Lazy Evaluation

My first publication describes a very lazy evaluation strategy (lazier than lazy evaluation, hence the name) on a generalised λ-calculus. Of this paper I am almost too ashamed to present it. That's because in it I have reinvented the wheel multiple times (different wheel each time), namely generalised β-reduction and head occurrence reduction the former having been introduced decades ago which shows that I haven't done my research right beforehand.

Jan Rochel. 2011. docThe very lazy λ-calculus and the STEC machine. In Proceedings of the 21st international conference on Implementation and application of functional languages (IFL'09), Marco T. Morazán and Sven-Bodo Scholz (Eds.). Springer-Verlag, Berlin, Heidelberg, 198-217.

Repetitive Reduction Patterns in Lambda Calculus with letrec

An optimisation that reduces the amount of β-reductions required to evaluate a term by lifting a certain kind of ‘constant’ parameters out of recursive positions. It is a generalisation of what is called the static argument transformation in GHC terminology.

Jan Rochel, Clemens Grabmayer. 2011. docRepetitive Reduction Patterns in Lambda Calculus with letrec (Work in Progress). Proceedings of TERMGRAPH 2011. Extended report: doi:10.4204/EPTCS.48.9

Expressibility in the Lambda Calculus with letrec

An unpublished paper which has as its main result a characterisation of the class of infinite λ-terms that are expressible finitely using the letrec-construct. It generalises results of a published paper (see below), in which the calculus has μ instead of letrec.

Clemens Grabmayer, Jan Rochel, 2012. docExpressibility in the Lambda Calculus with letrec.

Expressibility in the Lambda Calculus with μ

Clemens Grabmayer, Jan Rochel, 2013. docExpressibility in the Lambda Calculus with μ. Proceedings of RTA 2013.

Term Graph Representation for Cyclic Lambda-Terms

We study various representations for cyclic λ-terms as higher-order or as first-order term graphs. It is intended as a stepping stone for a follow-up paper about maximal sharing in λ-letrec.

Clemens Grabmayer, Jan Rochel, 2013. docTerm Graph Representation for Cyclic Lambda-Terms to appear in the proceedings of the 7th International Workshop on Computing with Terms and Graphs, TERMGRAPH 2013, Rome, Italy, 23rd March 2013

Maximal Sharing in the Lambda Calculus with letrec

Applying bisimulation on term graph interpretations of λ-letrec yields two results: a generalisation of Common Subexpression Elimination; and an efficient method to determine whether two λ-letrec-terms have the same unfolding.

Clemens Grabmayer, Jan Rochel, 2014. docMaximal Sharing in the Lambda Calculus with letrec. Accepted at ICFP 2014

Port graph rewriting in Haskell

Investigating different evaluators for the λ-calculus involves a lot of graph rewriting. It turned out that there is a lack of tools for specifying such systems and experimenting with them. Consequently I have implemented a suite of Haskell libraries and applications for interactive port graph rewriting, available on HackageDB:

Packages

Documentation

The suite comes with a doctechnical report as documention, which is unfortunately hardly complete. But together with the API documentation (see the links to the packages on HackageDB above) and the example implementations it should be possible to get by. The source code of the SKI combinator implementation is documented in tutorial style.

Further interests

music: Yes, definitively music. I have been playing piano from the age of 5. These days I'm focussed on Ravel. I'm also playing some drums, and for two years I have been playing the guitar. You can listen to a couple of covers I recorded. I currently am a member of the Utrecht University Chamber Choir.

cinema: A magical link that reveals to you the greatest films ever made.

Imprint

Jan Rochel <jan@rochel.info> (my public-key for encrypted communication: GPG-file)

Valid XHTML 1.0 Transitional Valide CSS! <Esc>:wq