Andreas Abel (2009):
Implementing a normalizer using sized heterogeneous types.
J. Funct. Program. 19(3-4),
pp. 287–310,
doi:10.1017/S0956796809007266.
Andreas Abel & Nicolai Kraus (2011):
A Lambda Term Representation Inspired by Linear Ordered Logic.
In: Herman Geuvers & Gopalan Nadathur: Proceedings Sixth International Workshop on Logical Frameworks and Meta-languages: Theory and Practice, LFMTP 2011, Nijmegen, The Netherlands, August 26, 2011.,
EPTCS 71,
pp. 1–13,
doi:10.4204/EPTCS.71.1.
Guillaume Allais, James Chapman, Conor McBride & James McKinna (2017):
Type-and-scope safe programs and their proofs.
In: Yves Bertot & Viktor Vafeiadis: Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, Paris, France, January 16-17, 2017.
ACM,
pp. 195–207,
doi:10.1145/3018610.3018613.
Thorsten Altenkirch, Martin Hofmann & Thomas Streicher (1995):
Categorical Reconstruction of a Reduction Free Normalization Proof.
In: David H. Pitt, David E. Rydeheard & Peter T. Johnstone: Category Theory and Computer Science, 6th International Conference, CTCS '95, Cambridge, UK, August 7-11, 1995, Proceedings,
Lecture Notes in Computer Science 953.
Springer,
pp. 182–199,
doi:10.1007/3-540-60164-3_27.
Thorsten Altenkirch & Bernhard Reus (1999):
Monadic presentations of lambda-terms using generalized inductive types.
In: Computer Science Logic 1999,
pp. 453–468,
doi:10.1007/3-540-48168-0_32.
Francoise Bellegarde & James Hook (1995):
Substitution: A formal methods case study using monads and transformations.
Science of Computer Programming,
doi:10.1016/0167-6423(94)00022-0.
Nick Benton, Chung-Kil Hur, Andrew Kennedy & Conor McBride (2012):
Strongly Typed Term Representations in Coq.
J. Autom. Reasoning 49(2),
pp. 141–159,
doi:10.1007/s10817-011-9219-0.
Richard Bird & Ross Paterson (1999):
de Bruijn notation as a nested datatype.
Journal of Functional Programming 9(1),
pp. 77–92,
doi:10.1017/S0956796899003366.
Nicolas G. de Bruijn (1972):
Lambda Calculus notation with nameless dummies: a tool for automatic formula manipulation.
Indagationes Mathematicæ 34,
pp. 381–392,
doi:10.1016/1385-7258(72)90034-0.
Lucas Dixon, Peter Hancock & Conor McBride (2007):
Why walk when you can take the tube?.
Available at http://strictlypositive.org/Holes.pdf.
Unpublished draft..
Jeremy Gibbons (2017):
APLicative Programming with Naperian Functors.
In: Hongseok Yang: 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,
Lecture Notes in Computer Science 10201.
Springer,
pp. 556–583,
doi:10.1007/978-3-662-54434-1_21.
Healfdene Goguen & James McKinna (1997):
Candidates for Substitution.
Technical Report ECS-LFCS-97-358.
University of Edinburgh.
Robert Harper, Furio Honsell & Gordon D. Plotkin (1993):
A Framework for Defining Logics.
J. ACM 40(1),
pp. 143–184,
doi:10.1145/138027.138060.
Dimitri Hendriks & Vincent van Oostrom (2003):
adbmal.
In: Franz Baader: Automated Deduction - CADE-19, 19th International Conference on Automated Deduction Miami Beach, FL, USA, July 28 - August 2, 2003, Proceedings,
Lecture Notes in Computer Science 2741.
Springer,
pp. 136–150,
doi:10.1007/978-3-540-45085-6_11.
Chantal Keller & Thorsten Altenkirch (2010):
Hereditary Substitutions for Simple Types, Formalized.
In: Venanzio Capretta & James Chapman: Proceedings of the 3rd ACM SIGPLAN Workshop on Mathematically Structured Functional Programming, MSFP@ICFP 2010, Baltimore, MD, USA, September 25, 2010..
ACM,
pp. 3–10,
doi:10.1145/1863597.1863601.
Richard Kennaway & M. Ronan Sleep (1987):
Variable Abstraction in O(n log n) Space.
Inf. Process. Lett. 24(5),
pp. 343–349,
doi:10.1016/0020-0190(87)90161-X.
Conor McBride (2000):
Dependently typed functional programs and their proofs.
University of Edinburgh, UK.
Conor McBride (2003):
First-order unification by structural recursion.
J. Funct. Program. 13(6),
pp. 1061–1075,
doi:10.1017/S0956796803004957.
Spike Milligan (1972):
The Last Goon Show of All.
BBC Radio 4.
Ulf Norell (2008):
Dependently Typed Programming in Agda.
In: Pieter W. M. Koopman, Rinus Plasmeijer & S. Doaitse Swierstra: Advanced Functional Programming, 6th International School, AFP 2008, Heijen, The Netherlands, May 2008, Revised Lectures,
Lecture Notes in Computer Science 5832.
Springer,
pp. 230–266,
doi:10.1007/978-3-642-04652-0_5.
Masahiko Sato, Randy Pollack, Helmut Schwichtenberg & Takafumi Sakurai (2013):
Viewing λ-terms through Maps.
Indagationes Mathematicæ 24(4),
doi:10.1016/j.indag.2013.08.003.
François-Régis Sinot, Maribel Fernández & Ian Mackie (2003):
Efficient Reductions with Director Strings.
In: Robert Nieuwenhuis: Rewriting Techniques and Applications, 14th International Conference, RTA 2003, Valencia, Spain, June 9-11, 2003, Proceedings,
Lecture Notes in Computer Science 2706.
Springer,
pp. 46–60,
doi:10.1007/3-540-44881-0_5.
Kevin Watkins, Iliano Cervesato, Frank Pfenning & David Walker (2003):
A Concurrent Logical Framework: The Propositional Fragment.
In: Stefano Berardi, Mario Coppo & Ferruccio Damiani: Types for Proofs and Programs, International Workshop, TYPES 2003, Torino, Italy, April 30 - May 4, 2003, Revised Selected Papers,
Lecture Notes in Computer Science 3085.
Springer,
pp. 355–377,
doi:10.1007/978-3-540-24849-1_23.
eptcs@eptcs.org