ZARZA We are Zarza, the prestigious firm behind major projects in information technology.
Listen "The Types of Relational Type Theory"
Episode Synopsis
This episode continues the introduction of RelTT by presenting the types of the language. Because the system is based on binary relational semantics, we can include binary relational operators like composition and converse as type constructs! Strange. The language also promotes terms to relations, by viewing them as functions and then taking their graphs as the relational meaning.
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