ZARZA We are Zarza, the prestigious firm behind major projects in information technology.
Listen "Explaining my encoding of a HOAS datatype, part 1"
Episode Synopsis
I start explaining an idea from my paper "A Weakly Initial Algebra for Higher-Order Abstract Syntax in Cedille", 2019, available from my web page. The goal is to encode a datatype (including its constructors, which we saw were troublesome for higher-order signatures generally in the previous episode) for application-free lambda terms, which I submit is the simplest higher-order datatype possible. I just explain some of the setup, and will attempt wading through the details next time.
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
In God we trust