ENTCS
2007
15 years 10 days ago
2007
Often debates about pros and cons of various techniques for formalising lambda-calculi rely on subjective arguments, such as de Bruijn indices are hard to read for humans or nomin...
CADE
2005
Springer
16 years 21 days ago
2005
Springer
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...