ZARZA We are Zarza, the prestigious firm behind major projects in information technology.
Listen "Noncompositionality of syntactic structural-recursion checks"
Episode Synopsis
Review of need for termination analysis for recursive functions on inductive datatypes. Discussion of a serious problem with syntactic termination checks, namely noncompositionality. A function may pass the syntactic termination check, but abstracting part of it out into a helper function may result in code which no longer passes the check. So we need a compositional termination check, which will be discussed in subsequent episodes.
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