Joachim Breitner's Homepage

Today was a nice day with a surprising number of early Christmas presents:

• I submitted my Ph.D. thesis “Lazy Evaluation: From formal semantics to to a machine-checked compiler transformation” about an Isabelle formalisation of Launchbury’s natural semantics (also found in the Launchbury entry in the Archive of Formal Proofs), about the GHC optimization “Call Arity” that I developed (see the TFP 2014 paper) and a formal proof that it is indeed an optimization (Haskell Symposium 2015 paper, AFP entry). After 243 pages, it is finally done and I can now turn to new things.

  Speaking of “something new”: I’m hunting jobs right now. I am in particular interested in academic post-doc positions in my field (functional programming languages and/or interactive theorem proving), but I’d also like to hear about attractive non-academic positions that fit my profile.

• Someone who I value and respect a lot asked me to co-author a paper with him. I am not sure whether further details at this stage belong to a public blog post, so I’ll keep them back. But nevertheless this is very nice.

• A paper on information flow control by my colleagues Jürgen Graf, Martin Hecker and Martin Mohr, my advisor Gregor Snelting and (although only marginally) me was accepted at POST 2016, and the notification reached us today.

• Together with Carsten Podszun, I have written an article about the Ravensburger Tip-toi pen and how to create your own books for that using the tttool program that I have created for the German magazine Make:, and it is included in issue 6/2015, which arrived today in my mailbox.

• The Incredible Proof Machine attracts new contributors. Well, one. But a few days ago, I heard that a 11½ year old girl has great fun with it!

• Tonight, my group is having their Christmas party and I can expect to be fed well by home-cooked Mexican something. Got to go…