Proof Pearl: de Bruijn Terms Really Do Work

Select |




Print


Norrish, Michael; Vestergaard, René

Norrish, Michael; Vestergaard, René


2007-09-20


Conference Material


Theorem Proving in Higher Order Logics, 20th International Conference


Kaiserslautern


4732


207-222


Placing our result in a web of related mechanised results, we give a direct proof that the de Bruijn λ-calculus (à 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 α-quotiented and the proper de Bruijn formalisms draws on techniques from the theory of nominal sets.


Springer


lambda-calculus theorem-proving


http://rsg.informatik.uni-kl.de/TPHOLs-2007/


Lecture Notes in Computer Science


nicta:594


Norrish, Michael; Vestergaard, René. Proof Pearl: de Bruijn Terms Really Do Work. In: Klaus Schneider and Jens Brandt Editor, editor/s. Theorem Proving in Higher Order Logics, 20th International Conference; Kaiserslautern. Springer; 2007-09-20. 207-222.



Loading citation data...

Citation counts
(Requires subscription to view)