Extracted from fox-bib.bib with
M-x bibtex-extract-matching-entries fox.bib keywords lf
Thu Mar  8 14:47:55 EST 2001
		  
@Unpublished{Cervesato?jsc,
  author =       "Iliano Cervesato and Frank Pfenning",
  title =        "Linear Higher-Order Pre-Unification",
  note =         "Submitted for publication to the {\em Journal of
                 Symbolic Computation}",
  annote =       "Extended version of~\cite{Cervesato97lics}",
  keywords =     "lf",
}

@Unpublished{Cervesato?ic,
  author =       "Iliano Cervesato and Frank Pfenning",
  title =        "A Linear Logical Framework",
  note =         "Submitted for publication to {\em Information and
                 Computation}",
  annote =       "Extended version of~\cite{Cervesato96lics}",
  URL =          "http://www.cs.cmu.edu/~fp/papers/llf00.ps.gz",
  keywords =     "lf",
}

@Unpublished{Colby?tcs,
  author =       "Christopher Colby and Karl Crary and Robert Harper and
                 Peter Lee and Frank Pfenning",
  title =        "Automated Techniques for Provably Safe Mobile Code",
  note =         "To appear in a special issue of Theoretical Computer
                 Science on {\em Dependable Computing}",
  annote =       "Preliminary version appeared in~\cite{Crary00discex}",
  urlabstract =  "http://www.cs.cmu.edu/~rwh/papers/certcomp/tcs.abstract",
  urlps =        "http://www.cs.cmu.edu/~fp/papers/tcs00.ps.gz",
  urlpdf =       "http://www.cs.cmu.edu/~rwh/papers/certcomp/tcs.pdf",
  keywords =     "lf, pcc, til",
}

@Unpublished{Pfenning?handbook,
  author =       "Frank Pfenning",
  title =        "Logical Frameworks",
  note =         "In press. Chapter 16 of Alan Robinson and Andrei
                 Voronkov, editors, {\em Handbook of Automated
                 Reasoning}, to be published by Elsevier Science and MIT
                 Press",
  keywords =     "lf",
}

@PhdThesis{Schurmann00phd,
  author =       "Carsten Sch{\"u}rmann",
  title =        "Automating the Meta Theory of Deductive Systems",
  school =       "Department of Computer Science, Carnegie Mellon
                 University",
  year =         "2000",
  month =        aug,
  note =         "Available as Technical Report CMU-CS-00-146",
  URL =          "http://reports-archive.adm.cs.cmu.edu/anon/2000/abstracts/00-146.html",
  keywords =     "lf",
}

@TechReport{Harper00tr148,
  author =       "Robert Harper and Frank Pfenning",
  title =        "On Equivalence and Canonical Forms in the {LF} Type
                 Theory",
  institution =  "School of Computer Science, Carnegie Mellon
                 University",
  year =         "2000",
  number =       "CMU-CS-00-148",
  month =        jul,
  urlabstract =  "http://reports-archive.adm.cs.cmu.edu/anon/2000/abstracts/00-148.html",
  urlps =        "http://reports-archive.adm.cs.cmu.edu/anon/2000/CMU-CS-00-148.ps",
  urlpdf =       "http://reports-archive.adm.cs.cmu.edu/anon/2000/CMU-CS-00-148.pdf",
  keywords =     "lf",
}

@InProceedings{Colby00pldi,
  author =       "Christopher Colby and Peter Lee and George C. Necula
                 and Fred Blau and Mark Plesko and Kenneth Cline",
  title =        "A Certifying Compiler for {J}ava",
  booktitle =    "Proceedings of the Conference on Programming Language
                 Design and Implementation",
  year =         "2000",
  publisher =    "ACM Press",
  address =      "Vancouver, Canada",
  pages =        "95--107",
  month =        jun,
  urlps =        "http://www.cs.berkeley.edu/~necula/pldi00b.ps.gz",
  keywords =     "lf, pcc",
}

@InProceedings{Pientka00induct,
  author =       "Brigitte Pientka and Frank Pfenning",
  title =        "Termination and Reduction Checking in the Logical
                 Framework",
  editor =       "Carsten Sch{\"u}rmann",
  booktitle =    "Proceedings of the {CADE} Workshop on Automation of
                 Proofs by Mathematical Induction",
  year =         "2000",
  address =      "Pittsburgh, Pennsylvania",
  month =        jun,
  URL =          "http://www.cs.cmu.edu/~fp/papers/induct00.ps.gz",
  keywords =     "lf",
}

@InProceedings{Polakow00lfm,
  author =       "Jeff Polakow and Frank Pfenning",
  title =        "Properties of Terms in Continuation-Passing Style in
                 an Ordered Logical Framework",
  editor =       "Jo{\"e}lle Despeyroux",
  booktitle =    "Proceedings of the Workshop on Logical Frameworks and
                 Meta-languages",
  year =         "2000",
  address =      "Santa Barbara, California",
  month =        jun,
  URL =          "http://www.cs.cmu.edu/~fp/papers/lfm00.ps.gz",
  keywords =     "lf",
}

@InProceedings{Schurmann00lfm,
  author =       "Carsten Sch{\"u}rmann",
  title =        "A Meta Logical Framework Based on Realizability",
  booktitle =    "Proceedings of the Workshop on Logical Frameworks and
                 Meta-Languages",
  editor =       "Jo{\"e}lle Despeyroux",
  year =         "2000",
  address =      "Santa Barbara, California",
  month =        jun,
  URL =          "http://cs-www.cs.yale.edu/homes/carsten/papers/S00a.ps.gz",
  keywords =     "lf",
}

@InProceedings{Necula00cade,
  author =       "George C. Necula and Peter Lee",
  title =        "Proof Generation in the {Touchstone} Theorem Prover",
  editor =       "David McAllester",
  pages =        "25--44",
  booktitle =    "Proceedings of the International Conference on
                 Automated Deduction",
  year =         "2000",
  publisher =    "Springer-Verlag LNAI 1831",
  address =      "Pittsburgh, Pennsylvania",
  month =        jun,
  urlps =        "http://www.cs.berkeley.edu/~necula/cade00.ps.gz",
  keywords =     "lf, pcc",
}

@Article{Pfenning00ic,
  author =       "Frank Pfenning",
  title =        "Structural Cut Elimination {I}. Intuitionistic and
                 Classical Logic",
  journal =      "Information and Computation",
  year =         "2000",
  volume =       "157",
  number =       "1/2",
  pages =        "84--141",
  month =        mar,
  urlpdf =       "http://www.idealibrary.com/links/artid/inco.1999.2832/production/pdf",
  keywords =     "lf",
}

@Article{Cervesato00tcs,
  author =       "Iliano Cervesato and Joshua S. Hodas and Frank
                 Pfenning",
  title =        "Efficient Resource Management for Linear Logic Proof
                 Search",
  journal =      "Theoretical Computer Science",
  year =         "2000",
  volume =       "232",
  number =       "1--2",
  pages =        "133--163",
  month =        feb,
  annote =       "Extended version of~\cite{Cervesato96elp}",
  URL =          "http://www.cs.stanford.edu/~iliano/papers/tcs00.ps.gz",
  keywords =     "lf",
}

@InProceedings{Crary00discex,
  author =       "Karl Crary and Robert Harper and Peter Lee and Frank
                 Pfenning",
  title =        "Automated Techniques for Provably Safe Mobile Code",
  booktitle =    "Proceedings of the {DARPA} Information Survivability
                 Conference and Exposition",
  volume =       "1",
  pages =        "406--419",
  year =         "2000",
  address =      "Hilton Head Island, South Carolina",
  month =        jan,
  publisher =    "IEEE Computer Society Press",
  URL =          "http://www.computer.org/proceedings/discex/0490/volume%201/04900406abs.htm",
  keywords =     "lf, pcc, til",
}

@InProceedings{Harper99lfm,
  author =       "Robert Harper and Frank Pfenning",
  title =        "On Equivalence and Canonical Forms in the {LF} Type
                 Theory (Extended Abstract)",
  booktitle =    "Proceedings of the Workshop on Logical Frameworks and
                 Meta-Languages",
  editor =       "Amy Felty",
  year =         "1999",
  address =      "Paris, France",
  month =        sep,
  annote =       "Extended version available as~\cite{Harper99tr159}",
  urlabstract =  "http://www.cs.cmu.edu/~rwh/papers/lf-theory/abstract",
  urlps =        "http://plan9.bell-labs.com/who/felty/LFM99/HarperPfenning.ps.gz",
  keywords =     "lf",
}

@TechReport{Harper99tr159,
  author =       "Robert Harper and Frank Pfenning",
  title =        "On Equivalence and Canonical Forms in the {LF} Type
                 Theory",
  institution =  "School of Computer Science, Carnegie Mellon
                 University",
  year =         "1999",
  number =       "CMU-CS-99-159",
  month =        sep,
  annote =       "Superseded by~\cite{Harper00tr148}",
  urlabstract =  "http://reports-archive.adm.cs.cmu.edu/anon/1999/abstracts/99-159.html",
  urlps =        "http://reports-archive.adm.cs.cmu.edu/anon/1999/CMU-CS-99-159.ps",
  urlpdf =       "http://reports-archive.adm.cs.cmu.edu/anon/1999/CMU-CS-99-159.pdf",
  keywords =     "lf",
}

@InProceedings{Pfenning99ppdp,
  author =       "Frank Pfenning",
  title =        "Logical and Meta-Logical Frameworks",
  booktitle =    "Proceedings of the International Conference on
                 Principles and Practice of Declarative Programming",
  editor =       "G. Nadathur",
  year =         "1999",
  publisher =    "Springer-Verlag LNCS 1702",
  address =      "Paris, France",
  month =        sep,
  pages =        "206",
  note =         "Abstract of invited talk",
  URL =          "http://www.cs.cmu.edu/~fp/talks/ppdp99-talk.ps",
  keywords =     "lf",
}

@PhdThesis{Virga99phd,
  author =       "Roberto Virga",
  title =        "Higher-Order Rewriting with Dependent Types",
  school =       "Department of Mathematical Sciences, Carnegie Mellon
                 University",
  month =        sep,
  year =         "1999",
  note =         "Available as Technical Report CMU-CS-99-167",
  urldvi =       "http://www.cs.cmu.edu/~rvirga/papers/thesis.dvi",
  urlps =        "http://www.cs.cmu.edu/~rvirga/papers/thesis.ps",
  urlpdf =       "http://www.cs.cmu.edu/~rvirga/papers/thesis.pdf",
  keywords =     "lf",
}

@InProceedings{Pfenning99cade,
  author =       "Frank Pfenning and Carsten Sch{\"u}rmann",
  title =        "System Description: Twelf --- {A} Meta-Logical
                 Framework for Deductive Systems",
  editor =       "H. Ganzinger",
  pages =        "202--206",
  booktitle =    "Proceedings of the International Conference on
                 Automated Deduction",
  year =         "1999",
  publisher =    "Springer-Verlag LNAI 1632",
  address =      "Trento, Italy",
  month =        jul,
  urlps =        "http://www.cs.cmu.edu/~fp/papers/cade99.ps.gz",
  keywords =     "lf",
}

@InProceedings{Plesko99,
  author =       "Mark Plesko and Frank Pfenning",
  title =        "A Formalization of the Proof-Carrying Code
                 Architecture in a Linear Logical Framework",
  editor =       "A. Pnueli and P. Traverso",
  booktitle =    "Proceedings of the {FLoC} Workshop on Run-Time Result
                 Verification",
  year =         "1999",
  address =      "Trento, Italy",
  month =        jul,
  urlps =        "http://www.cs.cmu.edu/~fp/papers/pccllf99.ps.gz",
  keywords =     "lf, pcc",
}

@InProceedings{Polakow99mfps,
  author =       "Jeff Polakow and Frank Pfenning",
  title =        "Relating Natural Deduction and Sequent Calculus for
                 Intuitionistic Non-Commutative Linear Logic",
  editor =       "Andre Scedrov and Achim Jung",
  booktitle =    "Proceedings of the Conference on Mathematical
                 Foundations of Programming Semantics",
  year =         "1999",
  address =      "New Orleans, Louisiana",
  month =        apr,
  note =         "Electronic Notes in Theoretical Computer Science,
                 Volume 20",
  urlps =        "http://www.cs.cmu.edu/~fp/papers/mfps99.ps.gz",
  keywords =     "lf",
}

@InProceedings{Polakow99tlca,
  author =       "Jeff Polakow and Frank Pfenning",
  title =        "Natural Deduction for Intuitionistic Non-Commutative
                 Linear Logic",
  editor =       "J.-Y. Girard",
  booktitle =    "Proceedings of the International Conference on Typed
                 Lambda Calculi and Applications",
  year =         "1999",
  publisher =    "Springer-Verlag LNCS 1581",
  address =      "L'Aquila, Italy",
  month =        apr,
  pages =        "295--309",
  urlps =        "http://www.cs.cmu.edu/~fp/papers/tlca99.ps.gz",
  keywords =     "lf",
}

@PhdThesis{Necula98phd,
  author =       "George C. Necula",
  title =        "Compiling with Proofs",
  school =       "Carnegie Mellon University",
  year =         "1998",
  month =        oct,
  note =         "Available as Technical Report CMU-CS-98-154",
  URL =          "http://reports-archive.adm.cs.cmu.edu/anon/1998/abstracts/98-154.html",
  keywords =     "lf, pcc",
}

@Manual{Pfenning98guide,
  title =        "Twelf User's Guide",
  author =       "Frank Pfenning and Carsten Sch{\"u}rmann",
  edition =      "1.2",
  year =         "1998",
  month =        sep,
  note =         "Available as Technical Report CMU-CS-98-173",
  urlhtml =      "http://www.cs.cmu.edu/~twelf/guide/",
  URL =          "http://reports-archive.adm.cs.cmu.edu/anon/1998/abstracts/98-173.html",
  keywords =     "lf",
}

@InProceedings{Pfenning98cade,
  author =       "Frank Pfenning",
  title =        "Reasoning About Deductions in Linear Logic",
  editor =       "Claude Kirchner and H{\'e}l{\`e}ne Kirchner",
  pages =        "1--2",
  booktitle =    "Proceedings of the International Conference on
                 Automated Deduction",
  year =         "1998",
  publisher =    "Springer-Verlag LNCS 1421",
  address =      "Lindau, Germany",
  month =        jul,
  note =         "Abstract for invited talk",
  urlps =        "http://www.cs.cmu.edu/~fp/papers/cade98inv.ps.gz",
  keywords =     "lf",
}

@InProceedings{Schurmann98cade,
  author =       "Carsten Sch{\"u}rmann and Frank Pfenning",
  title =        "Automated Theorem Proving in a Simple Meta-Logic for
                 {LF}",
  editor =       "Claude Kirchner and H{\'e}l{\`e}ne Kirchner",
  pages =        "286--300",
  booktitle =    "Proceedings of the International Conference on
                 Automated Deduction",
  year =         "1998",
  publisher =    "Springer-Verlag LNCS 1421",
  address =      "Lindau, Germany",
  month =        jul,
  urlps =        "http://www.cs.cmu.edu/~fp/papers/cade98m2.ps.gz",
  keywords =     "lf",
}

@InProceedings{Pfenning98pstt,
  author =       "Frank Pfenning and Carsten Sch{\"u}rmann",
  title =        "Algorithms for Equality and Unification in the
                 Presence of Notational Definitions",
  editor =       "D. Galmiche",
  booktitle =    "Proceedings of the {CADE} Workshop on Proof Search in
                 Type-Theoretic Languages",
  year =         "1998",
  publisher =    "Electronic Notes in Theoretical Computer Science",
  month =        jul,
  urlps =        "http://www.cs.cmu.edu/~fp/papers/strict98.ps.gz",
  keywords =     "lf",
}

@InProceedings{Necula98lics,
  author =       "George C. Necula and Peter Lee",
  title =        "Efficient Representation and Validation of Logical
                 Proofs",
  booktitle =    "Proceedings of the Symposium on Logic in Computer
                 Science",
  editor =       "Vaughan Pratt",
  pages =        "93--104",
  year =         "1998",
  publisher =    "IEEE Computer Society Press",
  address =      "Indianapolis, Indiana",
  month =        jun,
  annote =       "Extended version available as \cite{Necula97tr172}",
  urlps =        "http://foxnet.cs.cmu.edu/papers/necula-lics98.ps",
  urlabstract =  "http://foxnet.cs.cmu.edu/papers/necula-lics98.abstract",
  keywords =     "lf, pcc",
}

@InProceedings{Necula98pldi,
  author =       "George C. Necula and Peter Lee",
  title =        "The Design and Implementation of a Certifying
                 Compiler",
  editor =       "Keith D. Cooper",
  pages =        "333--344",
  booktitle =    "Proceedings of the Conference on Programming Language
                 Design and Implementation",
  year =         "1998",
  publisher =    "ACM Press",
  address =      "Montreal, Canada",
  month =        jun,
  urlps =        "http://foxnet.cs.cmu.edu/papers/necula-pldi98.ps",
  urlabstract =  "http://foxnet.cs.cmu.edu/papers/necula-pldi98.abstract",
  keywords =     "lf, pcc",
}

@InProceedings{Pfenning98types,
  author =       "Frank Pfenning and Carsten Sch{\"u}rmann",
  title =        "Algorithms for Equality and Unification in the
                 Presence of Notational Definitions",
  editor =       "T. Altenkirch and W. Naraschewski and B. Reus",
  booktitle =    "Proceedings of the Workshop on Types for Proofs and
                 Programs",
  month =        mar,
  year =         "1998",
  pages =        "179--193",
  address =      "Kloster Irsee, Germany",
  publisher =    "Springer-Verlag LNCS 1657",
  urlps =        "http://www.cs.cmu.edu/~fp/papers/types98.ps.gz",
  keywords =     "lf",
}

@Article{Harper98jlc,
  author =       "Robert Harper and Frank Pfenning",
  title =        "A Module System for a Programming Language Based on
                 the {LF} Logical Framework",
  journal =      "Journal of Logic and Computation",
  year =         "1998",
  month =        feb,
  volume =       "8",
  number =       "1",
  pages =        "5--31",
  keywords =     "lf",
}

@Unpublished{Pfenning97un,
  author =       "Frank Pfenning",
  title =        "Computation and Deduction",
  year =         "1997",
  note =         "Early draft of book to be published by Cambridge
                 University Press",
  urlps =        "http://www.cs.cmu.edu/~twelf/notes/cd.ps",
  month =        apr,
  keywords =     "lf",
}

@TechReport{Necula97tr172,
  author =       "George C. Necula and Peter Lee",
  title =        "Efficient Representation and Validation of Logical
                 Proofs",
  institution =  "School of Computer Science, Carnegie Mellon
                 University",
  year =         "1997",
  number =       "CMU-CS-97-172",
  month =        oct,
  URL =          "http://reports-archive.adm.cs.cmu.edu/anon/1997/abstracts/97-172.html",
  keywords =     "lf, pcc",
}

@TechReport{Cervesato97tr160,
  author =       "Iliano Cervesato and Frank Pfenning",
  title =        "Linear Higher-Order Pre-Unification",
  institution =  "School of Computer Science, Carnegie Mellon
                 University",
  year =         "1997",
  number =       "CMU-CS-97-160",
  month =        jul,
  annote =       "Extended version of~\cite{Cervesato97lics}",
  URL =          "http://reports-archive.adm.cs.cmu.edu/anon/1997/abstracts/97-160.html",
  keywords =     "lf",
}

@InProceedings{Cervesato97lics,
  author =       "Iliano Cervesato and Frank Pfenning",
  title =        "Linear Higher-Order Pre-Unification",
  editor =       "Glynn Winskel",
  booktitle =    "Proceedings of the Symposium on Logic in Computer
                 Science",
  pages =        "422--433",
  year =         "1997",
  publisher =    "IEEE Computer Society Press",
  address =      "Warsaw, Poland",
  month =        jun,
  annote =       "Revised version of~\cite{Cervesato96pstt}",
  urldvi =       "http://www.cs.cmu.edu/~fp/papers/lics97.dvi.gz",
  urlps =        "http://www.cs.cmu.edu/~fp/papers/lics97.ps.gz",
  keywords =     "lf",
}

@TechReport{Cervesato97tr125,
  author =       "Iliano Cervesato and Frank Pfenning",
  title =        "A Linear Spine Calculus",
  institution =  "School of Computer Science, Carnegie Mellon
                 University",
  year =         "1997",
  number =       "CMU-CS-97-125",
  month =        apr,
  URL =          "http://reports-archive.adm.cs.cmu.edu/anon/1997/abstracts/97-125.html",
  keywords =     "lf",
}

@InProceedings{Necula97popl,
  author =       "George C. Necula",
  title =        "Proof-Carrying Code",
  booktitle =    "Proceedings of the Symposium on Principles of
                 Programming Languages",
  year =         "1997",
  publisher =    "ACM Press",
  address =      "Paris, France",
  month =        jan,
  editor =       "Neil D. Jones",
  pages =        "106--119",
  urlps =        "http://foxnet.cs.cmu.edu/papers/necula-popl97.ps",
  urlabstract =  "http://foxnet.cs.cmu.edu/papers/necula-popl97.abstract",
  keywords =     "lf, pcc",
}

@InProceedings{Necula96osdi,
  author =       "George C. Necula and Peter Lee",
  title =        "Safe Kernel Extensions Without Run-Time Checking",
  booktitle =    "Proceedings of the Symposium on Operating System
                 Design and Implementation",
  year =         "1996",
  address =      "Seattle, Washington",
  month =        oct,
  pages =        "229--243",
  urlps =        "http://foxnet.cs.cmu.edu/papers/necula-osdi96.ps",
  urlhtml =      "http://foxnet.cs.cmu.edu/papers/necula-osdi96/osdi.html",
  urlabstract =  "http://foxnet.cs.cmu.edu/papers/necula-osdi96.abstract",
  keywords =     "lf, pcc",
}

@TechReport{Necula96tr165,
  author =       "George C. Necula and Peter Lee",
  title =        "Proof-Carrying Code",
  institution =  "School of Computer Science, Carnegie Mellon
                 University",
  year =         "1996",
  number =       "CMU-CS-96-165",
  month =        sep,
  URL =          "http://foxnet.cs.cmu.edu/papers/necula-ppctr.ps",
  urlabstract =  "http://foxnet.cs.cmu.edu/papers/necula-ppctr.abstract",
  keywords =     "lf, pcc",
}

@InProceedings{Cervesato96pstt,
  author =       "Iliano Cervesato and Frank Pfenning",
  title =        "Linear Higher-Order Pre-Unification",
  editor =       "D. Galmiche",
  booktitle =    "Informal Proceedings of the Workshop on Proof Search
                 in Type-Theoretic Language",
  year =         "1996",
  address =      "New Brunswick, New Jersey",
  month =        jul,
  pages =        "41--50",
  urlps =        "http://www.cs.cmu.edu/~fp/papers/pstt96.ps.gz",
  keywords =     "lf",
}

@InProceedings{Cervesato96lics,
  author =       "Iliano Cervesato and Frank Pfenning",
  title =        "A Linear Logical Framework",
  editor =       "E. Clarke",
  booktitle =    "Proceedings of the Symposium on Logic in Computer
                 Science",
  year =         "1996",
  publisher =    "IEEE Computer Society Press",
  address =      "New Brunswick, New Jersey",
  month =        jul,
  pages =        "264--275",
  note =         "This work also appeared as Preprint 1834 of the
                 Department of Mathematics of Technical University of
                 Darmstadt, Germany",
  urldvi =       "http://www.cs.cmu.edu/~fp/papers/lics96.dvi.gz",
  urlps =        "http://www.cs.cmu.edu/~fp/papers/lics96.ps.gz",
  keywords =     "lf",
}

@InProceedings{Pfenning96caap,
  author =       "Frank Pfenning",
  title =        "The Practice of Logical Frameworks",
  booktitle =    "Proceedings of the Colloquium on Trees in Algebra and
                 Programming",
  editor =       "H{\'e}l{\`e}ne Kirchner",
  year =         "1996",
  publisher =    "Springer-Verlag LNCS 1059",
  address =      "Link{\"o}ping, Sweden",
  month =        apr,
  pages =        "119--134",
  note =         "Invited talk",
  urldvi =       "http://www.cs.cmu.edu/~fp/papers/caap96.dvi.gz",
  urlps =        "http://www.cs.cmu.edu/~fp/papers/caap96.ps.gz",
  keywords =     "lf",
}

@InProceedings{Rohwedder96esop,
  author =       "Ekkehard Rohwedder and Frank Pfenning",
  title =        "Mode and Termination Checking for Higher-Order Logic
                 Programs",
  editor =       "Hanne Riis Nielson",
  booktitle =    "Proceedings of the European Symposium on Programming",
  year =         "1996",
  publisher =    "Springer-Verlag LNCS 1058",
  address =      "Link{\"o}ping, Sweden",
  month =        apr,
  pages =        "296--310",
  urlps =        "http://www.cs.cmu.edu/~fp/papers/esop96.ps.gz",
  keywords =     "lf",
}

@InProceedings{Cervesato96elp,
  author =       "Iliano Cervesato and Joshua S. Hodas and Frank
                 Pfenning",
  title =        "Efficient Resource Management for Linear Logic Proof
                 Search",
  editor =       "R. Dyckhoff and H. Herre and P. Schroeder-Heister",
  booktitle =    "Proceedings of the International Workshop on
                 Extensions of Logic Programming",
  year =         "1996",
  pages =        "67--81",
  publisher =    "Springer-Verlag LNAI 1050",
  address =      "Leipzig, Germany",
  month =        mar,
  URL =          "http://www.cs.stanford.edu/~iliano/papers/elp96.ps.gz",
  keywords =     "lf",
}

@Article{Harper93jacm,
  author =       "Robert Harper and Furio Honsell and Gordon Plotkin",
  title =        "A Framework for Defining Logics",
  journal =      "Journal of the ACM",
  year =         "1993",
  volume =       "40",
  number =       "1",
  month =        jan,
  pages =        "143--184",
  urlps =        "http://www.cs.cmu.edu/~rwh/papers/lf/jacm93.ps",
  urlpdf =       "http://www.cs.cmu.edu/~rwh/papers/lf/jacm93.pdf",
  keywords =     "lf",
}