auto-lfmtp11.bib

%%%% WARNING! AUTOMATICALLY CREATED BIBFILE
%%%% DO NOT EDIT! ALL CHANGES WILL BE LOST!

@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},
  ee		= {http://dx.doi.org/10.1017/S0956796800000186},
  bibsource	= {DBLP, http://dblp.uni-trier.de}
}

@Article{	  adams:jfp93,
  author	= {Stephen Adams},
  title		= {Efficient Sets - A Balancing Act},
  journal	= jfp,
  volume	= 3,
  number	= 4,
  year		= 1993,
  pages		= {553-561},
  ee		= {http://dx.doi.org/10.1017/S0956796800000885},
  bibsource	= {DBLP, http://dblp.uni-trier.de}
}

@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,
  ee		= {http://doi.acm.org/10.1145/1709093.1709094},
  bibsource	= {DBLP, http://dblp.uni-trier.de}
}

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

@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},
  ee		= {http://dx.doi.org/10.1007/BFb0037099},
  crossref	= {DBLP:conf/tlca/1993},
  bibsource	= {DBLP, http://dblp.uni-trier.de}
}

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

@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,
  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},
  ee		= {http://dx.doi.org/10.1093/logcom/13.5.639},
  bibsource	= {DBLP, http://dblp.uni-trier.de}
}

@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,
  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},
  ee		= {http://doi.acm.org/10.1145/507635.507639},
  bibsource	= {DBLP, http://dblp.uni-trier.de}
}

@Article{	  girard:linear,
  author	= {Jean-Yves Girard},
  title		= {Linear Logic},
  journal	= tcs,
  volume	= 50,
  year		= 1987,
  pages		= {1-102},
  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},
  ee		= {http://doi.acm.org/10.1145/581478.581501},
  bibsource	= {DBLP, http://dblp.uni-trier.de}
}

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

@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},
  ee		= {http://dx.doi.org/10.1016/j.ic.2006.08.008},
  bibsource	= {DBLP, http://dblp.uni-trier.de}
}

@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},
  ee		= {http://dx.doi.org/10.1017/S0956796803004829},
  bibsource	= {DBLP, http://dblp.uni-trier.de}
}

@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}
}

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

@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,
  ee		= {http://dx.doi.org/10.1007/s10817-004-6885-1},
  doi		= {10.1007/s10817-004-6885-1},
  pages		= {89--132}
}

@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}
}

@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},
  ee		= {http://dx.doi.org/10.1007/3-540-48959-2_21},
  crossref	= {DBLP:conf/tlca/1999},
  bibsource	= {DBLP, http://dblp.uni-trier.de}
}

@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},
  ee		= {http://dx.doi.org/10.1007/3-540-48660-7_14},
  crossref	= {DBLP:conf/cade/1999},
  bibsource	= {DBLP, http://dblp.uni-trier.de}
}

@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},
  ee		= {http://dx.doi.org/10.1007/s00200-005-0169-9},
  bibsource	= {DBLP, http://dblp.uni-trier.de}
}

@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},
  ee		= {http://dx.doi.org/10.1093/logcom/exi010},
  bibsource	= {DBLP, http://dblp.uni-trier.de}
}

@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}
}

@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}
}

@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},
  ee		= {http://dx.doi.org/10.1007/978-3-642-11503-5},
  bibsource	= {DBLP, http://dblp.uni-trier.de}
}

@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}
}

@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}
}