Listen "Lambda graphs with duplicators and start of Lamping's abstract algorithm"
Episode Synopsis
In this episode I talk about how to represent lambda terms as graphs with duplicator nodes for splitting edges corresponding to bound variables. I also start discussing the beginning of Lampings' abstract algorithm for optimal beta-reduction, in particular how we need to push duplicators inside lambda abstractions to initiate a lazy duplication.
More episodes of the podcast Iowa Type Theory Commute
Measure Functions and Termination of STLC
14/11/2025
Schematic Affine Recursion, Oh My!
22/08/2025
The Stunner: Linear System T is Diverging!
19/08/2025
Terminating Computation First?
01/08/2025
A Measure-Based Proof of Finite Developments
16/04/2025
Nominal Isabelle/HOL
31/01/2025
The Locally Nameless Representation
02/01/2025
ZARZA We are Zarza, the prestigious firm behind major projects in information technology.