Bibliography on LF and Elf
This is a bibliography on the LF logical framework, the logic programming
language Elf which is based on LF, and the Twelf metalogical framework (which
includes an implementation of Elf). It is a selection of papers from a more
general bibliography on
logical frameworks. Papers with known URLs in the WorldWide Web have
been annotated with their location and can be previewed or retrieved directly.
Corrections, additions, and new URL's for papers and implementations are
welcome.
Some pointers to basic references:
Last Updated: Tue Aug 3 1999
Compiled by Frank
Pfenning
fp@cs

Penny Anderson.
Program Derivation by Proof Transformation.
PhD thesis, Carnegie Mellon University, October 1993.
Available as Technical Report CMUCS93206.
Available electronically.

Penny Anderson.
Program extraction in a logical framework setting.
In Frank Pfenning, editor, Proceedings of the 5th International
Conference on Logic Programming and Automated Reasoning, pages 144158,
Kiev, Ukraine, July 1994. SpringerVerlag LNAI 822.

Penny Anderson.
Representing proof transformations for program optimization.
In Proceedings of the 12th International Conference on Automated
Deduction, pages 575589, Nancy, France, June 1994. SpringerVerlag LNAI
814.
Available electronically.

Andrew W. Appel and Edward W. Felten.
Proofcarrying authentication.
In G. Tsudik, editor, Proceedings of the 6th Conference on
Computer and Communications Security, Singapore, November 1999. ACM Press.
To appear.

Andrew W. Appel and Amy P. Felty.
Lightweight lemmas in lambda prolog.
In Danny De Schreye, editor, Proceedings of the International
Conference on Logic Programming (ICLP'99), Las Cruces, New Mexico, December
1999. MIT Press.
To appear.

Andrew W. Appel and Amy P. Felty.
A semantic model of types and machine instructions for proofcarrying
code.
Submitted, July 1999.

David Aspinall and Adriana Compagnoni.
Subtyping dependent types.
In E. Clarke, editor, Proceedings of the 11th Annual Symposium
on Logic in Computer Science, pages 8697, New Brunswick, New Jersey, July
1996. IEEE Computer Society Press.

Arnon Avron, Furio A. Honsell, Ian A. Mason, and Robert Pollack.
Using typed lambda calculus to implement formal systems on a machine.
Journal of Automated Reasoning, 9(3):309354, 1992.
A preliminary version appeared as University of Edinburgh Report
ECSLFCS8731.

Jason J. Brown.
Presentations of Unification in a Logical Framework.
PhD thesis, University of Oxford, January 1996.

Rod Burstall and Furio Honsell.
Operational semantics in a natural deduction setting.
In Gérard Huet and Gordon Plotkin, editors, Logical
Frameworks, pages 185214. Cambridge University Press, 1991.

Iliano Cervesato.
A Linear Logical Framework.
PhD thesis, Dipartimento di Informatica, Università di Torino,
February 1996.

Iliano Cervesato.
Prooftheoretic foundation of compilation in logic programming
languages.
In J. Jaffar, editor, Proceedings of the 1998 Joint
International Conference and Symposium on Logic Programming (JICSLP'98),
pages 115129, Manchester, UK, June 1998. MIT Press.
Available in PostScript format.

Iliano Cervesato, Joshua S. Hodas, and Frank Pfenning.
Efficient resource management for linear logic proof search.
Theoretical Computer Science, 1997.
To appear in a special issue on Proof Search in TypeTheoretic
Languages, D. Galmiche, editor.
Available in PostScript format.

Iliano Cervesato and Frank Pfenning.
Linear higherorder preunification.
In D. Galmiche, editor, Informal Proceedings of the Workshop on
Proof Search in TypeTheoretic Language, New Brunswick, New Jersey, July
1996.
Available in PostScript format.

Iliano Cervesato and Frank Pfenning.
A linear logical framework.
In E. Clarke, editor, Proceedings of the Eleventh Annual
Symposium on Logic in Computer Science, pages 264275, New Brunswick, New
Jersey, July 1996. IEEE Computer Society Press.
Available in DVI and
PostScript formats.

Iliano Cervesato and Frank Pfenning.
Linear higherorder preunification.
In Glynn Winskel, editor, Proceedings of the Twelfth Annual
Sumposium on Logic in Computer Science (LICS'97), pages 422433, Warsaw,
Poland, June 1997. IEEE Computer Society Press.
Available in DVI and
PostScript formats.

Iliano Cervesato and Frank Pfenning.
A linear spine calculus.
Technical Report CMUCS97125, Department of Computer Science,
Carnegie Mellon University, April 1997.
Available in PostScript format.

Iliano Cervesato and Frank Pfenning.
A linear logical framework.
Information and Computation, 1998.
To appear in a special issue with invited papers from LICS'96, E.
Clarke, editor.
Available in PostScript format.

Thierry Coquand.
An algorithm for testing conversion in type theory.
In Gérard Huet and Gordon Plotkin, editors, Logical
Frameworks, pages 255279. Cambridge University Press, 1991.

Olivier Danvy and Frank Pfenning.
The occurrence of continuation parameters in CPS terms.
Technical Report CMUCS95121, Department of Computer Science,
Carnegie Mellon University, February 1995.
Available in PostScript format.

Gilles Dowek.
The undecidability of typability in the lambdapicalculus.
In M. Bezem and J.F. Groote, editors, Proceedings of the
International Conference on Typed Lambda Calculi and Applications, pages
139145, Utrecht, The Netherlands, March 1993. SpringerVerlag LNCS 664.

Gilles Dowek, Gérard Huet, and Benjamin Werner.
On the definition of the etalong normal form in type systems of the
cube.
In Herman Geuvers, editor, Informal Proceedings of the Workshop
on Types for Proofs and Programs, Nijmegen, The Netherlands, May 1993.
Available in PostScript format.

Conal Elliott.
Higherorder unification with dependent types.
In N. Dershowitz, editor, Rewriting Techniques and
Applications, pages 121136, Chapel Hill, North Carolina, April 1989.
SpringerVerlag LNCS 355.
Available in PostScript format.

Conal Elliott and Frank Pfenning.
A semifunctional implementation of a higherorder logic programming
language.
In Peter Lee, editor, Topics in Advanced Language
Implementation, pages 289325. MIT Press, 1991.
Available electronically.

Conal M. Elliott.
Extensions and Applications of HigherOrder Unification.
PhD thesis, School of Computer Science, Carnegie Mellon University,
May 1990.
Available as Technical Report CMUCS90134.
Available in DVI and
PostScript formats.

Amy Felty.
Encoding dependent types in an intuitionistic logic.
In Gérard Huet and Gordon D. Plotkin, editors, Logical
Frameworks, pages 214251. Cambridge University Press, 1991.
Available in PostScript format.

Amy Felty and Dale Miller.
Encoding a dependenttype lambdacalculus in a logic programming
language.
In M.E. Stickel, editor, 10th International Conference on
Automated Deduction, pages 221235, Kaiserslautern, Germany, July 1990.
SpringerVerlag LNCS 449.
Available in PostScript format.

Philippa Gardner.
Representing Logics in Type Theory.
PhD thesis, University of Edinburgh, July 1992.
Available as Technical Report CST9392.

Philippa Gardner.
A new type theory for representing logics.
In Andrei Voronkov, editor, Proceedings of the 4th International
Conference on Logic Programming and Automated Reasoning (LPAR'93), pages
146157, St. Petersburg, Russia, July 1993. SpringerVerlag LNAI 698.

Wolfgang Gehrke.
Problems in rewriting applied to categorical concepts by the example
of a computational comonad.
Technical Report CMUCS94207, Carnegie Mellon University,
Pittsburgh, Pennsylvania, October 1994.
Available in DVI format.

Wolfgang Gehrke.
Proof of the decidability of the uniform word problem for monads
assisted by Elf.
Technical Report 9466, RISC, Linz, Austria, August 1994.
Available in DVI format.

Wolfgang Gehrke.
Decidability Results for Categorical Notions Related to Monads
by Rewriting Techniques.
PhD thesis, Research Institute for Symbolic Computation, Linz,
Austria, May 1995.
Available as RISC Report Number 9530.
Available in PostScript format.

Wolfgang Gehrke.
Problems in rewriting applied to categorical concepts by the example
of a computational comonad.
In Jieh Hsiang, editor, Proceedings of the Sixth International
Conference on Rewriting Techniques and Applications, pages 210224,
Kaiserslautern, Germany, April 1995. SpringerVerlag LNCS 914.
Available in PostScript format.

Herman Geuvers.
The ChurchRosser property for betaetareduction in typed
lambdacalculi.
In A. Scedrov, editor, Seventh Annual IEEE Symposium on Logic
in Computer Science, pages 453460, Santa Cruz, California, June 1992.

Healfdene Goguen.
Soundness of the logical framework for its typed operational
semantics.
In JeanYves Girard, editor, Proceedings of the 4th
International Conference on Typed Lambda Calculi and Applications (TLCA'99),
pages 177197, L'Aquila, Italy, April 1999. SpringerVerlag LNCS 1581.

John Hannan.
Searching for semantics.
In D. Schmidt, editor, Proceedings of the ACM SIGPLAN Symposium
on Partial Evaluation and Semantics Based Program Manipulation, pages 112,
Copenhagen, Denmark, June 1993.
Available in DVI format.

John Hannan and Frank Pfenning.
Compiler verification in LF.
In Andre Scedrov, editor, Seventh Annual IEEE Symposium on
Logic in Computer Science, pages 407418, Santa Cruz, California, June
1992.
Available in DVI and
PostScript formats.

Robert Harper.
An equational formulation of LF.
Technical Report ECSLFCS8867, University of Edinburgh, 1988.

Robert Harper.
Systems of polymorphic type assignment in LF.
Technical Report CMUCS90144, Carnegie Mellon University,
Pittsburgh, Pennsylvania, June 1990.
Available in DVI format.

Robert Harper, Furio Honsell, and Gordon Plotkin.
A framework for defining logics.
In Symposium on Logic in Computer Science, pages 194204. IEEE
Computer Society Press, June 1987.

Robert Harper, Furio Honsell, and Gordon Plotkin.
A framework for defining logics.
Journal of the Association for Computing Machinery,
40(1):143184, January 1993.
Available in DVI format.

Robert Harper and Frank Pfenning.
A module system for a programming language based on the LF logical
framework.
Journal of Logic and Computation, 8(1):531, 1998.

Robert Harper, Donald Sannella, and Andrzej Tarlecki.
Logic representation.
In D.H. Pitt, D.E. Rydeheard, P. Dybjer, A.M. Pitts, and
A. Poigneé, editors, Proceedings of the Workshop on Category Theory
and Computer Science, pages 250272, Manchester, UK, September 1989.
SpringerVerlag LNCS 389.

Robert Harper, Donald Sannella, and Andrzej Tarlecki.
Structure and representation in LF.
In Fourth Annual Symposium on Logic in Computer Science, pages
226237, Pacific Grove, California, June 1989. IEEE Computer Society Press.

Robert Harper, Donald Sannella, and Andrzej Tarlecki.
Structured presentations and logic representations.
Annals of Pure and Applied Logic, 67:113160, 1994.
Available in PostScript format.

John Hatcliff.
Mechanically verifying the correctness of an offline partial
evaluator.
In M. Hermenegildo and S.D. Swierstra, editors, Proceedings of
the 7th International Symposium on Programming Languages: Implementations,
Logics and Programs, pages 279298, Utrecht, The Netherlands, September
1995. SpringerVerlag LNCS 982.
Available in PostScript format.

Samin Ishtiaq and David Pym.
A relevant analysis of natural deduction.
Journal of Logic and Computation, 8(6):809838, 1998.

Michael Kohlhase and Frank Pfenning.
Unification in a lambdacalculus with intersection types.
In Dale Miller, editor, Proceedings of the International Logic
Programming Symposium, pages 488505, Vancouver, Canada, October 1993. MIT
Press.
Available in DVI and
PostScript formats.

Chuck Liang.
Substitutions for proofs and types as logic programming.
In Didier Galmiche, editor, Informal Proceedings of the Workshop
on Proof Search in TypeTheoretic Languages, pages 6168, New Brunswick,
New Jersey, July 1996.

Ian A. Mason.
Hoare's logic in the LF.
Technical Report ECSLFCS8732, Laboratory for Foundations of
Computer Science, University of Edinburgh, June 1987.

Spiro Michaylov and Frank Pfenning.
Natural semantics and some of its metatheory in Elf.
In L.H. Eriksson, L. Hallnäs, and P. SchroederHeister, editors,
Proceedings of the Second International Workshop on Extensions of Logic
Programming, pages 299344, Stockholm, Sweden, January 1991.
SpringerVerlag LNAI 596.
Available in DVI and
PostScript formats.

Spiro Michaylov and Frank Pfenning.
An empirical study of the runtime behavior of higherorder logic
programs.
In D. Miller, editor, Proceedings of the Workshop on the
lambda Prolog Programming Language, pages 257271, Philadelphia,
Pennsylvania, July 1992. University of Pennsylvania.
Available as Technical Report MSCIS9286.
Available in DVI and
PostScript formats.

Spiro Michaylov and Frank Pfenning.
Higherorder logic programming as constraint logic programming.
In Position Papers for the First Workshop on Principles and
Practice of Constraint Programming, pages 221229, Newport, Rhode Island,
April 1993. Brown University.
Available in PostScript format.

Marino Miculan.
The expressive power of structural operational semantics with
explicit assumptions.
In Henk Barendregt and Tobias Nipkow, editors, Types for Proofs
and Programs, pages 263290. SpringerVerlag LNCS 806, 1994.

Dale Miller, Gordon Plotkin, and David Pym.
A relevant analysis of natural deduction.
Talk given at the Workshop on Logical Frameworks, Båstad, Sweden,
May 1992.

George C. Necula.
Proofcarrying code.
In Neil D. Jones, editor, Conference Record of the 24th
Symposium on Principles of Programming Languages (POPL'97), pages 106119,
Paris, France, January 1997. ACM Press.

George C. Necula.
Compiling with Proofs.
PhD thesis, Carnegie Mellon University, October 1998.
Available as Technical Report CMUCS98154.

George C. Necula and Peter Lee.
Safe kernel extensions without runtime checking.
In Proceedings of the Second Symposium on Operating System
Design and Implementation (OSDI'96), pages 229243, Seattle, Washington,
October 1996.

George C. Necula and Peter Lee.
The design and implementation of a certifying compiler.
In Keith D. Cooper, editor, Proceedings of the Conference on
Programming Language Design and Implementation (PLDI'98), pages 333344,
Montreal, Canada, June 1998. ACM Press.

George C. Necula and Peter Lee.
Efficient representation and validation of logical proofs.
In Proceedings of the 13th Annual Symposium on Logic in Computer
Science (LICS'98), pages 93104, Indianapolis, Indiana, June 1998. IEEE
Computer Society Press.

Frank Pfenning.
Elf: A language for logic definition and verified metaprogramming.
In Fourth Annual Symposium on Logic in Computer Science, pages
313322, Pacific Grove, California, June 1989. IEEE Computer Society Press.
Available in DVI and
PostScript formats.

Frank Pfenning.
Logic programming in the LF logical framework.
In Gérard Huet and Gordon Plotkin, editors, Logical
Frameworks, pages 149181. Cambridge University Press, 1991.
Available in DVI and
PostScript formats.

Frank Pfenning.
Unification and antiunification in the Calculus of
Constructions.
In Sixth Annual IEEE Symposium on Logic in Computer Science,
pages 7485, Amsterdam, The Netherlands, July 1991.
Available in DVI and
PostScript formats.

Frank Pfenning.
Computation and deduction.
Unpublished lecture notes, 277 pp. Revised May 1994, April 1996, May
1992.

Frank Pfenning.
Dependent types in logic programming.
In Frank Pfenning, editor, Types in Logic Programming,
chapter 10, pages 285311. MIT Press, Cambridge, Massachusetts, 1992.

Frank Pfenning.
A proof of the ChurchRosser theorem and its representation in a
logical framework.
Journal of Automated Reasoning, 1993.
To appear. A preliminary version is available as Carnegie Mellon
Technical Report CMUCS92186, September 1992.
Available in DVI and
PostScript formats.

Frank Pfenning.
Refinement types for logical frameworks.
In Herman Geuvers, editor, Informal Proceedings of the Workshop
on Types for Proofs and Programs, pages 285299, Nijmegen, The Netherlands,
May 1993.
Available in DVI and
PostScript formats.

Frank Pfenning.
Elf: A metalanguage for deductive systems.
In A. Bundy, editor, Proceedings of the 12th International
Conference on Automated Deduction, pages 811815, Nancy, France, June 1994.
SpringerVerlag LNAI 814.
System abstract.
Available in DVI and
PostScript formats.

Frank Pfenning.
Structural cut elimination in linear logic.
Technical Report CMUCS94222, Department of Computer Science,
Carnegie Mellon University, December 1994.
Available in PostScript format.

Frank Pfenning.
A structural proof of cut elimination and its representation in a
logical framework.
Technical Report CMUCS94218, Department of Computer Science,
Carnegie Mellon University, November 1994.
Available in DVI and
PostScript formats.

Frank Pfenning.
Structural cut elimination.
In D. Kozen, editor, Proceedings of the Tenth Annual Symposium
on Logic in Computer Science, pages 156166, San Diego, California, June
1995. IEEE Computer Society Press.
Available in PostScript format.

Frank Pfenning.
The practice of logical frameworks.
In Hélène Kirchner, editor, Proceedings of the
Colloquium on Trees in Algebra and Programming, pages 119134,
Linköping, Sweden, April 1996. SpringerVerlag LNCS 1059.
Invited talk.
Available in DVI and
PostScript formats.

Frank Pfenning.
Reasoning about deductions in linear logic.
In Claude Kirchner and Hélène Kirchner, editors, Proceedings of the 15th International Conference on Automated Deduction
(CADE15), pages 12, Lindau, Germany, July 1998. SpringerVerlag LNCS
1421.
Abstract for invited talk.
Available in PostScript format.

Frank Pfenning.
Logical frameworks.
In Alan Robinson and Andrei Voronkov, editors, Handbook of
Automated Reasoning. Elsevier Science Publishers, 1999.
In preparation.

Frank Pfenning.
Computation and Deduction.
Cambridge University Press, 2000.
In preparation. Draft from April 1997 available electronically.
Available in PostScript format.

Frank Pfenning and Ekkehard Rohwedder.
Implementing the metatheory of deductive systems.
In D. Kapur, editor, Proceedings of the 11th International
Conference on Automated Deduction, pages 537551, Saratoga Springs, New
York, June 1992. SpringerVerlag LNAI 607.
Available in DVI and
PostScript formats.

Frank Pfenning and Carsten Schürmann.
Algorithms for equality and unification in the presence of notational
definitions.
In D. Galmiche, editor, Proceedings of the CADE Workshop on
Proof Search in TypeTheoretic Languages. Electronic Notes in Theoretical
Computer Science, July 1998.
Available in PostScript format.

Frank Pfenning and Carsten Schürmann.
Algorithms for equality and unification in the presence of notational
definitions.
In T. Altenkirch, W. Naraschewski, and B. Reus, editors, Types
for Proofs and Programs. SpringerVerlag LNCS 1657, 1998.
To appear.
Available in PostScript format.

Frank Pfenning and Carsten Schürmann.
Twelf User's Guide, 1.2 edition, September 1998.
Available as Technical Report CMUCS98173, Carnegie Mellon
University.

Frank Pfenning and Carsten Schürmann.
System description: Twelf  a metalogical framework for deductive
systems.
In H. Ganzinger, editor, Proceedings of the 16th International
Conference on Automated Deduction (CADE16), pages 202206, Trento, Italy,
July 1999. SpringerVerlag LNAI 1632.
Available in PostScript format.

Luís Pinto and Roy Dyckhoff.
Sequent calculi for the normal terms of the lambdapi and
lambdapisigmacalculi.
In D. Galmiche, editor, Proceedings of the Workshop on Proof
Search in TypeTheoretic Languages, volume 17 of Electronic Notes in
Theoretical Computer Science, Lindau, Germany, July 1998. Elsevier Science.
Available electronically.

Mark Plesko and Frank Pfenning.
A formalization of the proofcarrying code architecture in a linear
logical framework.
In A. Pnueli and P. Traverso, editors, Proceedings of the FLoC
Workshop on RunTime Result Verification, Trento, Italy, July 1999.
Available in PostScript format.

Jeff Polakow and Frank Pfenning.
Natural deduction for intuitionistic noncommutative linear logic.
In J.Y. Girard, editor, Proceedings of the 4th International
Conference on Typed Lambda Calculi and Applications (TLCA'99), pages
295309, L'Aquila, Italy, April 1999. SpringerVerlag LNCS 1581.
Available in PostScript format.

Jeff Polakow and Frank Pfenning.
Relating natural deduction and sequent calculus for intuitionistic
noncommutative linear logic.
In Andre Scedrov and Achim Jung, editors, Proceedings of the
15th Conference on Mathematical Foundations of Programming Semantics, New
Orleans, Louisiana, April 1999.
Electronic Notes in Theoretical Computer Science, Volume 20.
Available in PostScript format.

D. J. Pym.
A note on representation and semantics in logical frameworks.
In Didier Galmiche, editor, Informal Proceedings of the Workshop
on Proof Search in TypeTheoretic Languages, pages 101108, New Brunswick,
New Jersey, July 1996.

David Pym.
Proofs, Search and Computation in General Logic.
PhD thesis, University of Edinburgh, 1990.
Available as CST6990, also published as ECSLFCS90125.

David Pym.
A unification algorithm for the lambdapicalculus.
International Journal of Foundations of Computer Science,
3(3):333378, September 1992.

David Pym and Lincoln Wallen.
Investigations into proofsearch in a system of firstorder dependent
function types.
In M.E. Stickel, editor, Proceedings of the 10th International
Conference on Automated Deduction, pages 236250, Kaiserslautern, Germany,
July 1990. SpringerVerlag LNCS 449.

David Pym and Lincoln A. Wallen.
Proof search in the lambdapicalculus.
In Gérard Huet and Gordon Plotkin, editors, Logical
Frameworks, pages 309340. Cambridge University Press, 1991.

David Pym and Lincoln A. Wallen.
Logic programming via proofvalued computations.
In K. Broda, editor, Proceedings of the 4th UK Annual
Conference on Logic Programming, London, March 1992. SpringerVerlag.

David J. Pym.
A note on the proof theory of the lambdapicalculus.
Studia Logica, 54(2):199230, 1995.

Ekkehard Rohwedder.
Verifying the metatheory of deductive systems.
Thesis Proposal, February 1994.

Ekkehard Rohwedder.
Verifying the MetaTheory of Deductive Systems.
PhD thesis, School of Computer Science, Carnegie Mellon University,
1996.
Forthcoming.

Ekkehard Rohwedder and Frank Pfenning.
Mode and termination checking for higherorder logic programs.
In Hanne Riis Nielson, editor, Proceedings of the European
Symposium on Programming, pages 296310, Linköping, Sweden, April 1996.
SpringerVerlag LNCS 1058.
Available in PostScript format.

Anne Salvesen.
The ChurchRosser theorem for LF with betaetareduction.
Unpublished notes to a talk given at the First Workshop on Logical
Frameworks in Antibes, France, May 1990.

Carsten Schürmann.
A computational meta logic for the Horn fragment of LF.
Master's thesis, Carnegie Mellon University, December 1995.
Available as Technical Report CMUCS95218.

Carsten Schürmann and Frank Pfenning.
Automated theorem proving in a simple metalogic for LF.
In Claude Kirchner and Hélène Kirchner, editors, Proceedings of the 15th International Conference on Automated Deduction
(CADE15), pages 286300, Lindau, Germany, July 1998. SpringerVerlag LNCS
1421.
Available in PostScript format.

Aaron Stump and David L. Dill.
Generating proofs from a decision procedure.
In A. Pnueli and P. Traverso, editors, Proceedings of the FLoC
Workshop on RunTime Result Verification, Trento, Italy, July 1999.

Roberto Virga.
Higherorder superposition for dependent types.
In Harald Ganzinger, editor, Proceedings of the 7th
International Conference on Rewriting Techniques and Applications, pages
123137, New Brunswick, New Jersey, July 1996. SpringerVerlag LNCS 1103.
Extended version available as Technical Report CMUCS95150, May
1995.
Available in PostScript format.

Roberto Virga.
HigherOrder Rewriting with Dependent Types.
PhD thesis, Department of Mathematical Sciences, Carnegie Mellon
University, 1999.
Forthcoming.