Recent Material on Logical Frameworks
This provides pointers to recent papers, implementations, and other items
relating to logical frameworks.
Last Updated: Tue Aug 8 2000
Recent Books

Proof, Language, and Interaction

Essays in Honour of Robin Milner
edited by Gordon Plotkin, Colin Stirling, and Mads Tofte
MIT Press, May 2000
New Personal Home Pages
 Peter Aczel,
petera@cs.man.ac.uk
 Andrew Appel,
appel@princeton.edu
 Arnon Avron,
aa@math.tau.ac.il
 Gilles Barthe,
gilles.barthe@sophia.inria.fr
 Stefano Berardi,
stefano@di.unito.it
 Ulrich Berger,
berger@rz.mathematik.unimuenchen.de
 Marc Bezem,
bezem@phil.uu.nl
 Ana Bove,
bove@cs.chalmers.se
 Adriana Compagnoni,
abc@cs.stevenstech.edu
 Catarina Coquand,
catarina@cs.chalmers.se
 Judicael Courant,
judicael.courant@lri.fr
 Peter Dybjer,
peterd@cs.chalmers.se
 JeanChristophe Filliatre,
filliatr@lri.fr
 Daniel Friedlender,
daniel@brics.dk
 Murdoch Gabbay,
m.j.gabbay@cantab.com
 Veronica Gaspes,
vero@itn.hh.se
 Rajeev Gore,
rpg@arp.anu.edu.au
 Hugo Herbelin,
hugo.herbelin@inria.fr
 Martin Hofmann,
mxh@dcs.ed.ac.uk
 Furio Honsell,
honsell@dimi.uniud.it
 Douglas Howe,
howe@research.belllabs.com
 Samin Ishtiaq,
si@dcs.qmw.ac.uk
 JeanPierre Jouannaud,
jouannau@lri.fr
 Claude Kirchner,
claude.kirchner@loria.fr
 Hélène Kirchner,
helene.kirchner@loria.fr
 Connor McBride,
ctm@dcs.ed.ac.uk
 Raymond McDowell,
mcdowell@kzoo.edu
 James McKinna,
j.h.mckinna@durham.ac.uk
 Marino Miculan,
miculan@dimi.uniud.it
 Mitsuhiro Okada,
mitsu@abelard.flet.keio.ac.jp
 Michel Parigot,
parigot@logique.jussieu.fr
 Christine Paulin,
christine.paulin@lri.fr
 Andrew Pitts,
ap@cl.cam.ac.uk
 Mark Plesko,
mp5f@cs.cmu.edu
 Aarne Ranta,
aarne@cs.chalmers.se
 Giovanni Sambin,
sambin@math.unipd.it
 Alan Smaill,
A.Smaill@ed.ac.uk
 Jan Smith,
smith@cs.chalmers.se
 Aaron Stump,
stump@cs.stanford.edu
 Nora Szasz,
nora@fing.edu.uy
 Markus Wenzel,
wenzelm@in.tum.de
 Vincent van Oostrom,
oostrom@phil.uu.nl
 Jan von Plato,
vonplato@helsinki.fi
New Implementation Home Pages
 Twelf, a metalogical
framework based on LF. Includes an implementation of Elf.
 Yarrow Proof
Assistant for Pure Type Systems.
 Proof General, a
generic Emacs interface for proof assistants. It is supplied readycustomised
for Coq, Isabelle and LEGO.
 Maude, a reflective language and
system supporting equational and rewriting logic specfication and programming.
 AF2 Proof
Assistant for secondorder intuitionistic logic.
New Related Pointers
Recent Publications
Also included are some older references recently added to the bibliography.
Deleted for the moment while I am updating the master bibliography.

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.

Sergei N. Artemov.
On explicit reflection in theorem proving and formal verification.
In Harald Ganzinger, editor, Proceedings of the 16th
International Conference on Automated Deduction (CADE16), pages 267281,
Trento, Italy, July 1999. SpringerVerlag LNAI 1632.

Clemens Ballarin and Lawrence C. Paulson.
Reasoning about coding theory: The benefits we get from computer
algebra.
In J. Calmet and J. Plaze, editors, Proceedings of the
International Conference on Artificial Intelligence and Symbolic Computation
(AISC'98), pages 5566, Plattsburgh, New York, September 1998.
SpringerVerlag LNAI 1476.
Available in DVI format.

David Basin, Seán Matthews, and Luca Viganò.
Labelled modal logic: Quantifiers.
Journal of Logic, Language, and Information, 7(3):237263,
July 1998.

David Basin, Seán Matthews, and Luca Viganò.
A modular presentation of modal logics in a logical framework.
In The Tbilisi Symposium on Language, Logic and Computation:
Selected Papers. CSLI Publications, 1998.
Available electronically.

Giampaolo Bella and Lawrence C. Paulson.
Kerberos version IV: Inductive analysis of the secrecy goals.
In J.J. Quisquater, editor, Proceedings of the 5th European
Symposium on Research in Computer Security, pages 361375,
LouvainlaNeuve, Belgium, September 1998. SpringerVerlag LNCS 1485.
Available in PostScript format.

Giampaolo Bella and Lawrence C. Paulson.
Machanising BAN Kerberos by the inductive method.
In A.J. Hu and M.Y. Vardi, editors, Proceedings of the 10th
International Conference on ComputerAided Verification (CAV'98), pages
416427, Vancouver, B.C., Canada, June 1998. SpringerVerlag LNCS 1427.
Available in PostScript format.

Frédéric Blanqui, JeanPierre Jouannaud, and Mitsuhiro Okada.
The calculus of algebraic constructions.
In P. Narendran and M. Rusinowitch, editors, Proceedings of the
10th International Conference on Rewriting Techniques and Applications
(RTA99), pages 301316, Trento, Italy, July 1999. SpringerVerlag LNCS
1631.
Available in PostScript format.

Peter Borovanský, Claude Kirchner, Hélène Kirchner, PierreEtienne
Moreau, and Christophe Ringeissen.
An overview of ELAN.
In Claude Kirchner and Hélène Kirchner, editors, Proceedings of the International Workshop on Rewriting Logic and its
Applications, volume 15 of Electronic Notes in Theoretical Computer
Science, PontàMousson, France, September 1998. Elsevier Science.
Available electronically.

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

M. Clavel, F. Durán, S. Eker, P. Lincoln, N. MartíOliet, J. Meseguer,
and J.F. Quesada.
The Maude system.
In P. Narendran and M. Rusinowitch, editors, Proceedings of the
10th International Conference on Rewriting Techniques and Applications
(RTA99), pages 240243, Trento, Italy, July 1999. SpringerVerlag LNCS
1631.
System Description.

Judicaël Courant.
MC: a modular calculus for Pure Type Systems.
Rapport de Recherche 1217, CNRS Université Paris Sud, June 1999.

Gilles Dowek, Thérèse Hardin, and Claude Kirchner.
HOLlambdasigma: An intentional firstorder expression of
higherorder logic.
In P. Narendran and M. Rusinowitch, editors, Proceedings of the
10th International Conference on Rewriting Techniques and Applications
(RTA99), pages 317331, Trento, Italy, July 1999. SpringerVerlag LNCS
1631.

Marcelo Fiore, Gordon Plotkin, and Daniele Turi.
Abstract syntax and variable binding.
In G. Longo, editor, Proceedings of the 14th Annual Symposium on
Logic in Computer Science (LICS'99), pages 193202, Trento, Italy, July
1999. IEEE Computer Society Press.

Jacques D. Fleuriot and Lawrence C. Paulson.
A combination of nonstandard analysis and geometry theorem proving,
with application to Newton's Principia.
In C. Kirchner and H. Kirchner, editors, Proceedings of the 15th
International Conference on Automated Deduction (CADE15), pages 316,
Lindau, Germany, July 1998. SpringerVerlag LNAI 1421.

Murdoch Gabbay and Andrew Pitts.
A new approach to abstract syntax involving binders.
In G. Longo, editor, Proceedings of the 14th Annual Symposium on
Logic in Computer Science (LICS'99), pages 214224, Trento, Italy, July
1999. IEEE Computer Society Press.

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.

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.

Masahito Hasegawa.
Logical predicates for intuitionistic linear type theories.
In JeanYves Girard, editor, Proceedings of the 4th
International Conference on Typed Lambda Calculi and Applications (TLCA'99),
pages 198212, L'Aquila, Italy, April 1999. SpringerVerlag LNCS 1581.

Martin Hofmann.
Semantical analysis for higherorder abstract syntax.
In G. Longo, editor, Proceedings of the 14th Annual Symposium on
Logic in Computer Science (LICS'99), pages 204213, Trento, Italy, July
1999. IEEE Computer Society Press.

J.P. Jouannaud and A. Rubio.
The higherorder recursive path ordering.
In G. Longo, editor, Proceedings of the 14th Annual Symposium on
Logic in Computer Science (LICS'99), pages 402411, Trento, Italy, July
1999. IEEE Computer Society Press.

Claude Kirchner and Hélène Kirchner, editors.
Proceedings of the International Workshop on Rewriting Logic and
its Applications, volume 15 of Electronic Notes in Theoretical Computer
Science.
Elsevier Science, PontàMousson, France, September 1998.
Available electronically.

Pierre Leleu.
Induction et Syntaxe Abstraite d'Ordre Supérieur dans les
Théories Typées.
PhD thesis, Ecole Nationale des Ponts et Chaussees, MarnelaVallee,
France, December 1998.

José Meseguer, editor.
Proceedings of the First International Workshop on Rewriting
Logic and its Applications, volume 4 of Electronic Notes in Theoretical
Computer Science.
Elsevier Science, Pacific Grove, California, September 1998.
Available electronically.

Olaf Müller, Tobias Nipkow, David von Oheimb, and Oscar Slotosch.
Holcf = HOL + LCF.
Journal of Functional Programming, 9:191223, 1999.

Gopalan Nadathur and Dustin J. Mitchell.
System description: Teyjus  a compiler and abstract machine based
implementation of lambda prolog.
In H. Ganzinger, editor, Proceedings of the 16th International
Conference on Automated Deduction (CADE16), pages 287291, Trento, Italy,
July 1999. SpringerVerlag LNCS.

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

George C. Necula and Peter Lee.
The design and implementation of a certifying compiler.
In Keith D. Cooper, editor, Proceedings of the 1998 ACM SIGPLAN
Conference on Programming Language Design and Implementation (PLDI), 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.

Tobias Nipkow.
Verified lexical analysis.
In J. Grundy and M. Newey, editors, Proceedings of the 11th
International Conference on Theorem Proving in Higher Order Logics
(TPHOLs'98), pages 115, Canberra, Australia, September 1998.
SpringerVerlag LNCS 1479.

Tobias Nipkow.
Embedding programming language in theorem provers.
In Harald Ganzinger, editor, Proceedings of the 16th
International Conference on Automated Deduction (CADE16), pages 398399,
Trento, Italy, July 1999. SpringerVerlag LNAI 1632.
Abstract for Invited Talk.

Tobias Nipkow and Leonor Prensa Nieto.
Owicki/Ggries in Isabelle/HOL.
In J.P. Finance, editor, Proceedings of the Second
International Conference on Fundamental Approaches to Software Engineering
(FASE'99), pages 188203, Amsterdam, The Netherlands, March 1999.
SpringerVerlag LNCS 1577.

Tobias Nipkow and David von Oheimb.
Javalight is typesafe  definitely.
In L. Cardelli, editor, Conference Record of the 25th Symposium
on Principles of Programming Languages (POPL'98), pages 161170, San Diego,
California, January 1998. ACM Press.

Lawrence C. Paulson.
A generic tableau prover and its integration with Isabelle.
In Proceedings of the CADE15 Workshop on Integration of
Deduction Systems, pages 5160, July 1998.
Available as Technical Report 441, Computer Laboratory, University of
Cambridge.
Available in PostScript format.

Lawrence C. Paulson.
The inductive approach to verifying cryptographic protocols.
Journal of Computer Security, 6:85128, 1998.
Available in PostScript format.

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

Robert Pollack.
How to believe a machinechecked proof.
In G. Sambin and J. Smith, editors, TwentyFive Years of
Constructive Type Theory. Oxford University Press, August 1998.
Proceedings of a Congress held in Venice, Italy, October 1995.
Available in PostScript format.

David J. Pym.
On bunched predicate logic.
In G. Longo, editor, Proceedings of the 14th Annual Symposium on
Logic in Computer Science (LICS'99), pages 183192, Trento, Italy, July
1999. IEEE Computer Society Press.

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.

Femke van Raamsdonk.
Higherorder rewriting.
In P. Narendran and M. Rusinowitch, editors, Proceedings of the
10th International Conference on Rewriting Techniques and Applications
(RTA99), pages 4559, Trento, Italy, July 1999. SpringerVerlag LNCS 1631.
Invited Tutorial.

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

David von Oheimb and Tobias Nipkow.
Machinechecking the Java specification: Proving typesafety.
In J. AlvesFoss, editor, Formal Syntax and Semantics of
Java, pages 119156. SpringerVerlag LNCS 1523, 1999.
See also:
Frank Pfenning
fp@cs