Skip navigation

It is a warm start to summer here in Iowa, and among other interesting things to think about, I have been studying the subject of optimal beta-reduction, which has been developed from Jean-Jacques Levy’s dissertation in the 1970s to John Lamping’s 1990 POPL paper, and beyond.  I am using an amazing book by Andrea Asperti and Stefano Guerrini: The Optimal Implementation of Functional Programming Languages.

To help myself learn this, I am giving (and have decided to record) some lectures on the topic.  I am definitely not an expert, only an aspirant!  If you happen to watch these and find errors or confusions, please correct me.  The screencast for the first lecture, covering some main points of Chapter 2 of Asperti and Guerrini, is here.  The notes you will see me writing in the screencast are here, in jpg and ora formats.

I am interested in this because my friend Victor Maia of Ethereum Foundation is considering using a variant of Lamping’s abstract algorithm to run smart contracts in Ethereum, to be written in pure lambda calculus and verified with Cedille (the tool we are working on here now the past few years).



  1. Hey Aaron,
    I’m very happy you got interested in the topic. In my opinion variants of this reduction order are superior to call by value, call by name and very close to call-by-need.
    I recommend you read short Andrea’s paper which puts optimal reduction in context of practice
    In particular, note that Optimal reduction is time-optimal but very peak-memory-inoptimal. Situation is similar to Haskell’s space-leaks (sometimes also slightly incorrectly called memory leaks).

    I’m drawing the attention to this topic since my belief is that this is the main obstacle from wide adoption.

    • Many thanks, Łukasz, for your comment and the link to this short paper of Asperti’s. I am eager to read it! There is a lot to understand in this area…

Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out /  Change )

Google photo

You are commenting using your Google account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s

%d bloggers like this: