Slides on Measure-Based Termination for STLC
I gave this talk at NEPLS this morning! It was fun, and seemed to get people curious about this problem.
QA9
Exploring the Computational Logic Literature
Latest posts
Notes for “The Stunner”
I am releasing a podcast episode where I discuss some parts of the paper “Gödel’s system T revisited”, and here is a brief note with some of the definitions I tried to talk through:
A Script for Wadler’s Parable of LEM
In 2005, I believe it was, I watched Phil Wadler and Frank Pfenning perform a dramatic version of the proof, under Curry-Howard and following Griffin, of the Law of Excluded Middle. Amazing to see Frank in horns. This way of understanding Curry-Howard for LEM has stuck with me ever since. For my spring class, I […]
A Measure-Based Proof of the Finite Developments Theorem
RTA Open Problem 19 asks for a measure-based proof of termination for beta-reduction of simply typed terms. I thought hard about this in the fall (2024) and got… nowhere really. One good thing that came out of the head-banging exercise was finding this paper: In it, de Vrijer gives a measure-based proof of termination for […]
Could tail be a fold?
Did you know you can write a safe version of the tail function as a fold? Did you know you can’t? Let me start with the second question. In this very interesting paper from some years ago, illustrious authors give necessary and sufficient conditions for when a function can be expressed as a fold (or […]
What kind of principle is parametricity?
Parametricity is a profound principle in the theory of programming languages — but what kind of principle is it? To answer this, let me first recall the idea, as introduced by the great John C. Reynolds in his seminal paper “Types, Abstraction, and Parametric Polymorphism”. (I wrote about this paper in an earlier post.) Suppose […]
Logging, pure and simple
I recently watched a pretty inspiring talk by Avi Press about his experience using Haskell at his startup, Scarf. I enjoyed the whole talk, but something that particularly got me excited was his point that although Haskell is pure, in practice, almost all the code his company was writing ended up being monadic. One simple reason was […]
Practical Strong Functional Programming
Strong functional programming was proposed by David Turner, a founding father of modern functional programming (FP), as a better version of the functional programming paradigm realized today in Haskell. Where Haskell insists on purity, strong FP further insists that all functions terminate on all inputs. So strong FP goes beyond pure FP, to guarantee an […]
Predecessor with maybe
Everyone hates to define the predecessor function on Church-encoded natural numbers, right? The wikipedia page has a couple painful options, including Kleene’s solution. Now, I don’t know how original this is, but here is a simpler one. Code below checks in Haskell (with ghc), using language extensions TypeApplications , ExplicitForAll , ImpredicativeTypes. (Thanks to ghc […]
Deriving a case of the omega-rule in pure lambda calculus
The omega-rule of lambda calculus is the principle that if for all closed terms t we have t1 t beta,eta-equal to t2 t, then t1 is beta,eta-equal to t2. This principle is not valid for all t1 and t2, due to the existence of so-called universal generators, which Gordon Plotkin used in a 1974 paper […]