
The Fox Project
Logical Frameworks / Bibliography
This is a bibliography of research papers and reports related to
logical frameworks from the Fox project at Carnegie Mellon University.
The BibTeX source is available. This is only
indirectly related to Frank Pfenning's much more extensive 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 URLs for papers and
implementations are welcome.
Last updated: Fri May 4 2001

Iliano Cervesato, Joshua S. Hodas, and Frank Pfenning.
Efficient resource management for linear logic proof search.
In R. Dyckhoff, H. Herre, and P. SchroederHeister, editors, Proceedings of the International Workshop on Extensions of Logic
Programming, pages 6781, Leipzig, Germany, March 1996. SpringerVerlag
LNAI 1050.
Available electronically.

Iliano Cervesato, Joshua S. Hodas, and Frank Pfenning.
Efficient resource management for linear logic proof search.
Theoretical Computer Science, 232(12):133163, February
2000.
Available electronically.

Iliano Cervesato and Frank Pfenning.
Linear higherorder preunification.
Submitted for publication to the Journal of Symbolic
Computation.

Iliano Cervesato and Frank Pfenning.
A linear logical framework.
Submitted for publication to Information and Computation.
Available electronically.

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

Iliano Cervesato and Frank Pfenning.
A linear logical framework.
In E. Clarke, editor, Proceedings of the Symposium on Logic in
Computer Science, pages 264275, New Brunswick, New Jersey, July 1996. IEEE
Computer Society Press.
This work also appeared as Preprint 1834 of the Department of
Mathematics of Technical University of Darmstadt, Germany.
Available electronically
(DVI,
Postscript).

Iliano Cervesato and Frank Pfenning.
Linear higherorder preunification.
Technical Report CMUCS97160, School of Computer Science, Carnegie
Mellon University, July 1997.
Available electronically.

Iliano Cervesato and Frank Pfenning.
Linear higherorder preunification.
In Glynn Winskel, editor, Proceedings of the Symposium on Logic
in Computer Science, pages 422433, Warsaw, Poland, June 1997. IEEE
Computer Society Press.
Available electronically
(DVI,
Postscript).

Iliano Cervesato and Frank Pfenning.
A linear spine calculus.
Technical Report CMUCS97125, School of Computer Science, Carnegie
Mellon University, April 1997.
Available electronically.

Christopher Colby, Karl Crary, Robert Harper, Peter Lee, and Frank Pfenning.
Automated techniques for provably safe mobile code.
To appear in a special issue of Theoretical Computer Science on Dependable Computing.
Available electronically
(Abstract,
Postscript,
PDF).

Christopher Colby, Peter Lee, George C. Necula, Fred Blau, Mark Plesko, and
Kenneth Cline.
A certifying compiler for Java.
In Proceedings of the Conference on Programming Language Design
and Implementation, pages 95107, Vancouver, Canada, June 2000. ACM Press.
Available electronically.

Karl Crary, Robert Harper, Peter Lee, and Frank Pfenning.
Automated techniques for provably safe mobile code.
In Proceedings of the DARPA Information Survivability
Conference and Exposition, volume 1, pages 406419, Hilton Head Island,
South Carolina, January 2000. IEEE Computer Society Press.
Available electronically.

Robert Harper, Furio Honsell, and Gordon Plotkin.
A framework for defining logics.
Journal of the ACM, 40(1):143184, January 1993.
Available electronically
(Postscript,
PDF).

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, February 1998.

Robert Harper and Frank Pfenning.
On equivalence and canonical forms in the LF type theory (extended
abstract).
In Amy Felty, editor, Proceedings of the Workshop on Logical
Frameworks and MetaLanguages, Paris, France, September 1999.
Available electronically
(Abstract,
Postscript).

Robert Harper and Frank Pfenning.
On equivalence and canonical forms in the LF type theory.
Technical Report CMUCS99159, School of Computer Science, Carnegie
Mellon University, September 1999.
Available electronically
(Abstract,
Postscript,
PDF).

Robert Harper and Frank Pfenning.
On equivalence and canonical forms in the LF type theory.
Technical Report CMUCS00148, School of Computer Science, Carnegie
Mellon University, July 2000.
Available electronically
(Abstract,
Postscript,
PDF).

George C. Necula.
Proofcarrying code.
In Neil D. Jones, editor, Proceedings of the Symposium on
Principles of Programming Languages, pages 106119, Paris, France, January
1997. ACM Press.
Available electronically
(Abstract,
Postscript).

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

George C. Necula and Peter Lee.
Proofcarrying code.
Technical Report CMUCS96165, School of Computer Science, Carnegie
Mellon University, September 1996.
Available electronically
(Abstract).

George C. Necula and Peter Lee.
Safe kernel extensions without runtime checking.
In Proceedings of the Symposium on Operating System Design and
Implementation, pages 229243, Seattle, Washington, October 1996.
Available electronically
(Abstract,
HTML,
Postscript).

George C. Necula and Peter Lee.
Efficient representation and validation of logical proofs.
Technical Report CMUCS97172, School of Computer Science, Carnegie
Mellon University, October 1997.
Available electronically.

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, pages 333344, Montreal,
Canada, June 1998. ACM Press.
Available electronically
(Abstract,
Postscript).

George C. Necula and Peter Lee.
Efficient representation and validation of logical proofs.
In Vaughan Pratt, editor, Proceedings of the Symposium on Logic
in Computer Science, pages 93104, Indianapolis, Indiana, June 1998. IEEE
Computer Society Press.
Available electronically
(Abstract,
Postscript).

George C. Necula and Peter Lee.
Proof generation in the Touchstone theorem prover.
In David McAllester, editor, Proceedings of the International
Conference on Automated Deduction, pages 2544, Pittsburgh, Pennsylvania,
June 2000. SpringerVerlag LNAI 1831.
Available electronically.

Frank Pfenning.
Logical frameworks.
In press. Chapter 16 of Alan Robinson and Andrei Voronkov, editors,
Handbook of Automated Reasoning, to be published by Elsevier Science
and MIT Press.

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 electronically
(DVI,
Postscript).

Frank Pfenning.
Computation and deduction.
Early draft of book to be published by Cambridge University Press,
April 1997.
Available electronically.

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

Frank Pfenning.
Logical and metalogical frameworks.
In G. Nadathur, editor, Proceedings of the International
Conference on Principles and Practice of Declarative Programming, page 206,
Paris, France, September 1999. SpringerVerlag LNCS 1702.
Abstract of invited talk.
Available electronically.

Frank Pfenning.
Structural cut elimination I. intuitionistic and classical logic.
Information and Computation, 157(1/2):84141, March 2000.
Available electronically.

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 electronically.

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, Proceedings of the Workshop on Types for Proofs and Programs, pages
179193, Kloster Irsee, Germany, March 1998. SpringerVerlag LNCS 1657.
Available electronically.

Frank Pfenning and Carsten Schürmann.
Twelf User's Guide, 1.2 edition, September 1998.
Available as Technical Report CMUCS98173.
Available electronically
(HTML).

Frank Pfenning and Carsten Schürmann.
System description: Twelf  A metalogical framework for
deductive systems.
In H. Ganzinger, editor, Proceedings of the International
Conference on Automated Deduction, pages 202206, Trento, Italy, July 1999.
SpringerVerlag LNAI 1632.
Available electronically.

Brigitte Pientka and Frank Pfenning.
Termination and reduction checking in the logical framework.
In Carsten Schürmann, editor, Proceedings of the CADE
Workshop on Automation of Proofs by Mathematical Induction, Pittsburgh,
Pennsylvania, June 2000.
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 electronically.

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

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
Conference on Mathematical Foundations of Programming Semantics, New
Orleans, Louisiana, April 1999.
Electronic Notes in Theoretical Computer Science, Volume 20.
Available electronically.

Jeff Polakow and Frank Pfenning.
Properties of terms in continuationpassing style in an ordered
logical framework.
In Joëlle Despeyroux, editor, Proceedings of the Workshop on
Logical Frameworks and Metalanguages, Santa Barbara, California, June 2000.
Available electronically.

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 electronically.

Carsten Schürmann.
Automating the Meta Theory of Deductive Systems.
PhD thesis, Department of Computer Science, Carnegie Mellon
University, August 2000.
Available as Technical Report CMUCS00146.
Available electronically.

Carsten Schürmann.
A meta logical framework based on realizability.
In Joëlle Despeyroux, editor, Proceedings of the Workshop on
Logical Frameworks and MetaLanguages, Santa Barbara, California, June 2000.
Available electronically.

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 International Conference on Automated Deduction, pages
286300, Lindau, Germany, July 1998. SpringerVerlag LNCS 1421.
Available electronically.

Roberto Virga.
HigherOrder Rewriting with Dependent Types.
PhD thesis, Department of Mathematical Sciences, Carnegie Mellon
University, September 1999.
Available as Technical Report CMUCS99167.
Available electronically
(DVI,
Postscript,
PDF).
[ Home
 Contact Information
 Publications
 Researchers
]
[ FoxNet
 Typed Intermediate Languages
 ProofCarrying Code
]
[ Logical Frameworks
 Staged Computation
 Language Design
]
Fox_Project@cs.cmu.edu
http://www.cs.cmu.edu/~fox/
