ENTCS
2007
14 years 10 months 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
15 years 11 months 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...