ZARZA We are Zarza, the prestigious firm behind major projects in information technology.
Listen "Terminating Computation First?"
Episode Synopsis
In this episode, I discuss an intriguing idea proposed by Victor Taelin, to base a logically sound type theory on an untyped but terminating language, upon which one may then erect as exotic a type system as one wishes. By enforcing termination already for the untyped language, we no longer have to make the type system do the heavy work of enforcing termination.
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
A Measure-Based Proof of Finite Developments
16/04/2025
Nominal Isabelle/HOL
31/01/2025
The Locally Nameless Representation
02/01/2025
POPLmark Reloaded, Part 2
22/12/2024
In God we trust