% lf.bib
% Aaron Stump, 3/17/99
%
% This file contains references to works about the 
% Edinburgh Logical Framework (LF).

@article{HHP93,
author = "R. Harper and F. Honsell and G. Plotkin",
title = {{A Framework for Defining Logics}},
journal = "Journal of the Association for Computing Machinery",
volume="40",
number="1",
month = Jan,
year = 1993,
pages = "143-184"}


@techreport{BSF01,
author = "L. Bauer and M. Schneider and E. Felten",
institution = {{Princeton University}},
title = {{A Proof-Carrying Authorization System}},
number = "CS-TR-638-01",
month = April,
year = "2001"}


@conference{PfS98,
author = "F. Pfenning and C. Sch{\"u}rmann",
title = {{System Description: Twelf --- A Meta-Logical Framework for Deductive Systems}},
booktitle = "16th International Conference on Automated Deduction",
year="1999"}

@conference{NA00,
author = "N. Michael and A. Appel",
title = {{Machine Instruction Syntax and Semantics in Higher Order Logic}},
booktitle = "17th International Conference on Automated Deduction",
editor="D. McAllester",
year="2000"}

@conference{AF99,
author = "A. Appel and E. Felten",
title = {{Proof-carrying authentication}},
booktitle = "6th ACM Conference on Computer and Communication Security",
year="1999"}

@conference{A01,
author = "A. Appel",
title = {{Foundational Proof-Carrying Code}},
booktitle = "16th Annual IEEE Symposium on Logic in Computer Science",
year="2001"}

@phdthesis{ahmed04,
title={{Semantics of Types for Mutable State}},
author="A. Ahmed",
year=2004,
month=nov,
school={Princeton University}}

@conference{HP92,
author = "J. Hannan and F. Pfenning",
title = {{Compiler verification in LF}},
booktitle = "7th Annual IEEE Symposium on Logic in Computer Science",
editor="A. Scedrov",
year="1992"}

@conference{CP96,
author = "I. Cervesato and F. Pfenning",
title = {{A linear logical framework}},
booktitle = "11th Annual IEEE Symposium on Logic in Computer Science",
editor="E. Clarke",
year="1996"}


@conference{PY01,
author = "J. Polakow and K. Yi",
title = {{Proving Syntactic Properties of Exceptions in an Ordered Logical Framework}},
booktitle = "The Fifth International Symposium on Functional and Logic Programming (FLOPS 2001)",
year="2001"}

@Inproceedings{Pf92a,
author = {F. Pfenning},
editor = {F. Pfenning},
booktitle = {{Types in Logic Programming}},
publisher = "The MIT Press",
title = {{Dependent Types in Logic Programming}},
year = "1992",
pages = "285-299"}

@Book{HG91,
title = {{Logical Frameworks}},
editor = "G. Huet and G. Plotkin",
year = "1991",
publisher = "Cambridge University Press"}

@Inbook{C91,
title = {{An algorithm for testing conversion in Type Theory}},
author = "T. Coquand",
crossref = "HG91",
pages = "255-79"}

@Inbook{M00,
title = {{Arity Polymorphism and Dependent Types}},
author = "E. Moggi",
booktitle = "APPSEM Workshop on Subtyping and Dependent Types in Programming (DTP '00)",
year = "2000",
publisher = "http://www-sop.inria.fr/oasis/DTP00/"}

@inproceedings{NL00,
author = "G. Necula and P. Lee",
title = {{Proof Generation in the Touchstone Theorem Prover}},
booktitle= "17th International Conference on Automated Deduction",
Editor="David McAllester",
year = "2000"}

@conference{N97,
author = "G. Necula",
title = {{Proof-Carrying Code}},
booktitle = "24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages",
year="1997",
month=jan,
pages = "106-119"}

@conference{NL98,
author = "G. Necula and P. Lee",
title = {{Efficient representation and validation of proofs}},
booktitle = "13th Annual IEEE Symposium on Logic in Computer Science",
year="1998",
pages = "93-104"}

@inproceedings{necula+01,
title={{Oracle-Based Checking of Untrusted Software}},
author="G. Necula and S. Rahul",
booktitle={{Proceedings of the 28th ACM Symposium on Principles of Programming Languages}},
year=2001}

@conference{specialj00,
title={{A Certifying Compiler for Java}}, 
author="C. Colby and P. Lee and G. Necula and F. Blau and K. Cline and M. Plesko",
booktitle={{Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation}},
year=2000}

@conference{necula98,
author="G. Necula and P. Lee",
title="The Design and Implementation of a Certifying Compiler",
booktitle={{Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation}},
year=1998}

@conference{necula00,
title={{Translation Validation for an Optimizing Compiler}},
author="G. Necula",
booktitle={{Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation}},
year=2000}

@phdthesis{N98,
author = "G. Necula",
title = {{Compiling with Proofs}},
year="1998",
month=sep,
school={Carnegie Mellon University}}

@inproceedings{B98,
author = "G. Barthe",
title= {{Existence and Uniqueness of Normal Forms in Pure Type Systems with beta-eta conversion}},
editor= "G. Gottlob and E. Grandjean and K. Seyr",
booktitle="Proceedings of Computer Science Logic",
series="LNCS",
publisher="Springer-Verlag",
number=1584,
year=1998}

@techreport{HP00,
author = "R. Harper and F. Pfenning",
institution = {{Carnegie Mellon University}},
title = {{On Equivalence and Canonical Forms in the LF Type Theory}},
number = "CMU-CS-00-148",
month = Jul,
year = "2000"}

@Article{Harper05tocl,
  author = 	 {Robert Harper and Frank Pfenning},
  title = 	 {On Equivalence and Canonical Forms in the {LF} Type Theory},
  journal = 	 {Transactions on Computational Logic},
  year = 	 2005,
  month =        jan,
  volume =       6,
  issue =        1,
  pages =        {61--101}
}

@inproceedings{Goguen05,
  author    = {Healfdene Goguen},
  title     = {A syntactic approach to eta equality in type theory.},
  booktitle = {Principles of Programming Languages (POPL)},
  year      = {2005},
  pages     = {75-84}
}

@inproceedings{P01b,
author= "F. Pfenning",
title={{Intensionality, Extensionality, and Proof Irrelevance in Modal Type Theory}},
booktitle="16th IEEE Symposium on Logic in Computer Science",
Publisher="IEEE Computer Society",
year = 2001
}

@phdthesis{V99,
author = "R. Virga",
title = {{Higher-Order Rewriting with Dependent Types}},
year="1999",
month=oct,
school={Carnegie Mellon University}}

@phdthesis{G93,
author = "H. Geuvers",
title = {{Logics and Type systems}},
year="1993",
month="September",
school={University of Nijmegen}}

@phdthesis{M95,
author = "M. Hofmann",
title = {{Extensional concepts in intensional type theory}},
year="1995",
school={University of Edinburgh}}

@inproceedings{PS98,
author = "F. Pfenning and C. Sch{\"u}rmann",
title = "Algorithms for Equality and Unification in the Presence of Notational Definitions",
booktitle = "Proceedings of the {CADE} Workshop on Proof Search in Type-Theoretic Languages",
publisher = "Electronic Notes in Theoretical Computer Science",
editor = "D. Galmiche",
year = "1998"}

@Book{AGM92,
title = {{Handbook of Logic in Computer Science}},
editor = "S. Abramsky and D. Gabbay and T. Maibaum",
year = "1992",
publisher = "Oxford University Press"}

@book{barendregt84,
author="H. Barendregt",
title={{The Lambda Calculus, Its Syntax and Semantics}},
publisher="North-Holland",
year=1984}

@Inbook{B92,
title = {{Lambda Calculi with Types}},
author = "H. Barendregt",
crossref = "AGM92",
volume = "2",
pages = "117-309"}

@techreport{LP92,
author = "Z. Luo and R. Pollack",
title = {{LEGO Proof Development System: User's Manual}},
institution = "Edinburgh LFCS",
number = "ECS-LFCS-92-211",
year = "1992"}

@book{J99,
author = "B. Jacobs",
title = {{Categorical Logic and Type Theory}},
publisher = "Elsevier",
year = "1999"}

@article{AC01,
author = "D. Aspinall and A. Compagnoni",
title = "Subtyping Dependent Types",
journal = "Theoretical Computer Science",
year = "2001",
volume=266,
number="1-2"}

@inproceedings{A00,
author = "D. Aspinall",
title = "Subtyping with Power Types",
booktitle = "Computer Science Logic (CSL)",
publisher="Springer",
series="LNCS",
year = "2000"}


@INPROCEEDINGS{SO99,
     AUTHOR = "N. Shankar and S. Owre",
     TITLE = {{Principles and Pragmatics of Subtyping in PVS}},
     YEAR = {1999},
     URL = {http://www.csl.sri.com/papers/wadt99/},
     SERIES = "LNCS",
     BOOKTITLE = {Recent Trends in Algebraic Development Techniques},
     PUBLISHER = {Springer-Verlag},
     EDITOR = "D. Bert and C. Choppy and P. Mosses"}

@article{L99a,
author = "Z. Luo",
title = {{Coercive subtyping}},
journal = "Journal of Logic and Computation",
volume="9",
number="1",
year = 1999}

@article{K01,
author = "F. Kamareddine",
title = {{Reviewing the classical and the de Bruijn notation for $\lambda$-calculus and pure type systems}},
journal="Logic and Computation",
volume="11",
number="3",
pages= "363-394"}

@inproceedings{CKL01,
author="H. Cirstea and C. Kirchner and L. Liquori",
title = {{The Rho Cube}},
booktitle="Foundations of Software Science and Computation Structures (FOSSACS)",
editor="F. Honsell",
year="2001"}

@inproceedings{CKL01b,
author="H. Cirstea and C. Kirchner and L. Liquori",
title = {{Matching Power}},
booktitle="Rewriting Techniques and Applications (RTA)",
editor="A. Middeldorp",
year="2001"}

@techreport{J01,
author = "G. Jojgov",
title = {{Systems for Open Terms: An Overview}},
institution = "Technische Universiteit Eindhoven",
number = "CS-Report 01-03",
year = "2001"}

@INPROCEEDINGS{PS93,
 AUTHOR={A.~Pitts and I.~Stark},
 TITLE={Observable Properties of Higher Order Functions That
 Dynamically Create Local Names, or: What's new?}, 
 BOOKTITLE={Mathematical Foundations of Computer Science, Proc.\ 18th
 Int.\ Symp., {Gda{\'n}sk}, 1993},
 SERIES={Lecture Notes in Computer Science},
 VOLUME=711,
 PUBLISHER={Springer-Verlag},
 YEAR=1993}

@techreport{Sa04,
author = "J. Sarnat",
title = {{LF-Sigma: The Metatheory of LF with Sigma types}},
institution = "Yale CS department",
number = "1268",
year = "2004"}

@inproceedings{pe88,
author="F. Pfenning and C. Elliott",
title="Higher-order abstract syntax",
booktitle="ACM SIGPLAN Symposium on Language Design and Implementation",
year="1988"}

@Misc{alti:esslli96,
  author =	 "T. Altenkirch",
  title =	 "Integrated Verification in {Type} {Theory}",
  howpublished = "Lecture notes for a course at ESSLLI 96, Prague",
  year =	 "1996",
  note = "Available from the author's website"
}

@phdthesis{ magnusson95,
    author = "Lena Magnusson",
    title = "The Implementation of {ALF}---a Proof Editor Based on {M}artin-{L}{\"o}f's Monomorphic Type Theory with Explicit Substitution",
    year = "1995",
    school = {{Chalmers University of Technology and G\"{o}teborg University}}
}

@inproceedings{cayenne98,
 author = {Lennart Augustsson},
 title = {Cayenne -- a language with dependent types},
 booktitle = {{Proceedings of the third ACM SIGPLAN International Conference on Functional Programming}},
 year = {1998},
 pages = {239--250},
 publisher = {ACM Press}
 }

@inproceedings{XiLICS00,
author = "Hongwei Xi",
title = {{Imperative Programming with Dependent Types}},
booktitle = {{Proceedings of 15th IEEE Symposium on Logic in Computer Science}},
year = 2000,
month = "June",
pages = "375--387"
}

@InProceedings{alti:wcgp02,
  author = 	 {Thorsten Altenkirch and Conor McBride},
  title = 	 {Generic Programming Within Dependently Typed Programming},
  booktitle = 	 {Generic Programming},
  year =	 {2003},
  note =	 {Proceedings of the IFIP TC2 Working Conference on Generic Programming, Schloss Dagstuhl, July 2002}
}

@inproceedings{delphin01,
author = {C. Sch\"urmann},
title = "Recursion for Higher-Order Encodings",
booktitle = {{Proceedings of Computer Science Logic}},
year = 2001,
number = 2142,
series = "LNCS",
pages = "585--599"}

@inproceedings{hamid02syntactic,
  author = "N. Hamid and Z. Shao and V. Trifonov and S. Monnier and Z. Ni",
  title = {{A Syntactic Approach to Foundational Proof Carrying-Code}},
  booktitle = "IEEE Symposium on Logic in Computer Science",
  year = "2002" }

@techreport{crary03,
author = "K. Crary and S. Sarkar",
title= {{A Metalogical Approach to Foundational Certified Code}},
institution = "CMU Computer Science",
number= "CMU-CS-03-108",
month= "January",
year= 2003}

@ARTICLE{pollackFAC02,
  AUTHOR = {Robert Pollack},
  TITLE = {Dependently Typed Records in Type Theory},
  JOURNAL = {Formal Aspects of Computing},
  YEAR = 2002,
  VOLUME = 13,
  PAGES = {386--402}
}

@InProceedings{harper+:sharing,
  author = 	 "Robert Harper and Mark Lillibridge",
  title = 	 "A Type-Theoretic Approach to Higher-Order Modules with
		  Sharing",
  pages = 	 "123--137",
  booktitle =    "21st Symposium on Principles of Programming Languages",
  year = 	 1994
}

@unpublished{schurmann04,
author={{C. Sch\"{u}rmann}},
title={{Programming with Higher-Order Abstract Syntax}},
note="draft available from author's website"}

@techreport{clf02,
title={{A Concurrent Logical Framework I: Judgments and Properties}},
author="K. Watkins and I. Cervesato and F. Pfenning and D. Walker",
institution="Carnegie Mellon University",
number="CMU-CS-02-101",
year="2002"} 

@INPROCEEDINGS{Coq+03,
  AUTHOR = {T. Coquand and R. Pollack and M. Takeyama},
  TITLE = {{A Logical Framework with Dependently Typed Records}},
  BOOKTITLE = {Typed Lambda Calculus and Applications},
  YEAR = 2003,
  SERIES = {{LNCS}},
  VOLUME = 2701,
  PUBLISHER = {Springer-Verlag}
}


@ARTICLE{pollack02,
  AUTHOR = {Robert Pollack},
  TITLE = {{Dependently Typed Records in Type Theory}},
  JOURNAL = {Formal Aspects of Computing},
  YEAR = 2002,
  VOLUME = 13,
  PAGES = {386--402}
}

@INPROCEEDINGS{McKinnaPollack93,
  AUTHOR = {J. McKinna and R. Pollack},
  TITLE = {{P}ure {T}ype {S}ystems Formalized},
  BOOKTITLE = {{Proceedings of the International Conference on Typed
                 Lambda Calculi and Applications}},
  YEAR = 1993,
  EDITOR = {M.Bezem and J.F.Groote},
  PAGES = {289--305},
  MONTH = MAR,
  PUBLISHER = {Springer-Verlag},
  SERIES = {{LNCS}},
  NUMBER = 664
}

@ARTICLE{McKinnaPollack99,
  AUTHOR = {J. McKinna and R. Pollack},
  TITLE = {Some Lambda Calculus and Type Theory Formalized},
  JOURNAL = {Journal of Automated Reasoning},
  YEAR = 1999,
  VOLUME = 23,
  NUMBER = {3--4},
  MONTH = NOV,
  URL = {http://homepages.inf.ed.ac.uk/rpollack/export/McKinnaPollack99.ps.gz}
}

@inproceedings{kopylov03,
author="A. Kopylov",
title={{Dependent Intersection: A New Way of Defining Records in Type Theory}},
booktitle={IEEE Symposium on Logic in Computer Science},
year=2003,
editor="P. Kolaitis"}

@inproceedings{schurmann+03,
author={C. Sch\"{u}rmann and F. Pfenning},
title={{A Coverage Checking Algorithm for LF}},
editor="D. Basin and B. Wolff",
booktitle="Proceedings of the 16th International Conference on Theorem Proving in Higher Order Logics",
pages="120--135",
year=2003,
publisher="Springer-Verlag",
series="LNCS",
volume="2758"}

@inproceedings{sheard04b,
author="T. Sheard and E. Pasalic",
title={{Meta-Programming with Built-in Type Equality}},
booktitle="4th International Workshop on Logical Frameworks and Meta-Languages",
editor={{C. Sch\"{u}rmann}},
year=2004}

@inproceedings{aspinall+04,
author="D. Aspinall and L. Beringer and M. Hofmann and H-W. Loidl and A. Momigliano",
title={{A Program Logic for Resource Verification}},
booktitle="Proceedings of the 17th Interntaional Conference on Theorem Proving in Higher Order Logics",
editor="K. Slind",
year=2004}

@article{coq88,
 author = {T. Coquand and G. Huet},
 title = {{The Calculus of Constructions}},
 journal = {Information and Computation},
 volume = {76},
 number = {2-3},
 year = {1988},
 pages = "95--120"}

% use reference "coq" in theorem_provers instead.
@techreport{DAHH93,
 author = {G. Dowek and A. Felty and H. Herbelin and G. Huet},
 title = {The {Coq} proof assistant user's guide},
 number = {154},
 year = {1993},
 institution = {Inria-Rocquencourt},
 address = {France}
}

@inproceedings{hofmann+98,
author="M. Hofmann and T. Streicher",
title="The groupoid interpretation of type theory",
editor="G. Sambin",
booktitle="Twenty-five years of constructive type theory",
year="1998",
publisher="Oxford: Clarendon Press",
pages="83--111"}

@phdthesis{hofmann95,
author="M. Hofmann",
title ="Extensional concepts in intensional type theory",
year=1995,
school={Edinburgh LFCS}}

  @inproceedings{pfenning01irrel,
    author = 	 {F. Pfenning},
    title = 	 {{Intensionality, Extensionality, and Proof Irrelevance in Modal Type Theory}},
    booktitle = 	 {Proceedings of the Sixteenth Annual IEEE Symp. on Logic in Computer Science, {LICS} 2001},
    year =	 2001,
    editor =	 {J. Halpern},
    publisher =	 {IEEE Computer Society Press}
  }

@phdthesis{schurmann-thesis,
    author = {C. Sch\"{u}rmann},
    title = "Automating the Meta Theory of Deductive Systems",
    year = "2000",
    school = {{Carnegie Mellon University}}
}

@InProceedings{barras96b,
  author =       {B.~Barras},
  title =        {Verification of the Interface of a Small Proof
                  System in Coq},
  editor =       {E.~Gimenez and C.~Paulin-Mohring},
  booktitle =    {Proceedings of the 1996 Workshop on Types
                  for Proofs and Programs},
  publisher =    {Springer-Verlag LNCS 1512},
  address =      {Aussois, France},
  month =        dec,
  year =         {1996},
  pages =        {28--45}
}

@InProceedings{bauer+:grey,
  author = 	 {L. Bauer and S. Garriss and J. McCune and M. Reiter and J. Rouse and P. Rutenbar},
  title = 	 {Device-enabled authorization in the {G}rey system},
  booktitle =    {Proceedings of the 8th Information Security Conference (ISC'05)},
  month =        sep,
  year = 	 {2005}
}

@book{luo94,
author="Z. Luo",
title={{Computation and Reasoning: a Type Theory for Computer Science}},
publisher="Oxford Science Publications",
year=1994}

@inproceedings{geuvers+04,
author="H. Geuvers and F. Wiedijk",
title={{A Logical Framework with Explicit Conversions}},
booktitle={{Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-Languages}},
year=2004,
editor="C. Sch{\"u}rmann"}

@conference{thery07,
author = "Laurent Th\'{e}ry and Guillaume Hanrot",
title = {Primality Proving with Elliptical Curves},
booktitle = "20th International Conference on Theorem Proving in Higher Order Logics (TPHOLS '07)",
year="2007",
month="September"
}

@Article{bove+05,
  author = 	 {A. Bove and V. Capretta},
  title = 	 {Modelling General Recursion in Type Theory},
  journal = 	 {Mathematical Structures in Computer Science},
  year = 	 {2005},
  month =        {February},
  volume = 	 {15},
  pages = 	 {671--708},
  note = 	 {Cambridge University Press}
}

@book{ml84,
title="Intuitionistic type theory",
author="P. Martin-L{\"o}f",
publisher="Bibliopolis",
year=1984}



@article{debruijn72,
author="N. de Bruijn",
title={{Lambda Calculus Notation With Nameless Dummies, A Tool For Automatic Formula Manipulation, With Application To The Church-Rosser Theorem}},
journal="Indagationes Mathematicae",
volume=34,
number=5,
pages="381--392",
year="1972"}

@inproceedings{momigliano+07,
title={{Two-level Hybrid: A System for Reasoning Using Higher-Order Abstract Syntax}},
author="A. Momigliano and A. Martin and A. Felty",
booktitle={International Workshop on Logical Frameworks and Metalanguages: Theory and Practice (LFMTP)},
editor="C. Sch{\"u}rmann",
year="2007"}

@inproceedings{rabe06,
author = "F. Rabe",
title = "{First-Order Logic with Dependent Types}",
booktitle = "{Proceedings of the 3rd International Joint Conference on Automated Reasoning}",
editor = "N. Shankar and U. Furbach",
year = 2006,
publisher = "Springer",
series = "LNCS",
volume = "4130",
pages = "377--391",
}

@inproceedings{urban+08,
author="C. Urban and J. Cheney and S. Berghofer",
title={{Mechanising the Metatheory of LF}},
booktitle={Proc. of the 23rd IEEE Symposium on Logic in Computer Science},
publisher="IEEE Computer Society",
year="2008",
pages="45--56"}

@inproceedings{lee+07,
 author = {D. Lee and K. Crary and R. Harper},
 title = {{Towards a Mechanized Metatheory of Standard ML}},
 booktitle = {{Proc. 34th ACM Symposium on Principles of Programming Languages}},
 year = {2007},
 pages = {173--184},
 publisher = {ACM Press}
 }

@inproceedings{chapman08,
author="J. Chapman",
title={{Type Theory Should Eat Itself}},
booktitle={{Proc. Workshop on Logical Frameworks and Meta-Languages: Theory and Practice}},
editor="A. Abel and C. Urban",
year=2008}