nonauto-lfmtp11.bib

@STRING{aaecc   = "Applicable Algebra in Engineering, Communication and
                  Computing" }
@STRING{acm     = "ACM Press" }
@STRING{cade99  = "Automated Deduction - CADE-16, 16th International
                  Conference on Automated Deduction, Trento, Italy, July
                  7-10, 1999, Proceedings" }
@STRING{csechalmers="Department of Computer Science and Engineering, Chalmers
                  University of Technology" }
@STRING{elsevier= "Elsevier" }
@STRING{flops10 = "Functional and Logic Programming, 10th International
                  Symposium, FLOPS 2010, Sendai, Japan, April 19-21, 2010.
                  Proceedings " }
@STRING{icfp01  = "Proceedings of the sixth ACM SIGPLAN International
                  Conference on Functional Programming (ICFP 2001)" }
@STRING{icfp02  = "Proceedings of the seventh ACM SIGPLAN International
                  Conference on Functional Programming (ICFP '02),
                  Pittsburgh, Pennsylvania, USA, October 4-6, 2002" }
@STRING{infcomp = "Information and Computation" }
@STRING{jar     = "Journal of Automated Reasoning" }
@STRING{jflp    = "Journal of Functional and Logic Programming" }
@STRING{jfp     = "Journal of Functional Programming" }
@STRING{jlc     = "Journal of Logic and Computation" }
@STRING{lncs    = "Lecture Notes in Computer Science" }
@STRING{mpc95   = "Mathematics of Program Construction. Selected Papers from
                  the Third International Conference on the Mathematics of
                  Program Construction (July 17--21, 1995, Kloster Irsee,
                  Germany)" }
@STRING{padl10  = "Practical Aspects of Declarative Languages, 12th
                  International Symposium, PADL 2010, Madrid, Spain, January
                  18-19, 2010. Proceedings" }
@STRING{scp     = "Science of Computer Programming" }
@STRING{springer= "Springer-Verlag" }
@STRING{tcs     = "Theoretical Computer Science" }
@STRING{tlca93  = "Typed Lambda Calculi and Applications, International
                  Conference on Typed Lambda Calculi and Applications, TLCA
                  '93, Utrecht, The Netherlands, March 16-18, 1993,
                  Proceedings" }
@STRING{tlca99  = "Typed Lambda Calculi and Applications, 4th International
                  Conference, TLCA'99, L'Aquila, Italy, April 7-9, 1999,
                  Proceedings" }

@Article{         abadiCardelliCurienLevy:jfp91,
  author        = {Mart\'{\i}n Abadi and Luca Cardelli and Pierre-Louis
                  Curien and Jean-Jacques L{\'e}vy},
  title         = {Explicit Substitutions},
  journal       = jfp,
  volume        = 1,
  number        = 4,
  year          = 1991,
  pages         = {375--416},
  doi = {10.1017/S0956796800000186},
  bibsource     = {DBLP, http://dblp.uni-trier.de}
%  url          = {http://dx.doi.org/10.1017/S0956796800000186},
}

@Article{         adams:jfp93,
  author        = {Stephen Adams},
  title         = {Efficient Sets - A Balancing Act},
  journal       = jfp,
  volume        = 3,
  number        = 4,
  year          = 1993,
  pages         = {553-561},
  doi = {10.1017/S0956796800000885},
  bibsource     = {DBLP, http://dblp.uni-trier.de}
%  ee           = {http://dx.doi.org/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},
  title         = {Semantic foundations for typed assembly languages},
  journal       = toplas,
  volume        = 32,
  number        = 3,
  year          = 2010,
  doi = {10.1145/1709093.1709094},
  bibsource     = {DBLP, http://dblp.uni-trier.de}
%  ee           = {http://doi.acm.org/10.1145/1709093.1709094},
}

@Book{            barendregt:lambdacalculus,
  author        = {Henk Barendregt},
  title         = {The Lambda Calculus: Its Syntax and Semantics},
  publisher     = {North Holland},
  year          = 1984,
  address       = {Amsterdam}
%  doi = {},
}

@InProceedings{   bentonBiermanDePaivaHyland:tlca93,
  author        = {Nick Benton and Gavin M. Bierman and Valeria de Paiva and
                  Martin Hyland},
  title         = {A Term Calculus for Intuitionistic Linear Logic},
  booktitle     = tlca93,
  year          = 1993,
  pages         = {75-90},
  doi = {10.1007/BFb0037099},
  crossref      = {DBLP:conf/tlca/1993},
  bibsource     = {DBLP, http://dblp.uni-trier.de}
%  ee           = {http://dx.doi.org/10.1007/BFb0037099},
}

@InProceedings{   boespflug:padl10,
  author        = {Mathieu Boespflug},
  title         = {Conversion by Evaluation},
  booktitle     = padl10,
  year          = 2010,
  pages         = {58-72},
  doi = {10.1007/978-3-642-11503-5\_7},
  crossref      = {DBLP:conf/padl/2010},
  bibsource     = {DBLP, http://dblp.uni-trier.de}
%  ee           = {http://dx.doi.org/10.1007/978-3-642-11503-5\_7},
}

@Article{         deBruijn:nameless,
  author        = {N. G. de Bruijn},
  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},
  year          = 1972,
  volume        = 34,
  doi = {10.1016/1385-7258(72)90034-0},
  pages         = {381--392}
}

@Article{         cervesatoPfenning:spineCalculus,
  author        = {Iliano Cervesato and Frank Pfenning},
  title         = {A Linear Spine Calculus},
  journal       = jlc,
  volume        = 13,
  number        = 5,
  year          = 2003,
  pages         = {639-688},
  doi = {10.1093/logcom/13.5.639},
  bibsource     = {DBLP, http://dblp.uni-trier.de}
%  ee           = {http://dx.doi.org/10.1093/logcom/13.5.639},
}

@InProceedings{   coquand:type,
  author        = "Thierry Coquand",
  title         = "An Algorithm for Type-Checking Dependent Types",
  volume        = 26,
  number        = "1--3",
  series        = scp,
  pages         = "167--177",
  booktitle     = mpc95,
  year          = 1996,
  publisher     = elsevier,
  month         = may,
  doi = {10.1016/0167-6423(95)00021-6}
%  url          = {http://www.cs.chalmers.se/\~{}coquand/type.html}
}

@InProceedings{   fluetWeeks:icfp01,
  author        = {Matthew Fluet and Stephen Weeks},
  title         = {Contification Using Dominators},
  booktitle     = icfp01,
  year          = {2001},
  pages         = {2-13},
  doi = {10.1145/507635.507639},
  bibsource     = {DBLP, http://dblp.uni-trier.de}
%  ee           = {http://doi.acm.org/10.1145/507635.507639},
}

@Article{         girard:linear,
  author        = {Jean-Yves Girard},
  title         = {Linear Logic},
  journal       = tcs,
  volume        = 50,
  year          = 1987,
  pages         = {1-102},
  doi = {10.1016/0304-3975(87)90045-4},
  bibsource     = {DBLP, http://dblp.uni-trier.de}
}

@InProceedings{   gregoireLeroy:icfp02,
  author        = {Benjamin Gr{\'e}goire and Xavier Leroy},
  title         = {A compiled implementation of strong reduction},
  booktitle     = icfp02,
  year          = 2002,
  month         = sep,
  publisher     = acm,
  series        = {SIGPLAN Notices},
  volume        = 37,
  number        = 9,
  isbn          = {1-58113-487-8},
  pages         = {235--246},
  doi = {10.1145/581478.581501},
  bibsource     = {DBLP, http://dblp.uni-trier.de}
%  ee           = {http://doi.acm.org/10.1145/581478.581501},
}

@Manual{          inria:coq83,
  title         = {The Coq Proof Assistant Reference Manual},
  author        = {INRIA},
  organization  = {INRIA},
  edition       = {Version 8.3},
  year          = 2010,
  url           = {http://coq.inria.fr/}
%  note         = {{http://coq.inria.fr/}},
%  doi = {},
}

@Article{         kesnerLengrand:infcomp07,
  author        = {Delia Kesner and St{\'e}phane Lengrand},
  title         = {Resource operators for lambda-calculus},
  journal       = infcomp,
  volume        = 205,
  number        = 4,
  year          = 2007,
  pages         = {419-473},
  doi = {10.1016/j.ic.2006.08.008},
  bibsource     = {DBLP, http://dblp.uni-trier.de}
%  ee           = {http://dx.doi.org/10.1016/j.ic.2006.08.008},
}

@MastersThesis{   kraus:bachelor,
  author        = {Nicolai Kraus},
  title         = {A Lambda Term Representation Based on Linear Ordered
                  Logic},
  type          = {Bachelor's thesis},
  school        = {Department of Computer Science,
                  Ludwig-Maximilians-University Munich},
  year          = 2011
}

@Article{         mcBrideMcKinna:view,
  author        = {Conor McBride and James McKinna},
  title         = {The view from the left},
  journal       = jfp,
  volume        = 14,
  number        = 1,
  year          = 2004,
  pages         = {69-111},
  doi = {10.1017/S0956796803004829},
  bibsource     = {DBLP, http://dblp.uni-trier.de}
%  ee           = {http://dx.doi.org/10.1017/S0956796803004829},
}

@Article{         nadathur:jflp99,
  author        = {Gopalan Nadathur},
  title         = {A Fine-Grained Notation for Lambda Terms and Its Use in
                  Intensional Operations},
  journal       = jflp,
  volume        = 1999,
  number        = 2,
  year          = 1999,
  url           = {http://danae.uni-muenster.de/lehre/kuchen/JFLP/articles/1999/A99-02/A99-02.html},
  bibsource     = {DBLP, http://dblp.uni-trier.de}
%  doi = {},
}

@InProceedings{   nadathur:flops01,
  author        = {Gopalan Nadathur},
  title         = {The Metalanguage lambda-Prolog and Its Implementation},
  booktitle     = flops10,
  year          = 2001,
  pages         = {1-20},
  doi = {10.1007/3-540-44716-4\_1},
  crossref      = {DBLP:conf/flops/2001},
  bibsource     = {DBLP, http://dblp.uni-trier.de}
%  ee           = {http://dx.doi.org/10.1007/3-540-44716-4\_1},
}

@Article{         liangNadathurQi:jar05,
  author        = {Chuck Liang and Gopalan Nadathur and Xiaochu Qi},
  title         = {Choices in representation and reduction strategies for
                  lambda terms in intensional contexts},
  journal       = jar,
  year          = 2005,
  volume        = 33,
  number        = 2,
  doi           = {10.1007/s10817-004-6885-1},
  pages         = {89--132}
%  ee           = {http://dx.doi.org/10.1007/s10817-004-6885-1},
}

@PhDThesis{       norell:PhD,
  author        = {Ulf Norell},
  title         = {Towards a Practical Programming Language Based on
                  Dependent Type Theory},
  school        = csechalmers,
  year          = 2007,
  month         = sep,
  address       = {G\"{o}teborg, Sweden}
%  doi = {},
}

@InProceedings{   polakowPfenning:tlca99,
  author        = {Jeff Polakow and Frank Pfenning},
  title         = {Natural Deduction for Intuitionistic Non-communicative
                  Linear Logic},
  booktitle     = tlca99,
  year          = 1999,
  pages         = {295-309},
  doi = {10.1007/3-540-48959-2\_21},
  crossref      = {DBLP:conf/tlca/1999},
  bibsource     = {DBLP, http://dblp.uni-trier.de}
%  ee           = {http://dx.doi.org/10.1007/3-540-48959-2\_21},
}

@InProceedings{   carsten:twelf,
  author        = {Frank Pfenning and Carsten Sch{\"u}rmann},
  title         = {System Description: Twelf - A Meta-Logical Framework for
                  Deductive Systems},
  booktitle     = cade99,
  year          = {1999},
  pages         = {202-206},
  doi = {10.1007/3-540-48660-7\_14},
  crossref      = {DBLP:conf/cade/1999},
  bibsource     = {DBLP, http://dblp.uni-trier.de}
%  ee           = {http://dx.doi.org/10.1007/3-540-48660-7\_14},
}

@Article{         fernandezMackieSinot:aaecc05,
  author        = {Maribel Fern{\'a}ndez and Ian Mackie and
                  Fran\c{c}ois-R{\'e}gis Sinot},
  title         = {Lambda-Calculus with Director Strings},
  journal       = aaecc,
  volume        = 15,
  number        = 6,
  year          = 2005,
  pages         = {393-437},
  doi = {10.1007/s00200-005-0169-9},
  bibsource     = {DBLP, http://dblp.uni-trier.de}
%  ee           = {http://dx.doi.org/10.1007/s00200-005-0169-9},
}

@Article{         sinot:jlc05,
  author        = {Fran\c{c}ois-R{\'e}gis Sinot},
  title         = {Director Strings Revisited: A Generic Approach to the
                  Efficient Representation of Free Variables in Higher-order
                  Rewriting},
  journal       = jlc,
  volume        = 15,
  number        = 2,
  year          = 2005,
  pages         = {201-218},
  doi = {10.1093/logcom/exi010},
  bibsource     = {DBLP, http://dblp.uni-trier.de}
%  ee           = {http://dx.doi.org/10.1093/logcom/exi010},
}

@TechReport{      watkins:concurrentLFTR,
  author        = {Kevin Watkins and Iliano Cervesato and Frank Pfenning and
                  David Walker},
  title         = {A concurrent logical framework {I}: Judgements and
                  properties},
  institution   = {School of Computer Science, Carnegie Mellon University,
                  Pittsburgh},
  year          = 2003,
  key           = {CMU-CS02-101}
%  doi = {},
}

@Proceedings{     DBLP:conf/cade/1999,
  editor        = {Harald Ganzinger},
  title         = cade99,
  booktitle     = cade99,
  publisher     = springer,
  series        = lncs,
  volume        = 1632,
  year          = 1999,
  isbn          = {3-540-66222-7},
  bibsource     = {DBLP, http://dblp.uni-trier.de}
%  doi = {},
}

@Proceedings{     DBLP:conf/padl/2010,
  editor        = {Manuel Carro and Ricardo Pe{\~n}a},
  title         = padl10,
  booktitle     = padl10,
  publisher     = springer,
  series        = lncs,
  volume        = {5937},
  year          = {2010},
  isbn          = {978-3-642-11502-8},
  doi = {10.1007/978-3-642-11503-5},
  bibsource     = {DBLP, http://dblp.uni-trier.de}
%  ee           = {http://dx.doi.org/10.1007/978-3-642-11503-5},
}

@Proceedings{     DBLP:conf/tlca/1993,
  editor        = {Marc Bezem and Jan Friso Groote},
  title         = tlca93,
  booktitle     = tlca93,
  publisher     = springer,
  series        = lncs,
  volume        = 664,
  year          = 1993,
  isbn          = {3-540-56517-5},
  bibsource     = {DBLP, http://dblp.uni-trier.de}
%  doi = {},
}

@Proceedings{     DBLP:conf/tlca/1999,
  editor        = {Jean-Yves Girard},
  title         = tlca99,
  booktitle     = tlca99,
  publisher     = springer,
  series        = lncs,
  volume        = 1581,
  year          = 1999,
  isbn          = {3-540-65763-0},
  bibsource     = {DBLP, http://dblp.uni-trier.de}
%  doi = {},
}