@inproceedings(abelTwelf,
 author       = {Andreas Abel},
 year         = {2008},
 title        = {Normalization for the Simply-Typed Lambda-Calculus in Twelf},
 editor       = {Carsten Schürmann},
 booktitle    = {Proc. LFM '04},
 series       = {ENTCS},
 volume       = {199},
 publisher    = {Elsevier},
 pages        = {3--16},
 doi          = {10.1016/j.entcs.2007.11.009},
)
@article(poplmark2,
 author       = {Andreas Abel and Guillaume Allais and Aliya Hameer and Brigitte Pientka and Alberto Momigliano and Steven Schäfer and Kathrin Stark},
 year         = {2019},
 title        = {POPLMark reloaded: Mechanizing proofs by logical relations},
 journal      = {Journal of Functional Programming},
 volume       = {29},
 doi          = {10.1017/S0956796819000170},
)
@phdthesis(alti:phd93,
 author       = {Thorsten Altenkirch},
 year         = {1993},
 title        = {Constructions, Inductive Types and Strong Normalization},
 school       = {University of Edinburgh},
 url          = {https://www.cs.nott.ac.uk/~psztxa/publ/phd93.pdf},
)
@book(barendregt,
 author       = {Hendrik P. Barendregt},
 year         = {1985},
 title        = {The lambda calculus - its syntax and semantics},
 series       = {Studies in logic and the foundations of mathematics},
 volume       = {103},
 publisher    = {North-Holland},
)
@article(debruijn1972,
 author       = {Nicolaas Govert de Bruijn},
 year         = {1972},
 title        = {Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem},
 journal      = {Indagationes Mathematicae},
 volume       = {75},
 number       = {5},
 pages        = {381--392},
 doi          = {10.1016/1385-7258(72)90034-0},
)
@article(locallynameless,
 author       = {Arthur Charguéraud},
 year         = {2012},
 title        = {The Locally Nameless Representation},
 journal      = {Journal of Automated Reasoning},
 volume       = {49},
 number       = {3},
 pages        = {363--408},
 doi          = {10.1007/s10817-011-9225-2},
)
@article(church36,
 author       = {Alonzo Church},
 year         = {1936},
 title        = {An Unsolvable Problem of Elementary Number Theory},
 journal      = {American Journal of Mathematics},
 volume       = {58},
 number       = {2},
 pages        = {345--363},
 doi          = {10.2307/2371045},
)
@article(copello2016,
 author       = {Ernesto Copello and Nora Szasz and Álvaro Tasistro},
 year         = {2017},
 title        = {Formal metatheory of the Lambda calculus using Stoughton's substitution},
 journal      = {Theoretical Computer Science},
 volume       = {685},
 pages        = {65--82},
 doi          = {10.1016/j.tcs.2016.08.025},
)
@inproceedings(copes2018,
 author       = {Martín Copes and Nora Szasz and Álvaro Tasistro},
 year         = {2018},
 title        = {Formalization in Constructive Type Theory of the Standardization Theorem for the Lambda Calculus using Multiple Substitution},
 editor       = {Frédéric Blanqui and Giselle Reis},
 booktitle    = {Proc. LFMTP '18},
 series       = {EPTCS},
 volume       = {274},
 publisher    = {Open Publishing Association},
 pages        = {27–41},
 doi          = {10.4204/eptcs.274.3},
)
@inproceedings(donnelly2007,
 author       = {Kevin Donnelly and Hongwei Xi},
 year         = {2007},
 title        = {A Formalization of Strong Normalization for Simply-Typed Lambda-Calculus and System F},
 editor       = {Alberto Momigliano and Brigitte Pientka},
 booktitle    = {Proc. LFMTP '06},
 series       = {ENTCS},
 volume       = {174},
 publisher    = {Elsevier},
 pages        = {109--125},
 doi          = {10.1016/j.entcs.2007.01.021},
)
@book(girard1989,
 author       = {Jean-Yves Girard and Paul Taylor and Yves Lafont},
 year         = {1989},
 title        = {{Proofs and Types}},
 publisher    = {Cambridge University Press},
)
@article(godel1958,
 author       = {V. Kurt G\"{o}del},
 year         = {1958},
 title        = {\"{U}ber Eine Bisher Noch Nicht Ben\"{u}tzte Erweiterung des Finiten Standpunktes},
 journal      = {Dialectica},
 volume       = {12},
 number       = {4},
 pages        = {280--287},
 doi          = {10.1111/j.1746-8361.1958.tb01464.x},
)
@book(hindley,
 author       = {J. Roger Hindley and Jonathan P. Seldin},
 year         = {2008},
 title        = {Lambda-Calculus and Combinators: An Introduction},
 edition      = {second},
 publisher    = {Cambridge University Press},
 doi          = {10.1017/CBO9780511809835},
)
@article(joachimski2003,
 author       = {Felix Joachimski and Ralph Matthes},
 year         = {2003},
 title        = {Short proofs of normalization for the simply-typed $\lambda$-calculus, permutative conversions and Gödel's T},
 journal      = {Archive for Mathematical Logic},
 volume       = {42},
 pages        = {59--87},
 doi          = {10.1007/s00153-002-0156-9},
)
@manual(coq,
 author       = {\mbox{The Coq development team}},
 year         = {{2004}},
 title        = {{The Coq proof assistant reference manual}},
 url          = {http://coq.inria.fr},
)
@phdthesis(agda,
 author       = {Ulf Norell},
 year         = {2007},
 title        = {Towards a practical programming language based on dependent type theory},
 school       = {Chalmers University of Technology},
 url          = {https://www.cse.chalmers.se/~ulfn/papers/thesis.pdf},
)
@inproceedings(hoas,
 author       = {Frank Pfenning and Conal Elliott},
 year         = {1988},
 title        = {Higher-Order Abstract Syntax},
 editor       = {Richard L. Wexelblat},
 booktitle    = {Proc. PLDI '88},
 publisher    = {Association for Computing Machinery},
 pages        = {199–208},
 doi          = {10.1145/53990.54010},
)
@phdthesis(lego,
 author       = {Robert Pollack},
 year         = {1994},
 title        = {The Theory of LEGO},
 school       = {University of Edinburgh},
 url          = {https://era.ed.ac.uk/handle/1842/504},
)
@article(stoughton88,
 author       = {Allen Stoughton},
 year         = {1988},
 title        = {Substitution revisited},
 journal      = {Theoretical Computer Science},
 volume       = {59},
 number       = {3},
 pages        = {317--325},
 doi          = {10.1016/0304-3975(88)90149-1},
)
@article(tait,
 author       = {William W. Tait},
 year         = {1967},
 title        = {Intensional Interpretations of Functionals of Finite Type I},
 journal      = {The Journal of Symbolic Logic},
 volume       = {32},
 number       = {2},
 pages        = {198--212},
 doi          = {10.2307/2271658},
)
@inproceedings(tasistro2015,
 author       = {Álvaro Tasistro and Ernesto Copello and Nora Szasz},
 year         = {2015},
 title        = {Formalisation in Constructive Type Theory of Stoughton's Substitution for the Lambda Calculus},
 editor       = {Ayala-Rincón, Mauricio and Ian Mackie},
 booktitle    = {Proc. LSFA '14},
 series       = {ENTCS},
 volume       = {312},
 publisher    = {Elsevier},
 pages        = {215--230},
 doi          = {10.1016/j.entcs.2015.04.013},
)
@misc(agdastdlib,
 author       = {The Agda development team},
 year         = {2011},
 title        = {The Agda standard library},
 url          = {https://github.com/agda/agda-stdlib},
)
@article(urban2004,
 author       = {Christian Urban and Andrew M. Pitts and Murdoch J. Gabbay},
 year         = {2004},
 title        = {Nominal unification},
 journal      = {Theoretical Computer Science},
 volume       = {323},
 number       = {1},
 pages        = {473--497},
 doi          = {10.1016/j.tcs.2004.06.016},
)
@inproceedings(urciuoli2020,
 author       = {Sebasti\'an Urciuoli and \'Alvaro Tasistro and Nora Szasz},
 year         = {2020},
 title        = {Strong Normalization for the Simply-Typed Lambda Calculus in Constructive Type Theory Using Agda},
 editor       = {Cláudia Nalon and Giselle Reis},
 booktitle    = {Proc. LSFA '20},
 series       = {ENTCS},
 volume       = {351},
 publisher    = {Elsevier},
 pages        = {187--203},
 doi          = {10.1016/j.entcs.2020.08.010},
)
@inproceedings(ats,
 author       = {Hongwei Xi},
 year         = {2003},
 title        = {Applied type system},
 editor       = {Stefano Berardi and Mario Coppo and Ferruccio Damiani},
 booktitle    = {Proc. TYPES '03},
 series       = {LNCS},
 volume       = {3085},
 publisher    = {Springer},
 pages        = {394--408},
 doi          = {10.1007/978-3-540-24849-1_25},
)