Skip navigation

This past Tuesday (June 19) I gave the second lecture in the series I am working on, about optimal beta-reduction.  The screencast can be found here.  This lecture covers the basic nondeterministic graph reduction rules for lazy duplication.  The notes you will see my writing are here in ora and jpeg formats.  The lambdascope implementation I try using (and many thanks to Jan Rochel for this!) can be found here on hackage.  The lambdascope paper can be found here.


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

As you may know (for example, from my interview a little while back on the fantastic Type Theory Podcast), we are working here at U. Iowa on a new dependent type theory implementation called Cedille.  It is based on a new extrinsic (aka Curry-style) type theory, and aims to be a very compact theory in which standard parts of dependent type theory like inductive (and hopefully coinductive) datatypes can be defined from the more primitive constructs of the theory.

At our first Cedille meeting of the fall semester — also in attendance Larry Diehl, Richard Blair, Chris Jenkins, Tony Cantor, Colin McDonald, Nadav Kohen — I gave a rather long overview of the current state of Cedille, which I recorded as a screencast and as the notes I was drawing (.ora and .jpg formats) while talking.  While we are (still! [sigh]) not quite ready to make a public release, I think we will get there this fall, as I mention in the screencast.  A few quick highlights are: we have a derivation of induction that is parametrized by a functor (actually, we have two: one for Church encoding and one for Mendler encoding); we can do some surprising and cool things with casts, which are derivable in the theory, including define within Cedille monotone recursive types and get proof reuse between types which can be cast to each other, like lists and vectors; and we just need to complete a (very basic) module system and solve an unpleasant performance issue with our parser, and we should be ready to make a release.

I recently (May 1) gave a short presentation touching on ethics and technology, as well as the ethics of Internet pornography.  I am sharing the slides here.  Sadly, most of the references on the seemingly unending list of harms and evils associated with pornography are behind paywalls, although the article by Max Waltman is freely available.  As always when reading about this topic, please be aware that some of the material can be quite upsetting for people who have experienced sexual assault, abuse, childhood assault, or other traumatic experiences, as well as for young readers.

I have been blessed the past few days to have some amazing conversations with people working with me here at Iowa.  For one of these, I talked yesterday with Richard Blair and Ananda Guneratne about semantics of recursive types, as this is something Richard is currently working on.  The conversation was so inspiring I wrote up a short note summarizing it.  You can find this note here.