@article(abadiCardelliCurienLevy:jfp91,
 author       = "Mart\'{\i }n Abadi and Luca Cardelli and Pierre-Louis Curien and Jean-Jacques L{\'e}vy",
 year         = "1991",
 title        = "Explicit Substitutions",
 journal      = "Journal of Functional Programming",
 volume       = "1",
 number       = "4",
 pages        = "375--416",
 doi          = "10.1017/S0956796800000186",
)
@article(adams:jfp93,
 author       = "Stephen Adams",
 year         = "1993",
 title        = "Efficient Sets - A Balancing Act",
 journal      = "Journal of Functional Programming",
 volume       = "3",
 number       = "4",
 pages        = "553--561",
 doi          = "10.1017/S0956796800000885",
)
@article(appel:toplas10,
 author       = "Amal Ahmed and Andrew W. Appel and Christopher D. Richards and Kedar N. Swadi and Gang Tan and Daniel C. Wang",
 year         = "2010",
 title        = "Semantic foundations for typed assembly languages",
 journal      = "ACM Transactions on Programming Languages and Systems",
 volume       = "32",
 number       = "3",
 doi          = "10.1145/1709093.1709094",
)
@book(barendregt:lambdacalculus,
 author       = "Henk Barendregt",
 year         = "1984",
 title        = "The Lambda Calculus: Its Syntax and Semantics",
 publisher    = "North Holland",
 address      = "Amsterdam",
)
@inproceedings(bentonBiermanDePaivaHyland:tlca93,
 author       = "Nick Benton and Gavin M. Bierman and Valeria de Paiva and Martin Hyland",
 year         = "1993",
 title        = "A Term Calculus for Intuitionistic Linear Logic",
 editor       = "Marc Bezem and Jan Friso Groote",
 booktitle    = "Typed Lambda Calculi and Applications, International Conference on Typed Lambda Calculi and Applications, TLCA '93, Utrecht, The Netherlands, March 16-18, 1993, Proceedings",
 series       = "Lecture Notes in Computer Science",
 volume       = "664",
 publisher    = "Springer-Verlag",
 pages        = "75--90",
 doi          = "10.1007/BFb0037099",
)
@inproceedings(boespflug:padl10,
 author       = "Mathieu Boespflug",
 year         = "2010",
 title        = "Conversion by Evaluation",
 editor       = "Manuel Carro and Ricardo Pe{\~n}a",
 booktitle    = "Practical Aspects of Declarative Languages, 12th International Symposium, PADL 2010, Madrid, Spain, January 18-19, 2010. Proceedings",
 series       = "Lecture Notes in Computer Science",
 volume       = "5937",
 publisher    = "Springer-Verlag",
 pages        = "58--72",
 doi          = "10.1007/978-3-642-11503-5\_7",
)
@article(deBruijn:nameless,
 author       = "N. G. de Bruijn",
 year         = "1972",
 title        = "Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the {C}hurch-{R}osser theorem",
 journal      = "Indagationes Mathematicae",
 volume       = "34",
 pages        = "381--392",
 doi          = "10.1016/1385-7258(72)90034-0",
)
@article(cervesatoPfenning:spineCalculus,
 author       = "Iliano Cervesato and Frank Pfenning",
 year         = "2003",
 title        = "A Linear Spine Calculus",
 journal      = "Journal of Logic and Computation",
 volume       = "13",
 number       = "5",
 pages        = "639--688",
 doi          = "10.1093/logcom/13.5.639",
)
@inproceedings(coquand:type,
 author       = "Thierry Coquand",
 year         = "1996",
 title        = "An Algorithm for Type-Checking Dependent Types",
 booktitle    = "Mathematics of Program Construction. Selected Papers from the Third International Conference on the Mathematics of Program Construction (July 17--21, 1995, Kloster Irsee, Germany)",
 series       = "Science of Computer Programming",
 volume       = "26",
 publisher    = "Elsevier",
 pages        = "167--177",
 doi          = "10.1016/0167-6423(95)00021-6",
)
@article(fernandezMackieSinot:aaecc05,
 author       = "Maribel Fern{\'a}ndez and Ian Mackie and Fran\c {c}ois-R{\'e}gis Sinot",
 year         = "2005",
 title        = "Lambda-Calculus with Director Strings",
 journal      = "Applicable Algebra in Engineering, Communication and Computing",
 volume       = "15",
 number       = "6",
 pages        = "393--437",
 doi          = "10.1007/s00200-005-0169-9",
)
@inproceedings(fluetWeeks:icfp01,
 author       = "Matthew Fluet and Stephen Weeks",
 year         = "2001",
 title        = "Contification Using Dominators",
 booktitle    = "Proceedings of the sixth ACM SIGPLAN International Conference on Functional Programming (ICFP 2001)",
 pages        = "2--13",
 doi          = "10.1145/507635.507639",
)
@article(girard:linear,
 author       = "Jean-Yves Girard",
 year         = "1987",
 title        = "Linear Logic",
 journal      = "Theoretical Computer Science",
 volume       = "50",
 pages        = "1--102",
 doi          = "10.1016/0304-3975(87)90045-4",
)
@inproceedings(gregoireLeroy:icfp02,
 author       = "Benjamin Gr{\'e}goire and Xavier Leroy",
 year         = "2002",
 title        = "A compiled implementation of strong reduction",
 booktitle    = "Proceedings of the seventh ACM SIGPLAN International Conference on Functional Programming (ICFP '02), Pittsburgh, Pennsylvania, USA, October 4-6, 2002",
 series       = "SIGPLAN Notices",
 volume       = "37",
 publisher    = "ACM Press",
 pages        = "235--246",
 doi          = "10.1145/581478.581501",
)
@manual(inria:coq83,
 author       = "INRIA",
 year         = "2010",
 title        = "The Coq Proof Assistant Reference Manual",
 edition      = "version 8.3",
 organization = "INRIA",
 url          = "http://coq.inria.fr/",
)
@article(kesnerLengrand:infcomp07,
 author       = "Delia Kesner and St{\'e}phane Lengrand",
 year         = "2007",
 title        = "Resource operators for lambda-calculus",
 journal      = "Information and Computation",
 volume       = "205",
 number       = "4",
 pages        = "419--473",
 doi          = "10.1016/j.ic.2006.08.008",
)
@mastersthesis(kraus:bachelor,
 author       = "Nicolai Kraus",
 year         = "2011",
 title        = "A Lambda Term Representation Based on Linear Ordered Logic",
 type         = "Bachelor's thesis",
 school       = "Department of Computer Science, Ludwig-Maximilians-University Munich",
)
@article(liangNadathurQi:jar05,
 author       = "Chuck Liang and Gopalan Nadathur and Xiaochu Qi",
 year         = "2005",
 title        = "Choices in representation and reduction strategies for lambda terms in intensional contexts",
 journal      = "Journal of Automated Reasoning",
 volume       = "33",
 number       = "2",
 pages        = "89--132",
 doi          = "10.1007/s10817-004-6885-1",
)
@article(mcBrideMcKinna:view,
 author       = "Conor McBride and James McKinna",
 year         = "2004",
 title        = "The view from the left",
 journal      = "Journal of Functional Programming",
 volume       = "14",
 number       = "1",
 pages        = "69--111",
 doi          = "10.1017/S0956796803004829",
)
@article(nadathur:jflp99,
 author       = "Gopalan Nadathur",
 year         = "1999",
 title        = "A Fine-Grained Notation for Lambda Terms and Its Use in Intensional Operations",
 journal      = "Journal of Functional and Logic Programming",
 volume       = "1999",
 number       = "2",
 url          = "http://danae.uni-muenster.de/lehre/kuchen/JFLP/articles/1999/A99-02/A99-02.html",
)
@inproceedings(nadathur:flops01,
 author       = "Gopalan Nadathur",
 year         = "2001",
 title        = "The Metalanguage lambda-Prolog and Its Implementation",
 booktitle    = "Functional and Logic Programming, 10th International Symposium, FLOPS 2010, Sendai, Japan, April 19-21, 2010. Proceedings",
 pages        = "1--20",
 doi          = "10.1007/3-540-44716-4\_1",
)
@phdthesis(norell:PhD,
 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",
 address      = "G\"{o}teborg, Sweden",
)
@inproceedings(carsten:twelf,
 author       = "Frank Pfenning and Carsten Sch{\"u}rmann",
 year         = "1999",
 title        = "System Description: Twelf - A Meta-Logical Framework for Deductive Systems",
 editor       = "Harald Ganzinger",
 booktitle    = "Automated Deduction - CADE-16, 16th International Conference on Automated Deduction, Trento, Italy, July 7-10, 1999, Proceedings",
 series       = "Lecture Notes in Computer Science",
 volume       = "1632",
 publisher    = "Springer-Verlag",
 pages        = "202--206",
 doi          = "10.1007/3-540-48660-7\_14",
)
@inproceedings(polakowPfenning:tlca99,
 author       = "Jeff Polakow and Frank Pfenning",
 year         = "1999",
 title        = "Natural Deduction for Intuitionistic Non-communicative Linear Logic",
 editor       = "Jean-Yves Girard",
 booktitle    = "Typed Lambda Calculi and Applications, 4th International Conference, TLCA'99, L'Aquila, Italy, April 7-9, 1999, Proceedings",
 series       = "Lecture Notes in Computer Science",
 volume       = "1581",
 publisher    = "Springer-Verlag",
 pages        = "295--309",
 doi          = "10.1007/3-540-48959-2\_21",
)
@article(sinot:jlc05,
 author       = "Fran\c {c}ois-R{\'e}gis Sinot",
 year         = "2005",
 title        = "Director Strings Revisited: A Generic Approach to the Efficient Representation of Free Variables in Higher-order Rewriting",
 journal      = "Journal of Logic and Computation",
 volume       = "15",
 number       = "2",
 pages        = "201--218",
 doi          = "10.1093/logcom/exi010",
)
@techreport(watkins:concurrentlftr,
 author       = "Kevin Watkins and Iliano Cervesato and Frank Pfenning and David Walker",
 year         = "2003",
 title        = "A concurrent logical framework {I}: Judgements and properties",
 type         = "Technical Report",
 institution  = "School of Computer Science, Carnegie Mellon University, Pittsburgh",
)