Skip to content
Sign in
Artwork for Iowa Type Theory Commute
Iowa Type Theory Commute · Jan 31, 2025 · 16 min

Nominal Isabelle/HOL

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.

0:00-16:18
Play in

transcript

No transcript — this publisher did not publish one.

show notes

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. 

links1

more episodes

All episodes