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

New Implementation Home Pages

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.
  1. Andrew W. Appel and Edward W. Felten. Proof-carrying authentication. In G. Tsudik, editor, Proceedings of the 6th Conference on Computer and Communications Security, Singapore, November 1999. ACM Press. To appear.

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

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

  4. 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 (CADE-16), pages 267-281, Trento, Italy, July 1999. Springer-Verlag LNAI 1632.

  5. 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 55-66, Plattsburgh, New York, September 1998. Springer-Verlag LNAI 1476. Available in DVI format.

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

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

  8. 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 361-375, Louvain-la-Neuve, Belgium, September 1998. Springer-Verlag LNCS 1485. Available in PostScript format.

  9. 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 Computer-Aided Verification (CAV'98), pages 416-427, Vancouver, B.C., Canada, June 1998. Springer-Verlag LNCS 1427. Available in PostScript format.

  10. Frédéric Blanqui, Jean-Pierre 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 (RTA-99), pages 301-316, Trento, Italy, July 1999. Springer-Verlag LNCS 1631. Available in PostScript format.

  11. Peter Borovanský, Claude Kirchner, Hélène Kirchner, Pierre-Etienne 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.

  12. Iliano Cervesato. Proof-theoretic 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 115-129, Manchester, UK, June 1998. MIT Press. Available in PostScript format.

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

  14. 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 (RTA-99), pages 240-243, Trento, Italy, July 1999. Springer-Verlag LNCS 1631. System Description.

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

  16. Gilles Dowek, Thérèse Hardin, and Claude Kirchner. HOL-lambda-sigma: An intentional first-order expression of higher-order logic. In P. Narendran and M. Rusinowitch, editors, Proceedings of the 10th International Conference on Rewriting Techniques and Applications (RTA-99), pages 317-331, Trento, Italy, July 1999. Springer-Verlag LNCS 1631.

  17. 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 193-202, Trento, Italy, July 1999. IEEE Computer Society Press.

  18. 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 (CADE-15), pages 3-16, Lindau, Germany, July 1998. Springer-Verlag LNAI 1421.

  19. 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 214-224, Trento, Italy, July 1999. IEEE Computer Society Press.

  20. Healfdene Goguen. Soundness of the logical framework for its typed operational semantics. In Jean-Yves Girard, editor, Proceedings of the 4th International Conference on Typed Lambda Calculi and Applications (TLCA'99), pages 177-197, L'Aquila, Italy, April 1999. Springer-Verlag LNCS 1581.

  21. 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):5-31, 1998.

  22. Masahito Hasegawa. Logical predicates for intuitionistic linear type theories. In Jean-Yves Girard, editor, Proceedings of the 4th International Conference on Typed Lambda Calculi and Applications (TLCA'99), pages 198-212, L'Aquila, Italy, April 1999. Springer-Verlag LNCS 1581.

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

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

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

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

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

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

  29. 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 (CADE-16), pages 287-291, Trento, Italy, July 1999. Springer-Verlag LNCS.

  30. George C. Necula. Compiling with Proofs. PhD thesis, Carnegie Mellon University, October 1998. Available as Technical Report CMU-CS-98-154.

  31. 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 333-344, Montreal, Canada, June 1998. ACM Press.

  32. 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 93-104, Indianapolis, Indiana, June 1998. IEEE Computer Society Press.

  33. 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 1-15, Canberra, Australia, September 1998. Springer-Verlag LNCS 1479.

  34. Tobias Nipkow. Embedding programming language in theorem provers. In Harald Ganzinger, editor, Proceedings of the 16th International Conference on Automated Deduction (CADE-16), pages 398-399, Trento, Italy, July 1999. Springer-Verlag LNAI 1632. Abstract for Invited Talk.

  35. 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 188-203, Amsterdam, The Netherlands, March 1999. Springer-Verlag LNCS 1577.

  36. Tobias Nipkow and David von Oheimb. Java-light is type-safe - definitely. In L. Cardelli, editor, Conference Record of the 25th Symposium on Principles of Programming Languages (POPL'98), pages 161-170, San Diego, California, January 1998. ACM Press.

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

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

  39. 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 (CADE-15), pages 1-2, Lindau, Germany, July 1998. Springer-Verlag LNCS 1421. Abstract for invited talk. Available in PostScript format.

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

  41. 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 Type-Theoretic Languages. Electronic Notes in Theoretical Computer Science, July 1998. Available in PostScript format.

  42. 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. Springer-Verlag LNCS, 1998. To appear. Available in PostScript format.

  43. Frank Pfenning and Carsten Schürmann. Twelf User's Guide, 1.2 edition, September 1998. Available as Technical Report CMU-CS-98-173, Carnegie Mellon University.

  44. Frank Pfenning and Carsten Schürmann. System description: Twelf - a meta-logical framework for deductive systems. In H. Ganzinger, editor, Proceedings of the 16th International Conference on Automated Deduction (CADE-16), pages 202-206, Trento, Italy, July 1999. Springer-Verlag LNAI 1632. Available in PostScript format.

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

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

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

  48. Jeff Polakow and Frank Pfenning. Relating natural deduction and sequent calculus for intuitionistic non-commutative 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.

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

  50. 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 183-192, Trento, Italy, July 1999. IEEE Computer Society Press.

  51. Carsten Schürmann and Frank Pfenning. Automated theorem proving in a simple meta-logic for LF. In Claude Kirchner and Hélène Kirchner, editors, Proceedings of the 15th International Conference on Automated Deduction (CADE-15), pages 286-300, Lindau, Germany, July 1998. Springer-Verlag LNCS 1421. Available in PostScript format.

  52. 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 Run-Time Result Verification, Trento, Italy, July 1999.

  53. Femke van Raamsdonk. Higher-order rewriting. In P. Narendran and M. Rusinowitch, editors, Proceedings of the 10th International Conference on Rewriting Techniques and Applications (RTA-99), pages 45-59, Trento, Italy, July 1999. Springer-Verlag LNCS 1631. Invited Tutorial.

  54. Roberto Virga. Higher-Order Rewriting with Dependent Types. PhD thesis, Department of Mathematical Sciences, Carnegie Mellon University, 1999. Forthcoming.

  55. David von Oheimb and Tobias Nipkow. Machine-checking the Java specification: Proving type-safety. In J. Alves-Foss, editor, Formal Syntax and Semantics of Java, pages 119-156. Springer-Verlag LNCS 1523, 1999.

See also:

Frank Pfenning

fp@cs