@article(DBLP:journals/jfp/Abel09,
 author       = {Andreas Abel},
 year         = {2009},
 title        = {Implementing a normalizer using sized heterogeneous types},
 journal      = {J. Funct. Program.},
 volume       = {19},
 number       = {3-4},
 pages        = {287--310},
 doi          = {10.1017/S0956796809007266},
)
@inproceedings(DBLP:journals/corr/abs-1111-0085,
 author       = {Andreas Abel and Nicolai Kraus},
 year         = {2011},
 title        = {A Lambda Term Representation Inspired by Linear Ordered Logic},
 editor       = {Herman Geuvers and Gopalan Nadathur},
 booktitle    = {Proceedings Sixth International Workshop on Logical Frameworks and Meta-languages: Theory and Practice, {LFMTP} 2011, Nijmegen, The Netherlands, August 26, 2011.},
 series       = {{EPTCS}},
 volume       = {71},
 pages        = {1--13},
 doi          = {10.4204/EPTCS.71.1},
)
@inproceedings(DBLP:conf/cpp/Allais0MM17,
 author       = {Guillaume Allais and James Chapman and Conor McBride and James McKinna},
 year         = {2017},
 title        = {Type-and-scope safe programs and their proofs},
 editor       = {Yves Bertot and Viktor Vafeiadis},
 booktitle    = {Proceedings of the 6th {ACM} {SIGPLAN} Conference on Certified Programs and Proofs, {CPP} 2017, Paris, France, January 16-17, 2017},
 publisher    = {{ACM}},
 pages        = {195--207},
 doi          = {10.1145/3018610.3018613},
)
@inproceedings(DBLP:conf/ctcs/AltenkirchHS95,
 author       = {Thorsten Altenkirch and Martin Hofmann and Thomas Streicher},
 year         = {1995},
 title        = {Categorical Reconstruction of a Reduction Free Normalization Proof},
 editor       = {David H. Pitt and David E. Rydeheard and Peter T. Johnstone},
 booktitle    = {Category Theory and Computer Science, 6th International Conference, {CTCS} '95, Cambridge, UK, August 7-11, 1995, Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {953},
 publisher    = {Springer},
 pages        = {182--199},
 doi          = {10.1007/3-540-60164-3\_27},
)
@inproceedings(altenkirch.reus:monads.lambda,
 author       = {Thorsten Altenkirch and Bernhard Reus},
 year         = {1999},
 title        = {Monadic presentations of lambda-terms using generalized inductive types},
 booktitle    = {{C}omputer {S}cience {L}ogic 1999},
 pages        = {453--468},
 doi          = {10.1007/3-540-48168-0\_32},
)
@article(bellegarde.hook:substitution.monad,
 author       = {Francoise Bellegarde and James Hook},
 year         = {1995},
 title        = {Substitution: {A} formal methods case study using monads and transformations},
 journal      = {{S}cience of {C}omputer {P}rogramming},
 doi          = {10.1016/0167-6423(94)00022-0},
)
@article(DBLP:journals/jar/BentonHKM12,
 author       = {Nick Benton and Chung{-}Kil Hur and Andrew Kennedy and Conor McBride},
 year         = {2012},
 title        = {Strongly Typed Term Representations in Coq},
 journal      = {J. Autom. Reasoning},
 volume       = {49},
 number       = {2},
 pages        = {141--159},
 doi          = {10.1007/s10817-011-9219-0},
)
@article(bird.paterson:debruijn.nested,
 author       = {Richard Bird and Ross Paterson},
 year         = {1999},
 title        = {de {B}ruijn notation as a nested datatype},
 journal      = {Journal of {F}unctional {P}rogramming},
 volume       = {9},
 number       = {1},
 pages        = {77--92},
 doi          = {10.1017/S0956796899003366},
)
@article(deBruijn:dummies,
 author       = {Nicolas G. de Bruijn},
 year         = {1972},
 title        = {{Lambda Calculus notation with nameless dummies: a tool for automatic formula manipulation}},
 journal      = {Indagationes Mathematic{\ae}},
 volume       = {34},
 pages        = {381--392},
 doi          = {10.1016/1385-7258(72)90034-0},
)
@unpublished(conor:tube,
 author       = {Lucas Dixon and Peter Hancock and Conor McBride},
 year         = {2007},
 title        = {Why walk when you can take the tube?},
 url          = {http://strictlypositive.org/Holes.pdf},
 note         = {Unpublished draft.},
)
@inproceedings(DBLP:conf/esop/Gibbons17,
 author       = {Jeremy Gibbons},
 year         = {2017},
 title        = {APLicative Programming with Naperian Functors},
 editor       = {Hongseok Yang},
 booktitle    = {Programming Languages and Systems - 26th European Symposium on Programming, {ESOP} 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, {ETAPS} 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {10201},
 publisher    = {Springer},
 pages        = {556--583},
 doi          = {10.1007/978-3-662-54434-1\_21},
)
@techreport(goguenmckinna,
 author       = {Healfdene Goguen and James McKinna},
 year         = {1997},
 title        = {Candidates for Substitution},
 type         = {Technical Report},
 number       = {ECS-LFCS-97-358},
 institution  = {University of Edinburgh},
)
@article(DBLP:journals/jacm/HarperHP93,
 author       = {Robert Harper and Furio Honsell and Gordon D. Plotkin},
 year         = {1993},
 title        = {A Framework for Defining Logics},
 journal      = {J. {ACM}},
 volume       = {40},
 number       = {1},
 pages        = {143--184},
 doi          = {10.1145/138027.138060},
)
@inproceedings(DBLP:conf/cade/HendriksO03,
 author       = {Dimitri Hendriks and Vincent van Oostrom},
 year         = {2003},
 title        = {adbmal},
 editor       = {Franz Baader},
 booktitle    = {Automated Deduction - CADE-19, 19th International Conference on Automated Deduction Miami Beach, FL, USA, July 28 - August 2, 2003, Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {2741},
 publisher    = {Springer},
 pages        = {136--150},
 doi          = {10.1007/978-3-540-45085-6\_11},
)
@inproceedings(DBLP:conf/icfp/KellerA10,
 author       = {Chantal Keller and Thorsten Altenkirch},
 year         = {2010},
 title        = {Hereditary Substitutions for Simple Types, Formalized},
 editor       = {Venanzio Capretta and James Chapman},
 booktitle    = {Proceedings of the 3rd {ACM} {SIGPLAN} Workshop on Mathematically Structured Functional Programming, MSFP@ICFP 2010, Baltimore, MD, USA, September 25, 2010.},
 publisher    = {{ACM}},
 pages        = {3--10},
 doi          = {10.1145/1863597.1863601},
)
@article(DBLP:journals/ipl/KennawayS87,
 author       = {Richard Kennaway and M. Ronan Sleep},
 year         = {1987},
 title        = {Variable Abstraction in O(n log n) Space},
 journal      = {Inf. Process. Lett.},
 volume       = {24},
 number       = {5},
 pages        = {343--349},
 doi          = {10.1016/0020-0190(87)90161-X},
)
@phdthesis(DBLP:phd/ethos/McBride00,
 author       = {Conor McBride},
 year         = {2000},
 title        = {Dependently typed functional programs and their proofs},
 school       = {University of Edinburgh, {UK}},
)
@article(DBLP:journals/jfp/McBride03,
 author       = {Conor McBride},
 year         = {2003},
 title        = {First-order unification by structural recursion},
 journal      = {J. Funct. Program.},
 volume       = {13},
 number       = {6},
 pages        = {1061--1075},
 doi          = {10.1017/S0956796803004957},
)
@misc(eccles,
 author       = {Spike Milligan},
 year         = {1972},
 title        = {The Last Goon Show of All},
 howpublished = {BBC Radio 4},
)
@inproceedings(DBLP:conf/afp/Norell08,
 author       = {Ulf Norell},
 year         = {2008},
 title        = {Dependently Typed Programming in Agda},
 editor       = {Pieter W. M. Koopman and Rinus Plasmeijer and S. Doaitse Swierstra},
 booktitle    = {Advanced Functional Programming, 6th International School, {AFP} 2008, Heijen, The Netherlands, May 2008, Revised Lectures},
 series       = {Lecture Notes in Computer Science},
 volume       = {5832},
 publisher    = {Springer},
 pages        = {230--266},
 doi          = {10.1007/978-3-642-04652-0\_5},
)
@article(spss:lambda.maps,
 author       = {Masahiko Sato and Randy Pollack and Helmut Schwichtenberg and Takafumi Sakurai},
 year         = {2013},
 title        = {Viewing $\lambda$-terms through {M}aps},
 journal      = {Indagationes Mathematic{\ae}},
 volume       = {24},
 number       = {4},
 doi          = {10.1016/j.indag.2013.08.003},
)
@inproceedings(DBLP:conf/rta/SinotFM03,
 author       = {Fran{\c{c}}ois{-}R{\'{e}}gis Sinot and Maribel Fern{\'{a}}ndez and Ian Mackie},
 year         = {2003},
 title        = {Efficient Reductions with Director Strings},
 editor       = {Robert Nieuwenhuis},
 booktitle    = {Rewriting Techniques and Applications, 14th International Conference, {RTA} 2003, Valencia, Spain, June 9-11, 2003, Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {2706},
 publisher    = {Springer},
 pages        = {46--60},
 doi          = {10.1007/3-540-44881-0\_5},
)
@inproceedings(DBLP:conf/types/WatkinsCPW03,
 author       = {Kevin Watkins and Iliano Cervesato and Frank Pfenning and David Walker},
 year         = {2003},
 title        = {A Concurrent Logical Framework: The Propositional Fragment},
 editor       = {Stefano Berardi and Mario Coppo and Ferruccio Damiani},
 booktitle    = {Types for Proofs and Programs, International Workshop, {TYPES} 2003, Torino, Italy, April 30 - May 4, 2003, Revised Selected Papers},
 series       = {Lecture Notes in Computer Science},
 volume       = {3085},
 publisher    = {Springer},
 pages        = {355--377},
 doi          = {10.1007/978-3-540-24849-1\_23},
)