Bibliography on Logical Frameworks
The source
for this bibliography is in BibTeX format, DVI and
PostScript versions are
also available. 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.
Currently available more specialized bibliographies:
As of October 1994 these were subsets of this bibliography, but they are
likely to diverge over time. I will endeavor to incorporate new publications
into this bibliography periodically.
Some conventions I followed in compiling the bibliography are given in a
comment at the beginning of the source. I wrote some lightweight
Emacs tools in order to translate this bibliography from BibTeX to HTML format
and to generate the subsets mentioned above. If you are interested in these
tools, please inquire by email.
Last Updated: Tue Aug 3 1999
Compiled by Frank
Pfenning
fp@cs
Shortcuts:
ABCDEFGHIJKLMNOPQRSTUVWXYZ

Peter Aczel, David P. Carlisle, and Nax Mendler.
Two frameworks of theories and their implementation in Isabelle.
In G. Huet and G. Plotkin, editors, Logical Frameworks, pages
339. Cambridge University Press, 1991.

Sten Agerhold and Jacob Frost.
An Isabellebased theorem prover for VDMSL.
In E. Gunter and A. Felty, editors, Proceedings of the 10th
International Conference on Theorem Proving in Higher Order Logics
(TPHOLs'97), pages 116, Murray Hill, New Jersey, August 1997.

Thorsten Altenkirch.
Constructions, Inductive Types and Strong Normalization.
PhD thesis, University of Edinburgh, November 1993.
Available as Technical Report CST10693.

Thorsten Altenkirch.
A formalization of the strong normalization proof for System F in
LEGO.
In M. Bezem and J.F. Groote, editors, Proceedings of the
International Conference on Typed Lambda Calculi and Applications, pages
1328, Utrecht, The Netherlands, March 1993. SpringerVerlag LNCS 664.

Thorsten Altenkirch, Veronica Gaspes, Bengt Nordström, and Björn von
Sydow.
A User's Guide to ALF.
Chalmers University of Technology, Sweden, May 1994.
Available in PostScript format.

Thorsten Altenkirch, Martin Hofmann, and Thomas Streicher.
Reductionfree normalization for a polymorphic system.
In E. Clarke, editor, Proceedings of the 11th Annual Symposium
on Logic in Computer Science, pages 98106, New Brunswick, New Jersey, July
1996. IEEE Computer Society Press.

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.

Pablo Argón, John Mullins, and Olivier Roux.
A correct compiler construction using Coq.
In Didier Galmiche, editor, Informal Proceedings of the Workshop
on Proof Search in TypeTheoretic Languages, pages 312, New Brunswick, New
Jersey, July 1996.

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.

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.

David R. Aspinall.
Isabelle Modules: a new theory mechanism for Isabelle.
Undergraduate dissertation, University of Cambridge, 1991.

Jürgen Avenhaus and Carlos LoríaSáenz.
Higher order conditional rewriting and narrowing.
In J.P. Jouannaud, editor, Proceedings of the First
International Conference on Constraints in Computational Logics, pages
269284, Munich, Germany, September 1994. SpringerVerlag LNCS 845.

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.

Clemens Ballarin, Karsten Homann, and Jacques Calmet.
Theorems and algorithms: An interface between Isabelle and Maple.
In A. H. M. Levelt, editor, International Symposium on Symbolic
and Algebraic Computation, pages 150157. ACM Press, 1995.
Available in PostScript format.

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.

Henk P. Barendregt.
Lambda calculi with types.
In S. Abramsky, D. Gabbay, and T.S.E. Maibaum, editors, Handbook
of Logic in Computer Science, volume 2, chapter 2, pages 117309. Oxford
University Press, 1992.

David Basin and Doug Howe.
Some normalization properties of MartinLöf's type theory, and
applications.
In Theoretical Aspects of Computer Software, pages 475494,
Sendai, Japan, September 1991. SpringerVerlag LNCS 526.

David Basin and Seán Matthews.
Structuring metatheory on inductive definitions.
In M.A. McRobbie and J.K. Slaney, editors, Proceedings of the
13th International Conference on Automated Deduction (CADE13), pages
171185, New Brunswick, New Jersey, July 1996. SpringerVerlag LNAI 1104.

David Basin, Seán Matthews, and Luca Viganò.
Implementing modal and relevance logics in a logical framework.
In L.C. Aiello, J. Doyle, and S.C. Shapiro, editors, Proceegins
of the Fifth International Conference on Knowledge Representation and
Reasoning (KR'96), pages 386397. Morgan Kaufmann Publishers, 1996.

David Basin, Seán Matthews, and Luca Viganò.
A topography of labelled modal logics.
In F. Baader and K.U. Schulz, editors, Proceedings of the First
International Workshop on Frontiers of Combining Systems (FroCoS'96), pages
7592. Kluwer Academic Publishers, March 1996.
Available in PostScript format.

David Basin, Seán Matthews, and Luca Viganò.
Labelled propositional modal logics: Theory and practice.
Journal of Logic and Computation, 7(6):685717, 1997.

David Basin, Seán Matthews, and Luca Viganò.
Labelled quantified modal logics.
In G. Brewka, C. Habel, and B. Nebel, editors, Proceedings of
the 21st German Annual Conference on Artificial Intelligence (KI'97), pages
171182. SpringerVerlag LNAI 1303, 1997.

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.

David A. Basin.
IsaWhelk: Whelk interpreted in Isabelle.
In Pascal Van Hentenryck, editor, Proceedings of the Eleventh
International Conference on Logic Programming, page 741, Genoa, Italy, June
1994. MIT Press.
Abstract.
Available in DVI format.

David A. Basin.
Logic frameworks for logic programs.
In 4th International Workshop on Logic Program Synthesis and
Transformation, pages 116, Pisa, Italy, June 1994. SpringerVerlag LNCS
883.
Available in PostScript format.

David A. Basin, Alan Bundy, Ina Kraan, and Seán Matthews.
A framework for program development based on schematic proof.
In Proceedings of the 7th International Workshop on Software
Specification and Design, pages 162171. IEEE Computer Society Press, 1993.

David A. Basin and Robert L. Constable.
Metalogical frameworks.
In G. Huet and G. Plotkin, editors, Logical Environments, pages
129. Cambridge University Press, 1993.

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.

Yves Bertot, Gilles Kahn, and Laurent Théry.
Proof by pointing.
In M. Hagiya and J.C. Mitchell, editors, Proceedings of the
International Symposium on Theoretical Aspects of Computer Softward, pages
141160, Sendai, Japan, April 1994. SpringerVerlag LNCS 789.
Available in PostScript format.

Gustavo Betarte.
A case study in machineassisted proofs: The integers form an
integral domain.
Licentiate thesis, Chalmers University of Technology and University
of Göteborg, Sweden, November 1993.

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.

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

Manfred Broy, Ursula Hinkel, Tobias Nipkow, Christian Prehofer, and Birgit
Schieder.
Interpreter verification for a functional language.
In P.S. Thiagarajan, editor, Proceedings of the 14th Conference
on Foundations of Software Technology and Theoretical Computer Science,
pages 7788. SpringerVerlag LNCS 880, 1994.
Available electronically.

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.

Luis Caires and Luis Monteiro.
Higherorder polymorphic unification for logic programming.
In Pascal Van Hentenryck, editor, Proceedings of the Eleventh
International Conference on Logic Programming, pages 419433, Genoa, Italy,
June 1994. MIT Press.

Guillermo Calderón.
Implementing MartinLöf's theory of types in a higherorder
logic programming language.
Submitted, May 1995.

A. Cant.
Program verification using higher order logic.
Technical Report ERL0600RR, Electronics Research Laboratory, DSTO,
1992.

A. Cant and M. A. Ozols.
A verification environment for ML programs.
In Peter Lee, editor, Workshop on ML and its Applications,
pages 151156, San Francisco, California, June 1992. ACM SIGPLAN.

A. Cant and M. A. Ozols.
An approach to automated reasoning about operational semantics.
Technical report, Electronics Research Laboratory, DSTO, Salisbury,
South Astralia, 1994.

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.
In R. Dyckhoff, H. Herre, and P. SchroederHeister, editors, Proceedings of the 5th International Workshop on Extensions of Logic
Programming, pages 6781, Leipzig, Germany, March 1996. SpringerVerlag
LNAI 1050.
Available in DVI and
PostScript formats.

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.

Jawahar Lal Chirimar.
Proof Theoretic Approach to Specification Languages.
PhD thesis, University of Pennsylvania, May 1995.
Available in PostScript format.

Boleslaw Ciesielski and Mitchell Wand.
Using the theorem prover Isabelle91 to verify a simple proof of
compiler correctness.
Technical Report NUCCS9120, College of Computer Science,
Northeastern University, December 1991.

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.

Martin D. Coen.
Interactive Program Derivation.
PhD thesis, University of Cambridge, 1992.
Available as Computer Laboratory Technical Report 272.
Available in DVI format.

Robert Constable and Douglas Howe.
NuPrl as a general logic.
In P. Odifreddi, editor, Logic and Computation. Academic Press,
1990.

Robert L. Constable et al.
Implementing Mathematics with the Nuprl Proof Development
System.
PrenticeHall, Englewood Cliffs, New Jersey, 1986.

Catarina Coquand.
A proof of normalization for simply typed lambda calculus written in
ALF.
In Proceedings of the Workshop on Types for Proofs and
Programs, pages 8592, Båstad, Sweden, 1992.

Catarina Coquand.
From semantics to rules: A machine assisted analysis.
In E. Börger, Y. Gurevich, and K. Meinke, editors, Proceedings of the 7th Workshop on Computer Science Logic, pages 91105.
SpringerVerlag LNCS 832, 1993.

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.

Thierry Coquand.
Pattern matching with dependent types.
In Proceedings of the Workshop on Types for Proofs and
Programs, pages 7183, Båstad, Sweden, 1992.

Thierry Coquand, Bengt Nordström, Jan M. Smith, and Björn von Sydow.
Type theory and programming.
Bulletin of the European Association for Theoretical Computer
Science, 52:203228, February 1994.

Thierry Coquand and Jan M. Smith.
What is the status of pattern matching in type theory?
In Proceedings of the Workshop on Types for Proofs and
Programs, pages 9194, Nijmegen, The Netherlands, 1993.

C. Cornes and D. Terrasse.
Automating inversion and inductive predicates in Coq.
In Proceedings of the Workshop on Types for Proofs and
Programs, pages 85104, Torino, Italy, June 1995. SpringerVerlag LNCS
1158.
Available in PostScript format.

Judicael Courant.
A module calculus for pure type systems.
In R. Hindley, editor, Proceedings fo the Third International
Conference on Typed Lambda Calculus and Applications (TLCA'97), Nancy,
France, April 1997. SpringerVerlag LNCS.

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

Régis Curien, Zhenyu Qian, and Hui Shi.
Efficient secondorder matching.
In Harald Ganzinger, editor, Proceedings of the 7th
International Conference on Rewriting Techniques and Applications, pages
317331, New Brunswick, New Jersey, July 1996. SpringerVerlag LNCS 1103.

Silvia da Rosa and Alberto Pardo.
Representing program transformation in MartinLöf's type
theory.
Technical report, Instituto de Computación, Facultad de
Ingenieria, Universidad de la Republica Oriental del Uruguay, Montevideo,
Uruguay, 1994.

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.

Jeremy E. Dawson and Rajeev Goré.
A mechanisation of classical tense display logic.
In G. Antoniou and J. Slaney, editors, Proceedings of the 11th
Australian Joint Conference on Artificial Intelligence (AI'98), pages
107118, Brisbane, Australia, July 1998. SpringerVerlag LNAI 1502.
Available in PostScript format.

Jeremy E. Dawson and Rajeev Goré.
A mechanised proof system for relation algebra using display logic.
In J. Dix, L. Fariñas del Cerro, and U. Furbach, editors, Proceedings of the European Workshop on Logics in Artificial Intelligence
(JELIA'98), pages 264278, Dagstuhl, Germany, October 1998. SpringerVerlag
LNAI 1478.
Available in PostScript format.

N.G. de Bruijn.
The mathematical language AUTOMATH, its usage, and some of its
extensions.
In M. Laudet, editor, Proceedings of the Symposium on Automatic
Demonstration, pages 2961, Versailles, France, December 1968.
SpringerVerlag LNM 125.

N.G. de Bruijn.
Lambdacalculus notation with nameless dummies: a tool for automatic
formula manipulation with application to the ChurchRosser theorem.
Indag. Math., 34(5):381392, 1972.

N.G. de Bruijn.
AUTQE without type inclusion.
Memorandum 197804, Department of Mathematics, Eindhoven University
of Technology, August 1978.

N.G. de Bruijn.
A survey of the project AUTOMATH.
In J.P. Seldin and J.R. Hindley, editors, To H.B. Curry: Essays
in Combinatory Logic, Lambda Calculus and Formalism, pages 579606.
Academic Press, 1980.

N.G. de Bruijn.
Formalization of constructivity in AUTOMATH.
In Papers Dedicated to J.J. Seidel, P.J. de Doelder, J. de Graaf
and J.H van Lint, pages 76101. Department of Mathematics and Computing
Science, Eindhoven University of Technology, 1984.
EUT Report 84WSK03.

N.G. de Bruijn.
Generalizing AUTOMATH by means of a lambdatyped lambda calculus.
In D.W. Kueker, E.G.K. LopezEscobar, and C.H. Smith, editors, Mathematical Logic and Theoretical Computer Science, volume 106 of Lecture Notes in Pure and Applied Mathematics, pages 7192. Marcel Dekker,
New York, 1987.

N.G. de Bruijn.
The use of justification systems for integrated semantics.
In P. MartinLöf and G. Mints, editors, Proceedings of the
International Conference on Computer Logic COLOG'88, pages 924, Tallinn,
Estonia, December 1988. SpringerVerlag LNCS 417.

N.G. de Bruijn.
A plea for weaker frameworks.
In G. Huet and G. Plotkin, editors, Logical Frameworks, pages
4067. Cambridge University Press, 1991.

N.G. de Bruijn.
Telescopic mappings in typed lambda calculus.
Information and Computation, 91(2):189204, April 1991.

N.G. de Bruijn.
Algorithmic definition of lambdatyped lambda calculus.
In G. Huet and G. Plotkin, editors, Logical Environment, pages
131145. Cambridge University Press, 1993.

Joëlle Despeyroux, Amy Felty, and André Hirschowitz.
Higherorder abstract syntax in Coq.
In M. DezaniCiancaglini and G. Plotkin, editors, Proceedings of
the International Conference on Typed Lambda Calculi and Applications, pages
124138, Edinburgh, Scotland, April 1995. SpringerVerlag LNCS 902.
Available in PostScript format.

Joëlle Despeyroux and André Hirschowitz.
Higherorder abstract syntax with induction in Coq.
In Frank Pfenning, editor, Proceedings of the 5th
International Conference on Logic Programming and Automated Reasoning, pages
159173, Kiev, Ukraine, July 1994. SpringerVerlag LNAI 822.
Available in PostScript format.

Joëlle Despeyroux, Frank Pfenning, and Carsten Schürmann.
Primitive recursion for higherorder abstract syntax.
Technical Report CMUCS96172, Carnegie Mellon University, September
1996.
Available in DVI and
PostScript formats.

Joëlle Despeyroux, Frank Pfenning, and Carsten Schürmann.
Primitive recursion for higherorder abstract syntax.
In R. Hindley, editor, Proceedings of the Third International
Conference on Typed Lambda Calculus and Applications (TLCA'97), pages
147163, Nancy, France, April 1997. SpringerVerlag LNCS.
An extended version is available as Technical Report CMUCS96172,
Carnegie Mellon University.
Available in DVI and
PostScript formats.

Marco Devillers, David Griffioen, and Olaf Müller.
Possibly infinite sequences in theorem provers: A comparative study.
In E.L. Gunter and A. Felty, editors, Proceedings of the 10th
International Conference on Theorem Proving in Higher Order Logics
(TPHOLs'97), pages 89104, Murray Hill, New Jersey, August 1997.
SpringerVerlag LNCS 1275.

Scott Dietzen.
A Language for HigherOrder ExplanationBased Learning.
PhD thesis, School of Computer Science, Carnegie Mellon University,
1991.
Available as Technical Report CMUCS92110.

Scott Dietzen and Frank Pfenning.
A declarative alternative to assert in logic programming.
In Vijay Saraswat and Kazunori Ueda, editors, International
Logic Programming Symposium, pages 372386. MIT Press, October 1991.

Scott Dietzen and Frank Pfenning.
Higherorder and modal logic as a framework for explanationbased
generalization.
Machine Learning, 9:2355, 1992.

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, Amy Felty, Hugo Herbelin, Gérard Huet, Chet Murthy, Catherine
Parent, Christine PaulinMohring, and Benjamin Werner.
The Coq proof assistant user's guide.
Rapport Techniques 154, INRIA, Rocquencourt, France, 1993.
Version 5.8.

Gilles Dowek, Thérèse Hardin, and Claude Kirchner.
Higherorder unification via explicit substitutions.
In D. Kozen, editor, Proceedings of the Tenth Annual Symposium
on Logic in Computer Science, pages 366374, San Diego, California, June
1995. IEEE Computer Society Press.

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.

Gilles Dowek, Thérèse Hardin, Claude Kirchner, and Frank Pfenning.
Unification via explicit substitutions: The case of higherorder
patterns.
In M. Maher, editor, Proceedings of the Joint International
Conference and Symposium on Logic Programming, pages 259273, Bonn,
Germany, September 1996. MIT Press.
Available in DVI and
PostScript formats.

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.

Dominic Duggan.
Higherorder substitutions.
Technical Report CS9344, University of Waterloo, Waterloo, Ontario,
Canada, October 1993.
Revised September 1994.
Available electronically.

Dominic Duggan.
Unification with extended patterns.
Technical Report CS9337, University of Waterloo, Waterloo, Ontario,
Canada, July 1993.
Revised March 1994 and September 1994.
Available electronically.

Dominic Duggan.
Logical closures.
In Frank Pfenning, editor, Proceedings of the 5th International
Conference on Logic Programming and Automated Reasoning, pages 114129,
Kiev, Ukraine, July 1994. SpringerVerlag LNAI 822.

Peter Dybjer and Herbert Sander.
A functional programming approach to the specification and
verification of concurrent systems.
Formal Aspects of Computing, 1:303319, 1989.

Roy Dyckhoff and Luís Pinto.
Uniform proofs and natural deduction.
In D. Galmiche and L. Wallen, editors, Proceedings of the
Workshop on Proof Search in TypeTheoretic Languages, pages 1723, Nancy,
France, July 1994.
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.

LarsHenrik Eriksson.
A finitary version of the calculus of partial inductive definitions.
In L.H. Eriksson, L. Hallnäs, and P. SchroederHeister, editors,
Proceedings of the Second International Workshop on Extensions of Logic
Programming, pages 89134, Stockholm, Sweden, January 1992. SpringerVerlag
LNAI 596.

LarsHenrik Eriksson.
Finitary Partial Inductive Definitions and General Logic.
PhD thesis, Department of Computer and System Sciences, Royal
Institute of Technology, Stockholm, 1993.

LarsHenrik Eriksson.
Finitary partial inductive definitions as a general logic.
In R. Dyckhoff, editor, Proceedings of the 4th International
Workshop on Extensions of Logic Programming. SpringerVerlag LNAI 798, 1993.

LarsHenrik Eriksson.
Pi: An interactive derivation editor for the calculus of partial
inductive definitions.
In A. Bundy, editor, Proceedings of the 12th International
Conference on Automated Deduction, pages 821825, Nancy, France, June 1994.
Springer Verlag LNAI 814.

LarsHenrik Eriksson and Lars Hallnäs.
A programming calculus based on partial inductive definitions.
SICS Research Report R88013, Swedish Institute of Computer Science,
1988.

Solomon Feferman.
Finitary inductive systems.
In R. Ferro, editor, Proceedings of Logic Colloquium '88,
pages 191220, Padova, Italy, August 1988. NorthHolland.

Amy Felty.
A logic program for transforming sequent proofs to natural deduction
proofs.
In Peter SchroederHeister, editor, Proceedings of the
International Workshop on Extensions of Logic Programming, pages 157178,
Tübingen, Germany, December 1989. SpringerVerlag LNAI 475.
Available in PostScript format.

Amy Felty.
Specifying and Implementing Theorem Provers in a HigherOrder
Logic Programming Language.
PhD thesis, University of Pennsylvania, August 1989.
Available as Technical Report MSCIS8953.

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.
A logic programming approach to implementing higherorder term
rewriting.
In LarsHenrik Eriksson, Lars Hallnäs, and Peter
SchroederHeister, editors, Proceedings of the Second International
Workshop on Extensions of Logic Programming, pages 135161, Stockholm,
Sweden, January 1991. SpringerVerlag LNAI 596.
Available in PostScript format.

Amy Felty.
Encoding the calculus of constructions in a higherorder logic.
In M. Vardi, editor, Eighth Annual IEEE Symposium on Logic in
Computer Science, pages 233244, Montreal, Canada, June 1993.
Available in PostScript format.

Amy Felty.
Implementing tactics and tacticals in a higherorder logic
programming language.
Journal of Automated Reasoning, 11(1):4381, August 1993.
Available in PostScript format.

Amy Felty and Douglas Howe.
Generalization and reuse of tactic proofs.
In Frank Pfenning, editor, Proceedings of the 5th International
Conference on Logic Programming and Automated Reasoning, pages 115, Kiev,
Ukraine, July 1994. SpringerVerlag LNAI 822.

Amy Felty and Douglas Howe.
Tactic theorem proving with refinementtree proofs and metavariables.
In Alan Bundy, editor, Proceedings of the 12th International
Conference on Automated Deduction, pages 605619, Nancy, France, June 1994.
SpringerVerlag LNAI 596.
Available in PostScript format.

Amy Felty and Dale Miller.
Specifying theorem provers in a higherorder logic programming
language.
In Ewing Lusk and Ross Overbeek, editors, Proceedings of the
Ninth International Conference on Automated Deduction, pages 6180,
Argonne, Illinois, May 1988. SpringerVerlag LNCS 310.

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.

Roland Fettig and Bernd Löchner.
Unification of higherorder patterns in a simply typed
lambdacalculus with finite products and terminal type.
In Harald Ganzinger, editor, Proceedings of the 7th
International Conference on Rewriting Techniques and Applications, pages
347361, New Brunswick, New Jersey, July 1996. SpringerVerlag LNCS 1103.

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.

Daniel Fridlender.
Ramsey's theorem in type theory.
Licentiate thesis, Chalmers University of Technology and University
of Göteborg, Sweden, October 1993.

J. Frost and I. A. Mason.
An operational logic of effects.
In M.E. Houle and P. Eades, editors, Proceedings of Computing:
Australasian Theorem Symposium (CATS'96), pages 147156, Melbourne,
Australia, January 1996.
Available in PostScript format.

Jacob Frost.
A case study of coinduction in Isabelle.
Technical Report 359, University of Cambridge, Computer Laboratory,
February 1995.
Revised version of CUCL 308, August 1993.

D. M. Gabbay, editor.
What is a Logical System?
Oxford University Press, 1995.

Dov M. Gabbay.
Classical vs nonclassical logic.
In D.M. Gabbay, C.J. Hogger, and J.A. Robinson, editors, Handbook of Logic in Artificial Intelligence and Logic Programming,
volume 2, chapter 2.6. Oxford University Press, 1994.

Dov M Gabbay.
Labelled deductive systems, volume 1  foundations.
Technical Report MPII94223, MaxPlanckInstitut für
Informatik, Saarbrücken, Germany, 1994.

Dov M. Gabbay.
Labelled Deductive Systems, volume 1.
Oxford University Press, 1996.

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.

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.

Veronica Gaspes and Jan M. Smith.
Machine checked normalization proofs for typed combinator calculi.
In Proceedings of the Workshop on Types for Proofs and
Programs, pages 177192, Båstad, Sweden, 1992.

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.

Neil Ghani.
Etaexpansions in dependent type theory  the calculus of
constructions.
In P. de Groote and J.R. Hindley, editors, Proceedings of the
Third International Conference on Typed Lambda Calculus and Applications
(TLCA'97), pages 164180, Nancy, France, April 1997. SpringerVerlag LNCS
1210.

JeanYves Girard.
On the unity of logic.
Annals of Pure and Applied Logic, 59:201217, 1993.

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.

Warren D. Goldfarb.
The undecidability of the secondorder unification problem.
Theoretical Computer Science, 13:225230, 1981.

Andrew D. Gordan and Tom Melham.
Five axioms of alphaconversion.
In J. von Wright, J. Grundy, and J. Harrison, editors, Proceedings of the 9th International Conference on Theorem Proving in Higher
Order Logics (TPHOLs'96), pages 173191, Turku, Finland, August 1996.
SpringerVerlag LNCS 1125.

M.J.C. Gordon and T.F. Melham.
Introduction to HOL: A Theorem Proving Environment for Higher
Order Logic.
Cambridge University Press, 1993.

Elsa L. Gunter.
Extensions to logic programming motivated by the construction of a
generic theorem prover.
In Peter SchroederHeister, editor, Proceedings of the
International Workshop on Extensions of Logic Programming, pages 223244,
Tübingen, Germany, 1989. SpringerVerlag LNAI 475.

Marianne Haberstrau.
ECOLOG: An environment for constraint logics.
In J.P. Jouannaud, editor, Proceedings of the First
International Conference on Constraints in Computational Logics, pages
237252, Munich, Germany, September 1994. SpringerVerlag LNCS 845.

Masami Hagiya.
Generalization from partial parameterization in higherorder type
theory.
Theoretical Computer Science, 63:113139, 1989.

Masami Hagiya.
Programming by example and proving by example using higherorder
unification.
In M. E. Stickel, editor, Proceedings of the 10th International
Conference on Automated Deduction, pages 588602, Kaiserslautern, Germany,
July 1990. SpringerVerlag LNAI 449.

Masami Hagiya.
From programmingbyexample to provingbyexample.
In T. Ito and A. R. Meyer, editors, Proceedings of the
International Conference on Theoretical Aspects of Computer Software, pages
387419, Sendai, Japan, September 1991. SpringerVerlag LNCS 526.

Masami Hagiya and Yozo Toda.
On implicit arguments.
Technical Report 911, Department of Information Science, University
of Tokyo, January 1995.
Available in PostScript format.

W. A. Halang, B. Krämer, and N. Völker.
Formally verified building blocks in functional logic diagrams for
emergency shutdown system design.
High Integrity Systems, 1(3):277286, 1995.

Lars Hallnäs.
A note on the logic of a logic program.
In Proceedings of the Workshop on Programming Logic. University
of Göteborg and Chalmers University of Technology, Report PMGR37, 1987.

Lars Hallnäs.
Partial inductive definitions.
Theoretical Computer Science, 87(1):115142, September 1991.

John Hannan.
Implementing lambdacalculus reduction strategies in extended
logic programming languages.
In LarsHenrik Eriksson, Lars Hallnäs, and Peter
SchroederHeister, editors, Proceedings of the Second Workshop on
Extensions to Logic Programming, pages 193219. SpringerVerlag LNAI 596,
January 1991.

John Hannan.
Staging transformations for abstract machines.
In P. Hudak and N. Jones, editors, Proceedings of the ACM
SIGPLAN Symposium on Partial Evaluation and Semantics Based Program
Manipulation, pages 130141, New Haven, Connecticut, June 1991.

John Hannan.
Extended natural semantics.
Journal of Functional Programming, 3(2):123152, April 1993.
Available in DVI format.

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 Dale Miller.
Enriching a metalanguage with higherorder features.
Technical Report MSCIS8845, University of Pennsylvania, June 1988.

John Hannan and Dale Miller.
Uses of higherorder unification for implementing program
transformers.
In Kenneth A. Bowen and Robert A. Kowalski, editors, Fifth
International Logic Programming Conference, pages 942959, Seattle,
Washington, August 1988. MIT Press.

John Hannan and Dale Miller.
Deriving mixed evaluation from standard evaluation for a simple
functional programming language.
In J.L.A. van de Snepscheut, editor, Proceedings of the
International Conference on Mathematics of Program Construction, pages
239255. SpringerVerlag LNCS 375, 1989.

John Hannan and Dale Miller.
A metalogic for functional programming.
In H. Abramson and M. Rogers, editors, MetaProgramming in Logic
Programming, chapter 24, pages 453476. MIT Press, 1989.

John Hannan and Dale Miller.
From operational semantics to abstract machines: Preliminary results.
In M. Wand, editor, Proceedings of the 1990 ACM Conference on
Lisp and Functional Programming, pages 323332, Nice, France, 1990.

John Hannan and Dale Miller.
From operational semantics to abstract machines.
Mathematical Structures in Computer Science, 2(4):415459,
1992.
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.

John J. Hannan.
Investigating a ProofTheoretic MetaLanguage for Functional
Programs.
PhD thesis, University of Pennsylvania, January 1991.
Available as Technical Report MSCIS9109.

James Harland and David Pym.
Resourcedistribution via boolean constraints.
In W. McCune, editor, Proceedings of the 14th International
Conference on Automated Deduction (CADE14), pages 222236, Townsville,
Australia, July 1997. SpringerVerlag LNAI 1249.

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 Harrison.
Floating point verification in HOL Light: The exponential
function.
Technical Report 428, University of Cambridge Computer Laboratory,
1997.

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.

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.

Michael Hedberg.
Normalizing the associative law  an experiment with
MartinLöf's type theory.
Formal Aspects of Computing, 3:218252, 1991.
Extended version available as Licentiate Thesis, Chalmers University
of Technology, 1990.

Steve Hill and Simon Thompson.
Miranda in Isabelle.
In L.C. Paulson, editor, Proceedings of the First Isabelle Users
Workshop, pages 122135. University of Cambridge Computer Laboratory,
September 1995.
Availabe as Technical Report 397.
Available electronically.

Daniel Hirschkoff.
A full formalization of picalculus theory in the Calculus of
Constructions.
In E. Gunter and A. Felty, editors, Proceedings of the 10th
International Conference on Theorem Proving in Higher Order Logics
(TPHOLs'97), pages 153169, Murray Hill, New Jersey, August 1997.

Joshua Hodas and Dale Miller.
Logic programming in a fragment of intuitionistic linear logic.
Information and Computation, 110(2):327365, 1994.
A preliminary version appeared in the Proceedings of the Sixth Annual
IEEE Symposium on Logic in Computer Science, pages 3242, Amsterdam, The
Netherlands, July 1991.
Available in PostScript format.

Joshua S. Hodas.
Logic Programming in Intuitionistic Linear Logic: Theory,
Design, and Implementation.
PhD thesis, University of Pennsylvania, Department of Computer and
Information Science, 1994.

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.

Gérard Huet.
The undecidability of unification in third order logic.
Information and Control, 22(3):257267, 1973.

Gérard Huet.
A unification algorithm for typed lambdacalculus.
Theoretical Computer Science, 1:2757, 1975.

Gérard Huet.
An analysis of Böhm's theorem.
Technical Report 2008, INRIA, Rocquencourt, France, August 1993.

Gérard Huet.
Residual theory in lambdacalculus: A formal development.
Journal of Functional Programming, 4(3):371394, July 1994.
Preliminary version available as INRIA Technical Report 2009, August
1993.

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

Bharat Jayaraman and Gopalan Nadathur.
Implementation techniques for scoping constructs in logic
programming.
In Koichi Furukawa, editor, Proceedings of the Eighth
International Logic Programming Conference, pages 871886, Paris, France,
June 1991. MIT 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.

L.S. van Benthem Jutting.
Checking Landau's ``Grundlagen'' in the AUTOMATH System.
PhD thesis, Eindhoven University of Technology, 1977.

L.S. van Benthem Jutting, James McKinna, and Robert Pollack.
Checking algorithms for Pure Type Systems.
In Henk Barendregt and Tobias Nipkow, editors, Proceedings of
the International Workshop on Types for Proofs and Programs, pages 1961,
Nijmegen, The Netherlands, May 1994. SpringerVerlag LNCS 806.

Stefan Kahrs.
Towards a domain theory for termination proofs.
In Jieh Hsiang, editor, Proceedings of the Sixth International
Conference on Rewriting Techniques and Applications, pages 241255,
Kaiserslautern, Germany, April 1995. SpringerVerlag LNCS 914.

F. Kammüller.
Experimental support of a proof programming language with Isabelle.
Diplomarbeit, Technical University Berlin, 1995.
Available in PostScript format.

Claude Kircher, Hélène Kirchner, and Marian Vittek.
Implementing computational systems with constraints.
In P. van Hentenryck and V. Saraswat, editors, Proceedings of
the First Workshop on Principles and Practice of Constraints Programming,
Newport, Rhode Island, April 1993. MIT 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.

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.

Kolyang, C. Lüth, T. Meier, and B. Wolff.
Generic interfaces for transformation systems and interactive theorem
provers.
In K. Berghammer, J. Peleska, and B. Buth, editors, Proceedings
of the International Workshop for Tool support in Verification and
Validation. SpringerVerlag LNCS, 1997.

Kolyang, C. Lüth, T. Meier, and B. Wolff.
TAS and IsaWin: Generic interfaces for transformational program
development and theorem proving.
In M. Bidoit and M. Dauchet, editors, Proceedings of the Seventh
International Joint Conference on the Theory and Practice of Software
Development (TAPSOFT'97), pages 855858, Lille, France, April 1997.
SpringerVerlag LNCS 1214.
System abstract.

Kolyang, T. Santen, and B. Wolff.
Correct and userfriendly implementation of transformation systems.
In M.C. Gaudel and J. Woodcock, editors, Symposium on
Industrial Benefits and Advances in Formal Methods (FME'96), pages 629648,
Oxford, England, March 1996. SpringerVerlag LNCS 1051.
Available in PostScript format.

Kolyang, T. Santen, and B. Wolff.
A structure preserving encoding of Z in Isabelle/HOL.
In J. von Wright, J. Grundy, and J. Harrison, editors, Proceedings of the 9th International Conference on Theorem Proving in Higher
Order Logics, pages 283298, Turku, Finland, August 1996. SpringerVerlag
LNCS 1125.

Keehand Kwon, Gopalan Nadathur, and Debra Sue Wilson.
Implementing a notion of modules in the logic programming language
lambda Prolog.
In E. Lamma and P. Mello, editors, Proceedings of the Third
International Workshop on Extensions of Logic Programming, pages 359393,
Bologna, Italy, February 1993. SpringerVerlag LNAI 660.
Available in DVI format.

Keehang Kwon.
Towards a Verified Abstract Machine for a Logic Programming
Language with a Notion of Scope.
PhD thesis, Department of Computer Science, Duke University, December
1994.
Available as Technical Report CS199436.
Available in PostScript format.

Keehang Kwon, Gopalan Nadathur, and Debra Sue Wilson.
Implementing polymorphic typing in a logic programming language.
Computer Languages, 20(1):2542, 1994.
Available in DVI format.

Edmund Landau.
Grundlagen der Analysis.
Akademische Verlagsgesellschaft, Leipzig, Germany, 1930.
English translation Foundations of Analysis, Chelsea Publishing
Company, 1951.

F. Leclerc.
Termination proof of term rewriting system with the multiset path
ordering and derivation length: A complete development in the Calculus of
Constructions.
In M. DezaniCiancaglini and G. Plotkin, editors, Proceedings of
the International Conference on Typed Lambda Calculi and Applications, pages
312327, Edinburgh, Scotland, April 1995. SpringerVerlag LNCS 902.

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.

D. Lester and S. Mintchev.
Towards machinechecked compiler correctness for higherorder
languages.
In L. Pacholski and J. Tiuryn, editors, Proceedings of the 8th
Workshop on Computer Science Logic (CSL'94), Kazimierz, Poland, September
1994. Springer LNCS 933.

Jordi Levy.
Linear secondorder unification.
In Harald Ganzinger, editor, Proceedings of the 7th
International Conference on Rewriting Techniques and Applications, pages
332346, New Brunswick, New Jersey, July 1996. SpringerVerlag LNCS 1103.

Chuck Liang.
ObjectLevel Substitution, Unification and Generalization in
MetaLogic.
PhD thesis, University of Pennsylvania, August 1995.
Available in PostScript format.

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.

D. Lugiez.
Higherorder disunification: Some decidable cases.
In J.P. Jouannaud, editor, Proceedings of the First
International Conference on Constraints in Computational Logics, pages
121135, Munich, Germany, September 1994. SpringerVerlag LNCS 845.

Zhaohui Luo and Robert Pollack.
The LEGO proof development system: A user's manual.
Technical Report ECSLFCS92211, University of Edinburgh, May 1992.

Olav Lysne and Javier Piris.
A termination ordering for higher order rewrite systems.
In Jieh Hsiang, editor, Proceedings of the Sixth International
Conference on Rewriting Techniques and Applications, pages 2640,
Kaiserslautern, Germany, April 1995. SpringerVerlag LNCS 914.

Lena Magnusson.
Refinement and local undo in the interactive proof editor ALF.
In Proceedings of the Workshop on Types for Proofs and
Programs, pages 191208, Nijmegen, The Netherlands, 1993.

Lena Magnusson.
The Implementation of ALF  A Proof Editor Based on
MartinLöf's Monomorphic Type Theory with Explicit Substitution.
PhD thesis, Chalmers University of Technology and Göteborg
University, January 1995.

Lena Magnusson and Bengt Nordström.
The ALF proof editor and its proof engine.
In Henk Barendregt and Tobias Nipkow, editors, Types for Proofs
and Programs, pages 213237. SpringerVerlag LNCS 806, 1994.

Narciso MartìOliet and Jose Meseguer.
Rewriting logic as a logical and semantical framework.
Technical Report SRICSL9305, SRI International, August 1993.

Per MartinLöf.
Constructive mathematics and computer programming.
In Logic, Methodology and Philosophy of Science VI, pages
153175. NorthHolland, 1980.

Per MartinLöf.
On the meanings of the logical constants and the justifications of
the logical laws.
Technical Report 2, Scuola di Specializzazione in Logica Matematica,
Dipartimento di Matematica, Università di Siena, 1985.

Per MartinLöf.
Truth of a proposition, evidence of a judgement, validity of a proof.
Notes to a talk given at the workshop Theory of Meaning, Centro
Fiorentino di Storia e Filosofia della Scienza, June 1985.

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

Seán Matthews.
A theory and its metatheory in FS0.
In Dov Gabbay and Franz Guenthner, editors, What is a Logical
System? Oxford University Press, 1994.
Available in DVI and
PostScript formats.

Seán Matthews, Alan Smaill, and David Basin.
Experience with FS0 as a framework theory.
In Gérard Huet and Gordon Plotkin, editors, Logical
Environments, pages 6182. Cambridge University Press, 1993.

Raymond McDowell.
Reasoning in a Logic with Definitions and Induction.
PhD thesis, University of Pennsylvania, 1997.

Raymond McDowell and Dale Miller.
A logic for reasoning with higherorder abstract syntax: An extended
abstract.
In Glynn Winskel, editor, Proceedings of the Twelfth Annual
Symposium on Logic in Computer Science, pages 434445, Warsaw, Poland, June
1997.
Available in PostScript format.

Raymond McDowell, Dale Miller, and Catuscia Palamidessi.
Encoding transition systems in sequent calculus: Preliminary report.
In Proceedings of the Workshop on Linear Logic, volume 3 of
Electronic Notes in Theoretical Computer Science. Elsevier, 1996.

James McKinna and Robert Pollack.
Pure Type Sytems formalized.
In M.Bezem and J.F.Groote, editors, Proceedings of the
International Conference on Typed Lambda Calculi and Applications, pages
289305. SpringerVerlag LNCS 664, March 1993.

D. Méry and A. Mokkedem.
Demonstration of Crocos.
In O. Faergemand and R. Reed, editors, Fifth SDL Forum
Evolving Methods. NorthHolland, 1991.

D. Méry and A. Mokkedem.
A proof environment for a subset of SDL.
In O. Faergemand and R. Reed, editors, Fifth SDL Forum
Evolving Methods. NorthHolland, 1991.

D. Méry and A. Mokkedem.
Crocos: an integrated environment for interactive verification of
SDL specifications.
In G. v. Bochmann and D. K. Probst, editors, Computer Aided
Verification: Fourth International Workshop, CAV '92. SpringerVerlag LNCS
663, 1993.

José Meseguer.
General logics.
In H.D. Ebbinghaus, editor, Logic Colloquium '87, pages
275329, Granada, Spain, July 1987. NorthHolland.

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.

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.
A theory of modules for logic programming.
In Robert M. Keller, editor, Third Annual IEEE Symposium on
Logic Programming, pages 106114, Salt Lake City, Utah, September 1986.

Dale Miller.
Hereditary Harrop formulas and logic programming.
In Proceedings of the VIII International Congress of Logic,
Methodology, and Philosophy of Science, pages 153156, Moscow, Russia,
August 1987.

Dale Miller.
Lexical scoping as universal quantification.
In G. Levi and M. Martelli, editors, Proceedings of the Sixth
International Conference on Logic Programming, pages 268283, Lisbon,
Portugal, June 1989. MIT Press.

Dale Miller.
A logic programming language with lambdaabstraction, function
variables, and simple unification.
In Peter SchroederHeister, editor, Proceedings of the
International Workshop on Extensions of Logic Programming, pages 253281,
Tübingen, Germany, 1989. SpringerVerlag LNAI 475.

Dale Miller.
A logical analysis of modules in logic programming.
Journal of Logic Programming, 6(12):79108, January 1989.

Dale Miller.
Abstractions in logic programming.
In Piergiorgio Odifreddi, editor, Logic and Computer Science,
pages 329359. Academic Press, 1990.
Available in DVI format.

Dale Miller.
A logic programming language with lambdaabstraction, function
variables, and simple unification.
Journal of Logic and Computation, 1(4):497536, 1991.
Available in DVI format.

Dale Miller.
Unification of simply typed lambdaterms as logic programming.
In Koichi Furukawa, editor, Eighth International Logic
Programming Conference, pages 255269, Paris, France, June 1991. MIT Press.
Available in DVI format.

Dale Miller.
Abstract syntax and logic programming.
In Proceedings of the First and Second Russian Conferences on
Logic Programming, pages 322337, Irkutsk and St. Petersburg, Russia, 1992.
SpringerVerlag LNAI 592.
Available in DVI format.

Dale Miller, editor.
Proceedings of the Workshop on the lambda Prolog Programming
Language, Philadelphia, Pennsylvania, July 1992.
Available as University of Pennsylvania Technical Report
MSCIS9286.

Dale Miller.
Unification under a mixed prefix.
Journal of Symbolic Computation, 14:321358, 1992.
Available in DVI format.

Dale Miller.
A proposal for modules in lambda Prolog.
In R. Dyckhoff, editor, Proceedings of the 4th International
Workshop on Extensions to Logic Programming. SpringerVerlag LNAI 798, 1993.
Available in PostScript format.

Dale Miller.
A multipleconclusion metalogic.
In S. Abramsky, editor, Ninth Annual IEEE Symposium on Logic
in Computer Science, pages 272281, Paris, France, July 1994.
Available in DVI format.

Dale Miller and Gopalan Nadathur.
Higherorder logic programming.
In Ehud Shapiro, editor, Proceedings of the Third International
Logic Programming Conference, pages 448462, London, June 1986.

Dale Miller and Gopalan Nadathur.
Some uses of higherorder logic in computational linguistics.
In Proceedings of the 24th Annual Meeting of the Association for
Computational Linguistics, pages 247255. Association for Computational
Linguistics, Morristown, New Jersey, 1986.
Available in DVI format.

Dale Miller and Gopalan Nadathur.
A logic programming approach to manipulating formulas and programs.
In Seif Haridi, editor, IEEE Symposium on Logic Programming,
pages 379388, San Francisco, September 1987.
Available in PostScript format.

Dale Miller, Gopalan Nadathur, Frank Pfenning, and Andre Scedrov.
Uniform proofs as a foundation for logic programming.
Annals of Pure and Applied Logic, 51:125157, 1991.
Available in DVI format.

Dale Miller, Gopalan Nadathur, and Andre Scedrov.
Hereditary Harrop formulas and uniform proof systems.
In David Gries, editor, Symposium on Logic in Computer Science,
pages 98105, Ithaca, NY, June 1987.

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.

Olaf Müller and Tobias Nipkow.
Combining model checking and deduction of I/Oautomata.
In E. Brinksma, editor, Proceedings of the First International
Workshop on Tools and Algorithms for the Construction and Analysis of
Systems, Aarhus, Denmark, May 1995. SpringerVerlag LNCS 1019.

Olaf Müller and Tobias Nipkow.
Traces of I/Oautomata in Isabelle/HOLCF.
In M. Bidoit and M. Dauchet, editors, Proceedings of the Seventh
International Joint Conference on the Theory and Practice of Software
Development (TAPSOFT'97), Lille, France, April 1997. SpringerVerlag LNCS
1214.

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

Gopalan Nadathur.
A HigherOrder Logic as the Basis for Logic Programming.
PhD thesis, University of Pennsylvania, May 1987.
Available as Technical Report MSCIS8748.

Gopalan Nadathur.
A proof procedure for the logic of hereditary Harrop formulas.
Journal of Automated Reasoning, 11(1):115145, August 1993.
Available in DVI format.

Gopalan Nadathur.
A notation for lambda terms II: Refinements and applications.
Technical Report CS199401, Department of Computer Science, Duke
University, January 1994.
Available in DVI format.

Gopalan Nadathur.
Correspondences between classical, intuitionistic and uniform
provability.
Theoretical Computer Science, 1997.
To appear. Available as Technical Report TR9712, Department of
Computer Science, University of Chicago.
Available in PostScript format.

Gopalan Nadathur.
An explicit substitution notation in a lambdaProlog implementation.
In Proceedings of the First International Workshop on Explicit
Substitutions, Tsukuba, Japan, 1998.
Available as Technical Report TR9801, Department of Computer
Science, University of Chicago.
Available in PostScript format.

Gopalan Nadathur.
A finegrained notation for lambda terms and its use in intensional
operationa.
Journal of Functional and Logic Programming, 1999(2), March
1999.
Available electronically.

Gopalan Nadathur and Bharat Jayaraman.
Towards a WAM model for lambda Prolog.
In Ewing Lusk and Ross Overbeek, editors, Proceedings of the
North American Conference on Logic Programming, pages 11801198, Cleveland,
Ohio, October 1989.

Gopalan Nadathur, Bharat Jayaraman, and Keehang Kwon.
Scoping constructs in logic programming: Implementation problems and
their solution.
Journal of Logic Programming, 25(2):119161, November 1995.

Gopalan Nadathur, Bharat Jayaraman, and Debra Sue Wilson.
Implementation considerations for higherorder features in logic
programming.
Technical Report CS199316, Department of Computer Science, Duke
University, June 1993.
Available in DVI format.

Gopalan Nadathur and Donald W. Loveland.
Uniform proofs and disjunctive logic programming.
In D. Kozen, editor, Proceedings of the Tenth Annual Symposium
on Logic in Computer Science, pages 148155, San Diego, California, June
1995. IEEE Computer Society Press.
Available as Technical Report CS199440, Department of Computer
Science, Duke University, December 1994.
Available in PostScript format.

Gopalan Nadathur and Dale Miller.
An overview of lambda Prolog.
In Kenneth A. Bowen and Robert A. Kowalski, editors, Fifth
International Logic Programming Conference, pages 810827, Seattle,
Washington, August 1988. MIT Press.

Gopalan Nadathur and Dale Miller.
Higherorder Horn clauses.
Journal of the ACM, 37(4):777814, October 1990.
Available in DVI format.

Gopalan Nadathur and Dale Miller.
Higherorder logic programming.
In D.M. Gabbay, C.J. Hogger, and J.A. Robinson, editors, Handbook of Logic in Artificial Intelligence and Logic Programming,
volume 5, chapter 8. Oxford University Press, 1998.

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.

Gopalan Nadathur and Frank Pfenning.
The type system of a higherorder logic programming language.
In Frank Pfenning, editor, Types in Logic Programming, pages
245283. MIT Press, 1992.

Gopalan Nadathur and Guanshan Tong.
Realizing modularity in lambdaProlog.
Journal of Functional and Logic Programming, 1999(9), April
1999.
Available electronically.

Gopalan Nadathur and Debra Sue Wilson.
A representation of lambda terms suitable for operations on their
intensions.
In M. Wand, editor, Proceedings of the 1990 ACM Conference on
Lisp and Functional Programming, pages 341348, 1990.

Gopalan Nadathur and Debra Sue Wilson.
A notation for lambda terms: A generalization of environments.
Theoretical Computer Science, 198(12):4998, May 1998.
Previous version available as Technical Report TR9701, Department
of Computer Science, University of Chicago.
Available in PostScript format.

Wolfgang Naraschewski and Tobias Nipkow.
Type inference verified: Algorithm W in Isabelle/HOL.
Submitted, 1997.

Dieter Nazareth and Tobias Nipkow.
Formal verification of algorithm W: The monomorphic case.
In J. Wright, J. Grundy, and J. Harrison, editors, Proceedings
of the 9th International Conference on Theorem Proving in Higher Order Logics
(TPHOL'96), Turku, Finland, August 1996. SpringerVerlag LNCS 1125.

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

R.P. Nederpelt.
Strong Normalization in a Typed Lambda Calculus with Lambda
Structured Types.
PhD thesis, Eindhoven University of Technology, 1973.

R.P. Nederpelt, J.H. Geuvers, and R.C. de Vrijer, editors.
Selected Papers on Automath, volume 133 of Studies in
Logic and the Foundations of Mathematics.
NorthHolland, 1994.

Tobias Nipkow.
Equational reasoning in Isabelle.
Science of Computer Programming, 12:123149, 1989.

Tobias Nipkow.
Term rewriting and beyond  theorem proving in Isabelle.
Formal Aspects of Computing, 1:320338, 1989.

Tobias Nipkow.
Formal verification of data type refinement  theory and practice.
In J.W. de Bakker, W.P. de Roever, and G. Rozenberg, editors, Stepwise Refinement of Distributed Systems, pages 561591. SpringerVerlag
LNCS 430, 1990.

Tobias Nipkow.
Higherorder unification, polymorphism, and subsorts.
In S. Kaplan and M. Okada, editors, Proceedings of the 2nd
International Workshop on Conditional and Typed Rewriting Systems, pages
436447, Montreal, Canada, June 1990. SpringerVerlag LNCS 516.

Tobias Nipkow.
Constructive rewriting.
Computer Journal, 34:3441, 1991.

Tobias Nipkow.
Higherorder critical pairs.
In G. Kahn, editor, Sixth Annual IEEE Symposium on Logic in
Computer Science, pages 342349, Amsterdam, The Netherlands, July 1991.

Tobias Nipkow.
Functional unification of higherorder patterns.
In M. Vardi, editor, Eighth Annual IEEE Symposium on Logic in
Computer Science, pages 6474, Montreal, Canada, June 1993.

Tobias Nipkow.
Ordersorted polymorphism in Isabelle.
In G. Huet and G. Plotkin, editors, Logical Environments, pages
164188. Cambridge University Press, 1993.

Tobias Nipkow.
Orthogonal higherorder rewrite systems are confluent.
In M. Bezem and J.F. Groote, editors, Proceedings of the
International Conference on Typed Lambda Calculi and Applications, pages
306317, Utrecht, The Netherlands, May 1993.

Tobias Nipkow.
More ChurchRosser proofs (in Isabelle/HOL).
In M.A. McRobbie and J.K. Slaney, editors, Proceedings of the
13th International Conference on Automated Deduction (CADE13), pages
733747, New Brunswick, New Jersey, July 1996. SpringerVerlag LNAI 1104.

Tobias Nipkow.
Winskel is (almost) right: Towards a mechanized semantics textbook.
In V. Chandru and V. Vinay, editors, Proceedings of the
Conference on Foundations of Software Technology and Theoretical Computer
Science, pages 180192. SpringerVerlag LNCS 1180, 1996.

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.
Winskel is (almost) right: Towards a mechanized semantics textbook.
Formal Aspects of Computing, 10:171186, 1998.

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 Lawrence C. Paulson.
Isabelle91.
In D. Kapur, editor, Proceedings of the 11th International
Conference on Automated Deduction, pages 673676, Saratoga Springs, NY,
1992. SpringerVerlag LNAI 607.
System abstract.
Available in DVI format.

Tobias Nipkow and Konrad Slind.
I/O automata in Isabelle/HOL.
In P. Dybjer, B. Nordström, and J. Smith, editors, Proceedings of the International Workshop on Types for Proofs and Programs,
pages 101119, Båstad, Sweden, June 1994. SpringerVerlag LNCS 996.

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.

Philippe Noël.
A set theoretic semantics for a first order temporal logic:
Definition and application using Isabelle.
Technical Report UMCS91124, Department of Computer Science,
University of Manchester, 1991.

Philippe Noël.
Experimenting with Isabelle in ZF set theory.
Journal of Automated Reasoning, 10(1):1558, 1993.

Bengt Nordström.
The ALF proof editor.
In Proceedings of the Workshop on Types for Proofs and
Programs, pages 253266, Nijmegen, 1993.

Remo Pareschi and Dale Miller.
Extending definite clause grammars with scoping constructs.
In David H. D. Warren and Peter Szeredi, editors, Proceedings of
Seventh International Conference on Logic Programming, pages 373389,
Jerusalem, Israel, June 1990. MIT Press.
Available in DVI format.

Lawrence C. Paulson.
Natural deduction as higherorder resolution.
Journal of Logic Programming, 3:237258, 1986.
Available in DVI format.

Lawrence C. Paulson.
A formulation of the simple theory of types (for Isabelle).
In P. MartinLöf and G. Mints, editors, Proceedings of the
International Conference on Computer Logic COLOG'88, pages 246274,
Tallinn, Estonia, December 1988. SpringerVerlag LNCS 417.
Available in DVI format.

Lawrence C. Paulson.
Isabelle: The next seven hundred theorem provers.
In E. Lusk and R. Overbeek, editors, Proceedings of the 9th
International Conference on Automated Deduction, pages 772773, Argonne,
Illinois, 1988. Springer Verlag LNCS 310.
System abstract.
Available in DVI format.

Lawrence C. Paulson.
The foundation of a generic theorem prover.
Journal of Automated Reasoning, 5(3):363397, 1989.
Available in DVI format.

Lawrence C. Paulson.
Isabelle: The next 700 theorem provers.
In P. Odifreddi, editor, Logic and Computer Science, pages
361386. Academic Press, 1990.
Available in DVI format.

Lawrence C. Paulson.
Designing a theorem prover.
In S. Abramsky, D. M. Gabbay, and T. S. E. Maibaum, editors, Handbook of Logic in Computer Science, volume 2, pages 415475. Oxford
University Press, 1992.
Available in DVI format.

Lawrence C. Paulson.
Coinduction and corecursion in higherorder logic.
Technical Report 304, University of Cambridge, Computer Laboratory,
July 1993.
Available in PostScript format.

Lawrence C. Paulson.
Introduction to Isabelle.
Technical Report 280, University of Cambridge, Computer Laboratory,
1993.
Available in DVI format.

Lawrence C. Paulson.
The Isabelle reference manual.
Technical Report 283, University of Cambridge, Computer Laboratory,
1993.
Available in DVI format.

Lawrence C. Paulson.
Isabelle's objectlogics.
Technical Report 286, University of Cambridge, Computer Laboratory,
1993.
Available in DVI format.

Lawrence C. Paulson.
Set theory for verification: I. From foundations to functions.
Journal of Automated Reasoning, 11(3):353389, 1993.
Available in PostScript format.

Lawrence C. Paulson.
A fixedpoint approach to implementing (co)inductive definitions.
In Alan Bundy, editor, Proceedings of the 12th International
Conference on Automated Deduction, pages 148161, Nancy, France, June 1994.
SpringerVerlag LNAI 814.
Available in DVI format.

Lawrence C. Paulson.
Isabelle: A Generic Theorem Prover.
SpringerVerlag LNCS 828, 1994.

Lawrence C. Paulson, editor.
Proceedings of the First Isabelle Users Workshop, 1995.
Available as University of Cambridge, Computer Laboratory, Technical
Report 379.
Available electronically.

Lawrence C. Paulson.
Set theory for verification: II. Induction and recursion.
Journal of Automated Reasoning, 15(2):167215, 1995.
Available in PostScript format.

Lawrence C. Paulson.
A simple formatization and proof for the mutilated chess board.
Technical Report 394, University of Cambridge, Computer Laboratory,
May 1996.
Available in DVI format.

Lawrence C. Paulson.
Tool support for logics of programs.
In Manfred Broy, editor, Mathematical Methods in Program
Development, NATO ASI Series F. SpringerVerlag, 1996.
Summer School Marktoberdorf. In press.

Lawrence C. Paulson.
Generic automatic proof tools.
In Robert Veroff, editor, Automated Reasoning and Its
Applications, chapter 3. MIT Press, 1997.
In press.

Lawrence C. Paulson.
Mechanized proofs for a recursive authentication protocol.
In Proceedings of the 10th Computer Security Foundations
Workshop, pages 8495. IEEE Computer Society Press, June 1997.
Available in PostScript format.

Lawrence C. Paulson.
Mechanized proofs of security protocols: NeedhamSchroeder with
public keys.
Technical Report 413, University of Cambridge, Computer Laboratory,
January 1997.

Lawrence C. Paulson.
Mechanizing coinduction and corecursion in higherorder logic.
Journal of Logic and Computation, 7(2):175204, March 1997.

Lawrence C. Paulson.
Proving properties of security protocols by induction.
In Proceedings of the 10th Computer Security Foundations
Workshop, pages 7083. IEEE Computer Society Press, June 1997.
Available in PostScript format.

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.

Lawrence C. Paulson and Krzysztof Grabczewski.
Mechanising set theory: Cardinal arithmetic and the axiom of choice.
Technical Report 377, University of Cambridge, Computer Laboratory,
August 1995.
Available in PostScript format.

Lawrence C. Paulson and Tobias Nipkow.
Isabelle tutorial and user's manual.
Technical Report 189, University of Cambridge, Computer Laboratory,
January 1990.
Available in DVI format.

Patricia Peratto.
Courseofvalues recursion in MartinLöf's type theory.
Master's thesis, Instituto de Computación, Facultad de
Ingenieria, Universidad de la Republica Oriental del Uruguay, Montevideo,
Uruguay, 1991.

Patricia Peratto.
An Alf implementation of insertion sort.
Technical report, Instituto de Computación, Facultad de
Ingenieria, Universidad de la Republica Oriental del Uruguay, Montevideo,
Uruguay, 1995.

Patricia Peratto.
Courseofvalues recursion on lists and a definition for quicksort.
Technical report, Instituto de Computación, Facultad de
Ingenieria, Universidad de la Republica Oriental del Uruguay, Montevideo,
Uruguay, 1995.

Frank Pfenning.
Partial polymorphic type inference and higherorder unification.
In Proceedings of the 1988 ACM Conference on Lisp and
Functional Programming, pages 153163, Snowbird, Utah, July 1988. ACM
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 Conal Elliott.
Higherorder abstract syntax.
In Proceedings of the ACM SIGPLAN '88 Symposium on Language
Design and Implementation, pages 199208, Atlanta, Georgia, June 1988.
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, 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.

Frank Pfenning and HaoChi Wong.
On a modal lambdacalculus for S4.
In S. Brookes and M. Main, editors, Proceedings of the Eleventh
Conference on Mathematical Foundations of Programming Semantics, New
Orleans, Louisiana, March 1995.
Electronic Notes in Theoretical Computer Science, Volume 1,
Elsevier.
Available in DVI and
PostScript formats.

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.
Closure under alphaconversion.
In Henk Barendregt and Tobias Nipkow, editors, Proceedings of
the Workshop on Types for Proofs and Programs, pages 313332, Nijmegen, The
Netherlands, May 1993. SpringerVerlag LNCS 806.

Robert Pollack.
The Theory of LEGO: A Proof Checker for the Extended
Calculus of Constructions.
PhD thesis, University of Edinburgh, 1994.
Available in PostScript format.

Robert Pollack.
Polishing up the TaitMartinLöf proof of the ChurchRosser
theorem.
Unpublished note, January 1995.
Available in PostScript format.

Robert Pollack.
A verified typechecker.
In M. DezaniCiancaglini and G. Plotkin, editors, Proceedings of
the International Conference on Typed Lambda Calculi and Applications, pages
365380, Edinburgh, Scotland, April 1995. SpringerVerlag LNCS 902.

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.

Robert Pollak.
On extensibility of proof checkers.
In P. Dybjer, B. Nordström, and J. Smith, editors, Proceedings of the International Workshop on Types for Proofs and Programs,
pages 140161, Båstad, Sweden, June 1994. SpringerVerlag LNCS 996.

Christian Prehofer.
Decidable higherorder unification problems.
In Proceedings of the 12th International Conference on Automated
Deduction, pages 635649, Nancy, France, June 1994. Springer LNAI 814.

Christian Prehofer.
Higherorder narrowing.
In Proceedings of the Ninth Annual IEEE Symposium on Logic in
Computer Science, pages 507516, Paris, France, July 1994. IEEE Computer
Society Press.

Christian Prehofer.
Solving HigherOrder Equations: From Logic to Programming.
PhD thesis, Technische Universität München, March 1995.

Thomas Puls.
Annotation Logic for Standard ML.
PhD thesis, Technical University of Denmark, Lyngby, October 1990.
Department of Computer Science Report IDTR:199074.

Cornelia Pusch.
Verification of compiler correctness for the WAM.
In J. Wright, J. Grundy, and J. Harrison, editors, Proceedings
of the 9th International Conference on Theorem Proving in Higher Order Logics
(TPHOL'96), Turku, Finland, August 1996. SpringerVerlag LNCS 1125.
Available in DVI 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.

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.

David J. Pym and James A. Harland.
The uniform prooftheoretic foundation of linear logic programming.
Journal of Logic and Computation, 4(2):175207, April 1994.

Zhenyu Qian.
Linear unification of higherorder patterns.
In M.C. Gaudel and J.P. Jouannaud, editors, Proceedings of the
Colloquium on Trees in Algebra and Programming, pages 391405, Orsay,
France, April 1993. SpringerVerlag LNCS 668.

Zhenyu Qian.
Unification of higherorder patterns in linear time and space.
Journal of Logic and Computation, 6(3):315341, 1995.

Ole Rasmussen.
The ChurchRosser theorem in Isabelle: A proof porting
experiment.
Technical Report 364, University of Cambridge, Computer Laboratory,
March 1995.
Available in PostScript format.

Ole Rasmussen.
An embedding of Ruby in Isabelle.
In M.A. McRobbie and J.K. Slaney, editors, Proceedings of the
13th International Conference on Automated Deduction, pages 186200, New
Brunswick, New Jersey, July 1996. SpringerVerlag LNAI 1104.

Franz Regensburger.
HOLCF: Eine konservative Erweiterung von HOL um LCF.
PhD thesis, Technische Universität München, 1994.

Franz Regensburger.
HOLCF: Higher Order Logic of Computable Functions.
In E.T. Schubert, P.J. Windley, and J. AlvesFoss, editors, Proceedings of the 8th International Workshop on Higher Order Logic Theorem
Proving and Its Applications, Aspen Grove, Utah, September 1995.
SpringerVerlag LNCS 971.

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.

Eugene J. Rollins and Jeannette M. Wing.
Specifications as search keys for software libraries.
In Koichi Furukawa, editor, Proceedings of the 1991
International Conference on Logic Programming, pages 173187. MIT Press,
1991.

Lars Rossen.
Formal Ruby.
In J. Staunstrup, editor, Formal Methods for VLSI Design.
Elsevier, 1990.

Lars Rossen.
Proving (facts about) Ruby.
In G. Birtwistle, editor, IV Higher Order Workshop, pages
265283, Banff, Alberta, September 1990. SpringerVerlag Workshops in
Computing.

Lars Rossen.
Ruby algebra.
In G. Jones and M. Sheeran, editors, Designing Correct
Circuits, Oxford, England, September 1990. SpringerVerlag Workshops in
Computing.

Lars Rossen.
A Relational Approach to Sequential VLSI Design.
PhD thesis, Department of Computer Science, Technical University of
Denmark, 1992.

Piotr Rudnicki.
An overview of the Mizar project.
Notes to a talk at the workshop on Types for Proofs and
Programs, June 1992.

Harald Rueß.
Reflection of formal tactics in a deductive reflection framework.
In M.A. McRobbie and J.K. Slaney, editors, Proceedings of the
13th International Conference on Automated Deduction, pages 628642, New
Brunswick, New Jersey, July 1996. SpringerVerlag LNAI 1104.

Harald Ruess.
Computational reflection in the calculus of constructions and its
application to theorem proving.
In R. Hindley, editor, Proceedings fo the Third International
Conference on Typed Lambda Calculus and Applications (TLCA'97), Nancy,
France, April 1997. SpringerVerlag LNCS.

Amokrane Saïbi.
Formalization of a lambdacalculus with explicit substitutions
in Coq.
In P. Dybjer, B. Nordström, and J. Smith, editors, Proceedings of the International Workshop on Types for Proofs and Programs,
pages 183202, Båstad, Sweden, June 1994. SpringerVerlag LNCS 996.

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.

Roberto Sandner and Olaf Müller.
Theorem prover support for the refinement of stream processing
functions.
In E. Brinksma, editor, Proceedings of the Third International
Workshop on Tools and Algorithms for the Construction and Analysis of Systems
(TACAS'97), pages 351365, Enschede, The Netherlands, April 1997.
SpringerVerlag LNCS 1217.

Peter SchroederHeister.
Structural frameworks, substructural logics, and the role of
elimination inferences.
In Gérard Huet and Gordon Plotkin, editors, Logical
Frameworks, pages 385403. Cambridge University Press, 1991.

Peter SchroederHeister.
Definitional reflection and the completion.
In R. Dyckhoff, editor, Proceedings of the 4th International
Workshop on Extensions of Logic Programming, pages 333347. SpringerVerlag
LNAI 798, 1993.

Peter SchroederHeister.
Rules of definitional reflection.
In M. Vardi, editor, Proceedings of the Eighth Annual IEEE
Symposium on Logic in Computer Science, pages 222232, Montreal, Canada,
June 1993.

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.

N. Shankar.
A mechanical proof of the ChurchRosser theorem.
Journal of the Association for Computing Machinery,
35(3):475522, July 1988.

N. Shankar.
Metamathematics, Machines, and Gödel's Proof, volume 38 of
Cambridge Tracts in Theoretical Computer Science.
Cambridge University Press, 1994.

Martin Simons.
Proof presentation for Isabelle.
In E. Gunter and A. Felty, editors, Proceedings of the 10th
International Conference on Theorem Proving in Higher Order Logics
(TPHOLs'97), pages 259274, Murray Hill, New Jersey, August 1997.

Oscar Slotosch.
Higher order quotients and their implementation in Isabelle HOL.
In E. Gunter and A. Felty, editors, Proceedings of the 10th
International Conference on Theorem Proving in Higher Order Logics, pages
291306, Murray Hill, New Jersey, August 1997.

Wayne Snyder and Jean H. Gallier.
Higher order unification revisited: Complete sets of transformations.
Journal of Symbolic Computation, 8(12):101140, 1989.

Ian Stark.
Names, equations, relations: Practical ways to reason about ``new''.
In R. Hindley, editor, Proceedings of the Third International
Conference on Typed Lambda Calculus and Applications (TLCA'97), Nancy,
France, April 1997. SpringerVerlag LNCS.

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.

Nora Szasz.
A machine checked proof that Ackermann's function is not primitive
recursive.
Licentiate thesis, Chalmers University of Technology and University
of Göteborg, Sweden, June 1991.

A. Tasistro.
Formulation of MartinLöf's theory of types with explicit
substitutions.
Master's thesis, Chalmers Tekniska Högskola and Göteborgs
Universitet, May 1993.

H. Tej and B. Wolff.
A corrected failuredivergence model for CSP in Isabelle/HOL.
In C. Jones and J. Fitzgerald, editors, Proceedings of the
International Formal Methods Europe Symposium (FME'97), Graz, Austria,
September 1997.
Available in PostScript format.

Delphine Terrasse.
Encoding natural semantics in Coq.
In V.S. Alagar, editor, Proceedings of the Fourth International
Conference on Algebraic Methodology and Software Technology, pages 230244,
Montreal, Canada, July 1995. SpringerVerlag LNCS 936.

Delphine Terrasse.
Vers un environnement de développement de preuves en
sémantique naturelle.
Thèse de doctorat, ENPC, 1995.
Available in PostScript format.

Laurent Thery, Yves Bertot, and Gilles Kahn.
Real theorem provers deserve real userinterfaces.
In Proceedings of the Fifth ACM SIGSOFT Symposium on
Software Development Environments, pages 120129, 1992.
Published as SIGSOFT Software Engineering Notes, Vol. 17, No. 5.

D.T. van Daalen.
The Language Theory of Automath.
PhD thesis, Eindhoven University of Technology, 1980.

J. van de Pol and H. Schwichtenberg.
Strict functionals for termination proofs.
In M. DezaniCiancaglini and G. Plotkin, editors, Proceedings of
the International Conference on Typed Lambda Calculi and Applications, pages
350364, Edinburgh, Scotland, April 1995. SpringerVerlag LNCS 902.

Vincent van Oostrom.
Higherorder families.
In Harald Ganzinger, editor, Proceedings of the 7th
International Conference on Rewriting Techniques and Applications, pages
392407, New Brunswick, New Jersey, July 1996. SpringerVerlag LNCS 1103.

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.

Myra VanInwegen.
The MachineAssisted Proof of Programming Language Properties.
PhD thesis, University of Pennsylvania, August 1996.

Luca Viganò.
A Framework for NonClassical Logics.
PhD thesis, Universität des Saarlandes, September 1997.

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.

Marian Vittek.
A compiler for nondeterministic term rewriting systems.
In Harald Ganzinger, editor, Proceedings of the 7th
International Conference on Rewriting Techniques and Applications, pages
154168, New Brunswick, New Jersey, July 1996. SpringerVerlag LNCS 1103.

David von Oheimb and Thomas F. Gritzner.
RALL: Machinesupported proofs for relational algebra.
In W. McCune, editor, Proceedings of the 14th International
Conference on Automated Deduction, pages 380394, Townsville, Australia,
July 1997. SpringerVerlag LNCS 1249.

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.

Björn von Sydow.
A machineassisted proof of the fundamental theorem of arithmetic.
PMG Report 68, Chalmers University of Technology, Sweden, June 1992.

Lincoln A. Wallen.
Automated Deduction in NonClassical Logics.
MIT Press, 1990.

Markus Wenzel.
Type classes and overloading in higherorder logic.
In E. Gunter and A. Felty, editors, Proceedings of the 10th
International Conference on Theorem Proving in Higher Order Logics
(TPHOLs'97), pages 307322, Murray Hill, New Jersey, August 1997.

David Wolfram.
The Clausal Theory of Types.
Cambridge University Press, 1993.

David A. Wolfram.
Intractable unifiability problems and backtracking.
Journal of Automated Reasoning, 5:3747, 1989.

David A. Wolfram.
ACE: The abstract clause engine.
In Mark E. Stickel, editor, Proceedings of the Tenth
International Conference on Automated Deduction, pages 679680,
Kaiserslautern, Germany, July 1990. SpringerVerlag LNCS 449.
System Abstract.

David A. Wolfram.
The Clausal Theory of Types.
PhD thesis, University of Cambridge, March 1990.

David A. Wolfram.
Rewriting, and equational unification: The higherorder cases.
In Ronald V. Book, editor, Proceedings of the Fourth
International Conference on Rewriting Techniques and Applications, pages
2536, Como, Italy, April 1991. SpringerVerlag LNCS 488.

David A. Wolfram.
Semantics for abstract clauses.
In Henk Barendregt and Tobias Nipkow, editors, Proceedings of
the Workshop on Types for Proofs and Programs, pages 366383, Nijmegen, The
Netherlands, May 1993. SpringerVerlag LNCS 806.

David A. Wolfram.
A semantics for lambda Prolog.
Theoretical Computer Science, 136(1):277289, 1994.

J. Zucker.
Formalisation of classical mathematics in AUTOMATH.
In Colloques Internationaux du Centre National de Recherche
Scientifique, volume 249, pages 135145, July 1975.