Trustworthy Systems

Proof pearl: de bruijn terms really do work

Authors

Michael Norrish and Ren\'e Vestergaard

NICTA\ JAIST

Abstract

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.

BibTeX Entry

  @inproceedings{Norrish_Vestergaard_07,
    address          = {Kaiserslautern},
    author           = {Norrish, Michael and Vestergaard, Ren\'e},
    booktitle        = {International Conference on Theorem Proving in Higher Order Logics},
    editor           = {{Klaus Schneider and Jens Brandt}},
    keywords         = {lambda-calculus theorem-proving},
    month            = sep,
    pages            = {207--222},
    paperurl         = {https://trustworthy.systems/publications/nicta_full_text/594.pdf},
    publisher        = {Springer},
    series           = {Lecture Notes in Computer Science},
    title            = {Proof Pearl: de Bruijn Terms Really Do Work},
    volume           = {4732},
    year             = {2007}
  }

Download