Sciweavers

CADE
2005
Springer
15 years 23 days ago
Nominal Techniques in Isabelle/HOL
Abstract This paper describes a formalisation of the lambda-calculus in a HOL-based theorem prover using nominal techniques. Central to the formalisation is an inductive set that i...
Christian Urban, Christine Tasson