Listen "Nominal Isabelle/HOL"
Episode Synopsis
In this episode, I discuss the paper Nominal Techniques in Isabelle/HOL, by Christian Urban. This paper shows how to reason with terms modulo alpha-equivalence, using ideas from nominal logic. The basic idea is that instead of renamings, one works with permutations of names.
More episodes of the podcast Iowa Type Theory Commute
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
The Locally Nameless Representation
02/01/2025
POPLmark Reloaded, Part 2
22/12/2024
POPLmark Reloaded, Part 1
22/12/2024