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. I work together a lot with Clemens Grabmayer. Here are some of my contributions.

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:

- graph-rewriting: base package defining an EDSL for specifying monadic graph rewriting rules and on top of that
- graph-rewriting-layout: force-directed port-graph layouting
- graph-rewriting-gl: OpenGL interface by which one can build interactive applications to interactively perform graph reductions, such as
- graph-rewriting-ski: implementation of the SKI combinators, which also serves as a tutorial to the suite.
- graph-rewriting-trs: evaluate a first-order term rewrite system interactively using graph reduction. You don't need to know Haskell to use this tool. Just define your rewrite rules in a separate file and give an initial term. This package could in principle replace graph-rewriting-ski, but is far more generic and involved and therefore not suited for a tutorial.
- graph-rewriting-lambdascope (screenshot): An implementation of an optimal evaluator for the λ-calculus, Lambdascope

The suite comes with a technical 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 exemplary implementations it should be possible to get by. Particularly the source code of the SKI combinator implementation is documented in tutorial style.

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. The 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.

`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. Repetitive Reduction Patterns in Lambda Calculus with letrec (Work in Progress). In Proceedings TERMGRAPH 2011. doi:10.4204/EPTCS.48.9

A more recent, more complete, and more messy version

`letrec`

An unpublished, unpolished, very theoretical paper (by my standards) whose main result is a characterisation of the class of infinite λ-terms that are expressible finitely using the `letrec`

construct.

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

.

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. Term Graph Representation for Cyclic Lamda-Terms to appear in the proceedings of the 7th International Workshop on Computing with Terms and Graphs, TERMGRAPH 2013, Rome, Italy, 23rd March 2013

music: Yes, definitively music. I have been playing piano from the age of 5. These days I'm focussing on Ravel. I'm also playing the drums for a bit, and I recently bought a guitar. I currently am a member of the Utrecht University Chamber Choir.

cinema: Want to know which are IMHO the greatest films ever made? Click the link!

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