mathr / blog / #

GULCII in Edinburgh


Today I presented GULCII, my Graphical Untyped Lambda Calculus Interactive Interpreter, at the University of Edinburgh Informatics department. It went well I think. The first go around in the morning I missed some slides about de Bruijn indexes but the afternoon audience seemed to be familiar with it. First I performed with GULCII, the same set as the FARM conference music evening, testing an equivalence between Church encoding and Scott encoding of natural numbers. Then I presented some slides about those encoding schemes of data in untyped lambda calculus, and a bit about how GULCII works, some shortcomings, and ideas for future developments.

A week before the talk I discovered a bad bug in the evaluator ("exp two two" with Church numerals was not equal to "four"), but I managed to rewrite it in time, using the "scope extrusion" rules from the Lambdascope paper. However, sharing is still broken, so the next version will probably switch to using Lambdascope as a library, so that full lazy graph reduction will work properly. The bug had been there since 2011, and is visible in the video of my FARM performance.

You can download the slides from my presentation, or view the Pandoc Markdown for LaTex Beamer source code. I might upload some video of the second talk soon. GULCII itself is on Hackage so you can install it with cabal install gulcii.

Incidentally the brickwork opposite the Informatics Forum reminded me of Donky Kong, with its ladders:

Crichton Street