@inproceedings{c2e70c15f6b845bf88579555eee4df32,
title = "Proof pearl: De Bruijn terms really do work",
abstract = "Placing our result in a web of related mechanised results, we give a direct proof that the de Bruijn λ-calculus ({\`a} la Huet, Nipkow and Shankar) is isomorphic to an α-quotiented λ-calculus. In order to establish the link, we introduce an {"}index-carrying{"} abstraction mechanism over de Bruijn terms, and consider it alongside a simplified substitution mechanism. Relating the new notions to those of the a-quotiented and the proper de Bruijn formalisms draws on techniques from the theory of nominal sets.",
author = "Michael Norrish and Ren{\'e} Vestergaard",
year = "2007",
doi = "10.1007/978-3-540-74591-4_16",
language = "English",
isbn = "9783540745907",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "207--222",
booktitle = "Theorem Proving in Higher Order Logics - 20th International Conference, TPHOLs 2007, Proceedings",
address = "Germany",
note = "20th International Conference on Theorem Proving in Higher-Order Logics, TPHOLs 2007 ; Conference date: 10-09-2007 Through 13-09-2007",
}