references.bib

@PREAMBLE{"\providecommand{\refSortAs}[1]{}"}

@inproceedings{AydemirCPPW08,
  author       = {Brian E. Aydemir and
                  Arthur Chargu{\'{e}}raud and
                  Benjamin C. Pierce and
                  Randy Pollack and
                  Stephanie Weirich},
  editor       = {George C. Necula and
                  Philip Wadler},
  title        = {Engineering formal metatheory},
  booktitle    = {Proceedings of the 35th {ACM} {SIGPLAN-SIGACT} Symposium on Principles
                  of Programming Languages, {POPL} 2008, San Francisco, California,
                  USA, January 7-12, 2008},
  pages        = {3--15},
  publisher    = {{ACM}},
  year         = {2008},
  url          = {https://doi.org/10.1145/1328438.1328443},
}

@article{deBruijn72,
  author  = {Nicolaas G. {\refSortAs{Bruijn}{de Bruijn}}},
  title   = {Lambda calculus notation with nameless dummies,
    a tool for automatic formula manipulation, with application to the {Church}-{Rosser} theorem},
  journal = {Indagationes Mathematicae (Proceedings)},
  volume  = {75},
  number  = {5},
  pages   = {381--392},
  year    = {1972},
  issn    = {1385-7258},
  url     = {https://doi.org/10.1016/1385-7258(72)90034-0},
}

@article{Chargueraud12,
  author       = {Arthur Chargu{\'{e}}raud},
  title        = {The Locally Nameless Representation},
  journal      = {Journal of Automated Reasoning},
  volume       = {49},
  number       = {3},
  pages        = {363--408},
  year         = {2012},
  url          = {https://doi.org/10.1007/s10817-011-9225-2},
}

@article{Huet97,
  author       = {G{\'{e}}rard Huet},
  title        = {The Zipper},
  journal      = {Journal of Functional Programming},
  volume       = {7},
  number       = {5},
  pages        = {549--554},
  year         = {1997},
  url          = {https://doi.org/10.1017/s0956796897002864}
}

@unpublished{McBride,
  author = {Conor McBride},
  title  = {The Derivative of a Regular Type is its Type of One-Hole Contexts},
  note   = {Unpublished extended abstract}
}