ENTCS
2007
13 years 4 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
14 years 4 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...