bib.bib

@article{abadi1991,
  author    = {Mart\'{\i}n Abadi and
               Luca Cardelli and
               Pierre-Louis Curien and
               Jean-Jacques L{\'e}vy},
  title     = {Explicit Substitutions},
  journal   = {J. Funct. Program.},
  volume    = {1},
  number    = {4},
  year      = {1991},
  pages     = {375-416},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{deBruijn1972381,
title = "Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the {C}hurch-{R}osser theorem",
journal = "Indagationes Mathematicae (Proceedings)",
volume = 75,
number = 5,
pages = "381 - 392",
year = 1972,
issn = "1385-7258",
author = {de Bruijn, N. G.}
}

@incollection{adams2006formalized,
year=2006,
isbn={978-3-540-31428-8},
booktitle={Types for Proofs and Programs},
volume=3839,
series={Lecture Notes in Computer Science},
title={Formalized Metatheory with Terms Represented by an Indexed Family of Types},
publisher={Springer Berlin Heidelberg},
author={Adams, Robin},
pages={1-16}
}

@incollection{polonowski2013dbgen,
year={2013},
isbn={978-3-642-39633-5},
booktitle={Interactive Theorem Proving},
volume={7998},
series={Lecture Notes in Computer Science},
title={Automatically Generated Infrastructure for De {Bruijn} Syntaxes},
publisher={Springer Berlin Heidelberg},
keywords={De Bruijn syntax; formalization; infrastructure generation; Coq proof assistant},
author={Polonowski, Emmanuel},
pages={402-417}
}

@incollection{poplmark,
year=2005,
isbn={978-3-540-28372-0},
booktitle={Theorem Proving in Higher Order Logics},
volume=3603,
series={Lecture Notes in Computer Science},
doi={10.1007/11541868_4},
title={Mechanized Metatheory for the Masses: The {PoplMark} Challenge},
publisher={Springer Berlin Heidelberg},
author={Aydemir, Brian E. and Bohannon, Aaron and Fairbairn, Matthew and Foster, J. Nathan and Pierce, Benjamin C. and Sewell, Peter and Vytiniotis, Dimitrios and Washburn, Geoffrey and Weirich, Stephanie and Zdancewic, Steve},
pages={50-65}
}