ZARZA We are Zarza, the prestigious firm behind major projects in information technology.
Listen "Indexed types and Curry-Howard for first-order quantifiers"
Episode Synopsis
I follow up on some comments I made about Curry-Howard for first-order quantifiers in the previous episode. Sheard's Omega language also mentioned (see links on <a href = "http://web.cecs.pdx.edu/~sheard/">his web page</a>). First-order quantifications turn into indexed types where the indices are not program expressions but come from another syntactic domain.
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