Nominal Isabelle/HOL

31/01/2025 16 min Temporada 6 Episodio 5
Nominal Isabelle/HOL

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.