@book(bar:84,
 author       = {Hendrik Barendregt},
 year         = {1984},
 title        = {The Lambda Calculus Its Syntax and Semantics},
 edition      = {revised},
 series       = {Studies in Logic and the Foundations of Mathematics},
 volume       = {103},
 publisher    = {North Holland},
 doi          = {10.2307/2274112},
)
@misc(ernius:lib,
 author       = {Ernesto Copello},
 title        = {Agda Library for {F}ormal metatheory of the Lambda Calculus using {S}toughton's substitution},
 howpublished = {Available at https://github.com/ernius/formalmetatheory-stoughton},
)
@article(COPELLO2016,
 author       = {Ernesto Copello and Nora Szasz and \IeC{\'A}lvaro Tasistro},
 year         = {2017},
 title        = {Formal metatheory of the Lambda Calculus using {S}toughton's substitution},
 journal      = {Theoretical Computer Science},
 volume       = {685},
 pages        = {65 -- 82},
 doi          = {10.1016/j.tcs.2016.08.025},
)
@mastersthesis(copes:thesis,
 author       = {Martin Copes},
 year         = {2018},
 title        = {A machine checked proof of the Standardization Theorem in Lambda Calculus using multiple substitution},
 school       = {Universidad ORT Uruguay},
)
@book(curry,
 author       = {H. B. Curry and R. Feys},
 year         = {1958},
 title        = {Combinatory Logic, Volume I},
 publisher    = {North-Holland},
 note         = {Second printing 1968},
)
@misc(standard:coq,
 author       = {Johannes Emerich and Vy\IeC{\v s}niauskas, Ignas},
 year         = {2014},
 title        = {Coq formalisation of Postponement and Standardization theorems in the untyped lambda-calculus},
 howpublished = {Available at https://github.com/knuton/la-girafe-sportive},
 note         = {ILLC, Universiteit van Amsterdam},
)
@article(guidi:standard,
 author       = {Ferruccio Guidi},
 year         = {2012},
 title        = {Standardization and Confluence in Pure Lambda-Calculus Formalized for the {M}atita Theorem Prover},
 journal      = {Journal of Formalized Reasoning},
 volume       = {5},
 number       = {1},
 pages        = {1--25},
 doi          = {10.6092/issn.1972-5787/3392},
 url          = {https://jfr.unibo.it/article/view/3392},
)
@techreport(kashima,
 author       = {R. Kashima},
 year         = {2000},
 title        = {A Proof of the Standardization Theorem in Lambda-Calculus},
 type         = {Technical Report},
 institution  = {Tokyo Institute of Technology. Department of Information Sciences},
 url          = {http://www.is.titech.ac.jp/~kashima/pub/C-145.pdf},
)
@article(McKinna1999,
 author       = {James McKinna and Robert Pollack},
 year         = {1999},
 title        = {Some Lambda Calculus and Type Theory Formalized},
 journal      = {Journal of Automated Reasoning},
 volume       = {23},
 number       = {3},
 pages        = {373--409},
 doi          = {10.1023/A:1006294005493},
)
@phdthesis(agda,
 author       = {Ulf Norell},
 year         = {2007},
 title        = {{Towards a Practical Programming Language Based on Dependent Type Theory}},
 school       = {Department of Computer Science and Engineering, Chalmers University of Technology},
)
@article(stoughton,
 author       = {A. Stoughton},
 year         = {1988},
 title        = {Substitution Revisited},
 journal      = {Theoretical Computer Science},
 volume       = {59},
 pages        = {317--325},
 url          = {http://dx.doi.org/10.1016/0304-3975(88)90149-1},
)
@article(takahashi,
 author       = {M. Takahashi},
 year         = {1995},
 title        = {{Parallel Reductions in $\lambda$-Calculus}},
 journal      = {Information and Computation},
 volume       = {118},
 number       = {1},
 pages        = {120 -- 127},
 doi          = {10.1006/inco.1995.1057},
 url          = {http://www.sciencedirect.com/science/article/pii/S0890540185710577},
)
@article(vestergaard,
 author       = {Ren{\'e} Vestergaard and James Brotherston},
 year         = {2003},
 title        = {{A Formalised First-Order Confluence Proof for the $\lambda$-Calculus using One-Sorted Variable Names}},
 journal      = {Information and Computation},
 volume       = {183},
 number       = {2},
 pages        = {212--244},
 doi          = {10.1016/S0890-5401(03)00023-3},
)