Bibliography on Logical Frameworks

Currently available more specialized bibliographies:

Some conventions I followed in compiling the bibliography are given in a comment at the beginning of the source. I wrote some light-weight 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 e-mail.

Last Updated: Tue Aug 3 1999
Compiled by Frank Pfenning

1. 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 3-39. Cambridge University Press, 1991.

2. Sten Agerhold and Jacob Frost. An Isabelle-based theorem prover for VDM-SL. In E. Gunter and A. Felty, editors, Proceedings of the 10th International Conference on Theorem Proving in Higher Order Logics (TPHOLs'97), pages 1-16, Murray Hill, New Jersey, August 1997.

3. Thorsten Altenkirch. Constructions, Inductive Types and Strong Normalization. PhD thesis, University of Edinburgh, November 1993. Available as Technical Report CST-106-93.

4. 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 13-28, Utrecht, The Netherlands, March 1993. Springer-Verlag LNCS 664.

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

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

7. Penny Anderson. Program Derivation by Proof Transformation. PhD thesis, Carnegie Mellon University, October 1993. Available as Technical Report CMU-CS-93-206. Available electronically.

8. 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 144-158, Kiev, Ukraine, July 1994. Springer-Verlag LNAI 822.

9. Penny Anderson. Representing proof transformations for program optimization. In Proceedings of the 12th International Conference on Automated Deduction, pages 575-589, Nancy, France, June 1994. Springer-Verlag LNAI 814. Available electronically.

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

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

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

13. 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 Type-Theoretic Languages, pages 3-12, New Brunswick, New Jersey, July 1996.

14. Sergei N. Artemov. On explicit reflection in theorem proving and formal verification. In Harald Ganzinger, editor, Proceedings of the 16th International Conference on Automated Deduction (CADE-16), pages 267-281, Trento, Italy, July 1999. Springer-Verlag LNAI 1632.

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

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

17. Jürgen Avenhaus and Carlos Loría-Sáenz. Higher order conditional rewriting and narrowing. In J.-P. Jouannaud, editor, Proceedings of the First International Conference on Constraints in Computational Logics, pages 269-284, Munich, Germany, September 1994. Springer-Verlag LNCS 845.

18. 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):309-354, 1992. A preliminary version appeared as University of Edinburgh Report ECS-LFCS-87-31.

19. 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 150-157. ACM Press, 1995. Available in PostScript format.

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

21. 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 117-309. Oxford University Press, 1992.

22. David Basin and Doug Howe. Some normalization properties of Martin-Löf's type theory, and applications. In Theoretical Aspects of Computer Software, pages 475-494, Sendai, Japan, September 1991. Springer-Verlag LNCS 526.

23. 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 (CADE-13), pages 171-185, New Brunswick, New Jersey, July 1996. Springer-Verlag LNAI 1104.

24. 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 386-397. Morgan Kaufmann Publishers, 1996.

25. 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 75-92. Kluwer Academic Publishers, March 1996. Available in PostScript format.

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

27. 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 171-182. Springer-Verlag LNAI 1303, 1997.

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

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

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

31. David A. Basin. Logic frameworks for logic programs. In 4th International Workshop on Logic Program Synthesis and Transformation, pages 1-16, Pisa, Italy, June 1994. Springer-Verlag LNCS 883. Available in PostScript format.

32. 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 162-171. IEEE Computer Society Press, 1993.

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

34. Giampaolo Bella and Lawrence C. Paulson. Kerberos version IV: Inductive analysis of the secrecy goals. In J.-J. Quisquater, editor, Proceedings of the 5th European Symposium on Research in Computer Security, pages 361-375, Louvain-la-Neuve, Belgium, September 1998. Springer-Verlag LNCS 1485. Available in PostScript format.

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

36. 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 141-160, Sendai, Japan, April 1994. Springer-Verlag LNCS 789. Available in PostScript format.

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

38. Frédéric Blanqui, Jean-Pierre Jouannaud, and Mitsuhiro Okada. The calculus of algebraic constructions. In P. Narendran and M. Rusinowitch, editors, Proceedings of the 10th International Conference on Rewriting Techniques and Applications (RTA-99), pages 301-316, Trento, Italy, July 1999. Springer-Verlag LNCS 1631. Available in PostScript format.

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

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

41. 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 77-88. Springer-Verlag LNCS 880, 1994. Available electronically.

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

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

44. Guillermo Calderón. Implementing Martin-Löf's theory of types in a higher-order logic programming language. Submitted, May 1995.

45. A. Cant. Program verification using higher order logic. Technical Report ERL-0600-RR, Electronics Research Laboratory, DSTO, 1992.

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

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

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

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

50. Iliano Cervesato, Joshua S. Hodas, and Frank Pfenning. Efficient resource management for linear logic proof search. In R. Dyckhoff, H. Herre, and P. Schroeder-Heister, editors, Proceedings of the 5th International Workshop on Extensions of Logic Programming, pages 67-81, Leipzig, Germany, March 1996. Springer-Verlag LNAI 1050. Available in DVI and PostScript formats.

51. 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 Type-Theoretic Languages, D. Galmiche, editor. Available in PostScript format.

52. Iliano Cervesato and Frank Pfenning. Linear higher-order pre-unification. In D. Galmiche, editor, Informal Proceedings of the Workshop on Proof Search in Type-Theoretic Language, New Brunswick, New Jersey, July 1996. Available in PostScript format.

53. 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 264-275, New Brunswick, New Jersey, July 1996. IEEE Computer Society Press. Available in DVI and PostScript formats.

54. Iliano Cervesato and Frank Pfenning. Linear higher-order pre-unification. In Glynn Winskel, editor, Proceedings of the Twelfth Annual Sumposium on Logic in Computer Science (LICS'97), pages 422-433, Warsaw, Poland, June 1997. IEEE Computer Society Press. Available in DVI and PostScript formats.

55. Iliano Cervesato and Frank Pfenning. A linear spine calculus. Technical Report CMU-CS-97-125, Department of Computer Science, Carnegie Mellon University, April 1997. Available in PostScript format.

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

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

58. Boleslaw Ciesielski and Mitchell Wand. Using the theorem prover Isabelle-91 to verify a simple proof of compiler correctness. Technical Report NU-CCS-91-20, College of Computer Science, Northeastern University, December 1991.

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

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

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

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

63. 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 85-92, Båstad, Sweden, 1992.

64. 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 91-105. Springer-Verlag LNCS 832, 1993.

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

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

67. 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:203-228, February 1994.

68. 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 91-94, Nijmegen, The Netherlands, 1993.

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

70. 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. Springer-Verlag LNCS.

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

72. Régis Curien, Zhenyu Qian, and Hui Shi. Efficient second-order matching. In Harald Ganzinger, editor, Proceedings of the 7th International Conference on Rewriting Techniques and Applications, pages 317-331, New Brunswick, New Jersey, July 1996. Springer-Verlag LNCS 1103.

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

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

75. 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 107-118, Brisbane, Australia, July 1998. Springer-Verlag LNAI 1502. Available in PostScript format.

76. 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 264-278, Dagstuhl, Germany, October 1998. Springer-Verlag LNAI 1478. Available in PostScript format.

77. 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 29-61, Versailles, France, December 1968. Springer-Verlag LNM 125.

78. N.G. de Bruijn. Lambda-calculus notation with nameless dummies: a tool for automatic formula manipulation with application to the Church-Rosser theorem. Indag. Math., 34(5):381-392, 1972.

79. N.G. de Bruijn. AUT-QE without type inclusion. Memorandum 1978-04, Department of Mathematics, Eindhoven University of Technology, August 1978.

80. 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 579-606. Academic Press, 1980.

81. 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 76-101. Department of Mathematics and Computing Science, Eindhoven University of Technology, 1984. EUT Report 84-WSK-03.

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

83. N.G. de Bruijn. The use of justification systems for integrated semantics. In P. Martin-Löf and G. Mints, editors, Proceedings of the International Conference on Computer Logic COLOG'88, pages 9-24, Tallinn, Estonia, December 1988. Springer-Verlag LNCS 417.

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

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

86. N.G. de Bruijn. Algorithmic definition of lambda-typed lambda calculus. In G. Huet and G. Plotkin, editors, Logical Environment, pages 131-145. Cambridge University Press, 1993.

87. Joëlle Despeyroux, Amy Felty, and André Hirschowitz. Higher-order abstract syntax in Coq. In M. Dezani-Ciancaglini and G. Plotkin, editors, Proceedings of the International Conference on Typed Lambda Calculi and Applications, pages 124-138, Edinburgh, Scotland, April 1995. Springer-Verlag LNCS 902. Available in PostScript format.

88. Joëlle Despeyroux and André Hirschowitz. Higher-order abstract syntax with induction in Coq. In Frank Pfenning, editor, Proceedings of the 5th International Conference on Logic Programming and Automated Reasoning, pages 159-173, Kiev, Ukraine, July 1994. Springer-Verlag LNAI 822. Available in PostScript format.

89. Joëlle Despeyroux, Frank Pfenning, and Carsten Schürmann. Primitive recursion for higher-order abstract syntax. Technical Report CMU-CS-96-172, Carnegie Mellon University, September 1996. Available in DVI and PostScript formats.

90. Joëlle Despeyroux, Frank Pfenning, and Carsten Schürmann. Primitive recursion for higher-order abstract syntax. In R. Hindley, editor, Proceedings of the Third International Conference on Typed Lambda Calculus and Applications (TLCA'97), pages 147-163, Nancy, France, April 1997. Springer-Verlag LNCS. An extended version is available as Technical Report CMU-CS-96-172, Carnegie Mellon University. Available in DVI and PostScript formats.

91. 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 89-104, Murray Hill, New Jersey, August 1997. Springer-Verlag LNCS 1275.

92. Scott Dietzen. A Language for Higher-Order Explanation-Based Learning. PhD thesis, School of Computer Science, Carnegie Mellon University, 1991. Available as Technical Report CMU-CS-92-110.

93. 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 372-386. MIT Press, October 1991.

94. Scott Dietzen and Frank Pfenning. Higher-order and modal logic as a framework for explanation-based generalization. Machine Learning, 9:23-55, 1992.

95. Gilles Dowek. The undecidability of typability in the lambda-pi-calculus. In M. Bezem and J.F. Groote, editors, Proceedings of the International Conference on Typed Lambda Calculi and Applications, pages 139-145, Utrecht, The Netherlands, March 1993. Springer-Verlag LNCS 664.

96. Gilles Dowek, Amy Felty, Hugo Herbelin, Gérard Huet, Chet Murthy, Catherine Parent, Christine Paulin-Mohring, and Benjamin Werner. The Coq proof assistant user's guide. Rapport Techniques 154, INRIA, Rocquencourt, France, 1993. Version 5.8.

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

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

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

100. Gilles Dowek, Gérard Huet, and Benjamin Werner. On the definition of the eta-long 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.

101. Dominic Duggan. Higher-order substitutions. Technical Report CS-93-44, University of Waterloo, Waterloo, Ontario, Canada, October 1993. Revised September 1994. Available electronically.

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

103. Dominic Duggan. Logical closures. In Frank Pfenning, editor, Proceedings of the 5th International Conference on Logic Programming and Automated Reasoning, pages 114-129, Kiev, Ukraine, July 1994. Springer-Verlag LNAI 822.

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

105. 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 Type-Theoretic Languages, pages 17-23, Nancy, France, July 1994. Available in PostScript format.

106. Conal Elliott. Higher-order unification with dependent types. In N. Dershowitz, editor, Rewriting Techniques and Applications, pages 121-136, Chapel Hill, North Carolina, April 1989. Springer-Verlag LNCS 355. Available in PostScript format.

107. Conal Elliott and Frank Pfenning. A semi-functional implementation of a higher-order logic programming language. In Peter Lee, editor, Topics in Advanced Language Implementation, pages 289-325. MIT Press, 1991. Available electronically.

108. Conal M. Elliott. Extensions and Applications of Higher-Order Unification. PhD thesis, School of Computer Science, Carnegie Mellon University, May 1990. Available as Technical Report CMU-CS-90-134. Available in DVI and PostScript formats.

109. Lars-Henrik Eriksson. A finitary version of the calculus of partial inductive definitions. In L.-H. Eriksson, L. Hallnäs, and P. Schroeder-Heister, editors, Proceedings of the Second International Workshop on Extensions of Logic Programming, pages 89-134, Stockholm, Sweden, January 1992. Springer-Verlag LNAI 596.

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

111. Lars-Henrik Eriksson. Finitary partial inductive definitions as a general logic. In R. Dyckhoff, editor, Proceedings of the 4th International Workshop on Extensions of Logic Programming. Springer-Verlag LNAI 798, 1993.

112. Lars-Henrik 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 821-825, Nancy, France, June 1994. Springer Verlag LNAI 814.

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

114. Solomon Feferman. Finitary inductive systems. In R. Ferro, editor, Proceedings of Logic Colloquium '88, pages 191-220, Padova, Italy, August 1988. North-Holland.

115. Amy Felty. A logic program for transforming sequent proofs to natural deduction proofs. In Peter Schroeder-Heister, editor, Proceedings of the International Workshop on Extensions of Logic Programming, pages 157-178, Tübingen, Germany, December 1989. Springer-Verlag LNAI 475. Available in PostScript format.

116. Amy Felty. Specifying and Implementing Theorem Provers in a Higher-Order Logic Programming Language. PhD thesis, University of Pennsylvania, August 1989. Available as Technical Report MS-CIS-89-53.

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

118. Amy Felty. A logic programming approach to implementing higher-order term rewriting. In Lars-Henrik Eriksson, Lars Hallnäs, and Peter Schroeder-Heister, editors, Proceedings of the Second International Workshop on Extensions of Logic Programming, pages 135-161, Stockholm, Sweden, January 1991. Springer-Verlag LNAI 596. Available in PostScript format.

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

120. Amy Felty. Implementing tactics and tacticals in a higher-order logic programming language. Journal of Automated Reasoning, 11(1):43-81, August 1993. Available in PostScript format.

121. 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 1-15, Kiev, Ukraine, July 1994. Springer-Verlag LNAI 822.

122. Amy Felty and Douglas Howe. Tactic theorem proving with refinement-tree proofs and metavariables. In Alan Bundy, editor, Proceedings of the 12th International Conference on Automated Deduction, pages 605-619, Nancy, France, June 1994. Springer-Verlag LNAI 596. Available in PostScript format.

123. Amy Felty and Dale Miller. Specifying theorem provers in a higher-order logic programming language. In Ewing Lusk and Ross Overbeek, editors, Proceedings of the Ninth International Conference on Automated Deduction, pages 61-80, Argonne, Illinois, May 1988. Springer-Verlag LNCS 310.

124. Amy Felty and Dale Miller. Encoding a dependent-type lambda-calculus in a logic programming language. In M.E. Stickel, editor, 10th International Conference on Automated Deduction, pages 221-235, Kaiserslautern, Germany, July 1990. Springer-Verlag LNCS 449. Available in PostScript format.

125. Roland Fettig and Bernd Löchner. Unification of higher-order patterns in a simply typed lambda-calculus with finite products and terminal type. In Harald Ganzinger, editor, Proceedings of the 7th International Conference on Rewriting Techniques and Applications, pages 347-361, New Brunswick, New Jersey, July 1996. Springer-Verlag LNCS 1103.

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

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

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

129. 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 147-156, Melbourne, Australia, January 1996. Available in PostScript format.

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

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

132. Dov M. Gabbay. Classical vs non-classical 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.

133. Dov M Gabbay. Labelled deductive systems, volume 1 - foundations. Technical Report MPI-I-94-223, Max-Planck-Institut für Informatik, Saarbrücken, Germany, 1994.

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

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

136. Philippa Gardner. Representing Logics in Type Theory. PhD thesis, University of Edinburgh, July 1992. Available as Technical Report CST-93-92.

137. 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 146-157, St. Petersburg, Russia, July 1993. Springer-Verlag LNAI 698.

138. 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 177-192, Båstad, Sweden, 1992.

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

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

141. 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 95-30. Available in PostScript format.

142. 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 210-224, Kaiserslautern, Germany, April 1995. Springer-Verlag LNCS 914. Available in PostScript format.

143. Herman Geuvers. The Church-Rosser property for beta-eta-reduction in typed lambda-calculi. In A. Scedrov, editor, Seventh Annual IEEE Symposium on Logic in Computer Science, pages 453-460, Santa Cruz, California, June 1992.

144. Neil Ghani. Eta-expansions 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 164-180, Nancy, France, April 1997. Springer-Verlag LNCS 1210.

145. Jean-Yves Girard. On the unity of logic. Annals of Pure and Applied Logic, 59:201-217, 1993.

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

147. Warren D. Goldfarb. The undecidability of the second-order unification problem. Theoretical Computer Science, 13:225-230, 1981.

148. Andrew D. Gordan and Tom Melham. Five axioms of alpha-conversion. 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 173-191, Turku, Finland, August 1996. Springer-Verlag LNCS 1125.

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

150. Elsa L. Gunter. Extensions to logic programming motivated by the construction of a generic theorem prover. In Peter Schroeder-Heister, editor, Proceedings of the International Workshop on Extensions of Logic Programming, pages 223-244, Tübingen, Germany, 1989. Springer-Verlag LNAI 475.

151. 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 237-252, Munich, Germany, September 1994. Springer-Verlag LNCS 845.

152. Masami Hagiya. Generalization from partial parameterization in higher-order type theory. Theoretical Computer Science, 63:113-139, 1989.

153. Masami Hagiya. Programming by example and proving by example using higher-order unification. In M. E. Stickel, editor, Proceedings of the 10th International Conference on Automated Deduction, pages 588-602, Kaiserslautern, Germany, July 1990. Springer-Verlag LNAI 449.

154. Masami Hagiya. From programming-by-example to proving-by-example. In T. Ito and A. R. Meyer, editors, Proceedings of the International Conference on Theoretical Aspects of Computer Software, pages 387-419, Sendai, Japan, September 1991. Springer-Verlag LNCS 526.

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

156. 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):277-286, 1995.

157. 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 PMG-R37, 1987.

158. Lars Hallnäs. Partial inductive definitions. Theoretical Computer Science, 87(1):115-142, September 1991.

159. John Hannan. Implementing lambda-calculus reduction strategies in extended logic programming languages. In Lars-Henrik Eriksson, Lars Hallnäs, and Peter Schroeder-Heister, editors, Proceedings of the Second Workshop on Extensions to Logic Programming, pages 193-219. Springer-Verlag LNAI 596, January 1991.

160. 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 130-141, New Haven, Connecticut, June 1991.

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

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

163. John Hannan and Dale Miller. Enriching a meta-language with higher-order features. Technical Report MS-CIS-88-45, University of Pennsylvania, June 1988.

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

165. 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 239-255. Springer-Verlag LNCS 375, 1989.

166. John Hannan and Dale Miller. A meta-logic for functional programming. In H. Abramson and M. Rogers, editors, Meta-Programming in Logic Programming, chapter 24, pages 453-476. MIT Press, 1989.

167. 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 323-332, Nice, France, 1990.

168. John Hannan and Dale Miller. From operational semantics to abstract machines. Mathematical Structures in Computer Science, 2(4):415-459, 1992. Available in DVI format.

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

170. John J. Hannan. Investigating a Proof-Theoretic Meta-Language for Functional Programs. PhD thesis, University of Pennsylvania, January 1991. Available as Technical Report MS-CIS-91-09.

171. James Harland and David Pym. Resource-distribution via boolean constraints. In W. McCune, editor, Proceedings of the 14th International Conference on Automated Deduction (CADE-14), pages 222-236, Townsville, Australia, July 1997. Springer-Verlag LNAI 1249.

172. Robert Harper. An equational formulation of LF. Technical Report ECS-LFCS-88-67, University of Edinburgh, 1988.

173. Robert Harper. Systems of polymorphic type assignment in LF. Technical Report CMU-CS-90-144, Carnegie Mellon University, Pittsburgh, Pennsylvania, June 1990. Available in DVI format.

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

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

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

177. 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 250-272, Manchester, UK, September 1989. Springer-Verlag LNCS 389.

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

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

180. John Harrison. Floating point verification in HOL Light: The exponential function. Technical Report 428, University of Cambridge Computer Laboratory, 1997.

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

182. 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 279-298, Utrecht, The Netherlands, September 1995. Springer-Verlag LNCS 982. Available in PostScript format.

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

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

185. Daniel Hirschkoff. A full formalization of pi-calculus 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 153-169, Murray Hill, New Jersey, August 1997.

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

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

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

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

190. Gérard Huet. A unification algorithm for typed lambda-calculus. Theoretical Computer Science, 1:27-57, 1975.

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

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

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

194. 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 871-886, Paris, France, June 1991. MIT Press.

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

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

197. 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 19-61, Nijmegen, The Netherlands, May 1994. Springer-Verlag LNCS 806.

198. 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 241-255, Kaiserslautern, Germany, April 1995. Springer-Verlag LNCS 914.

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

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

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

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

203. 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. Springer-Verlag LNCS, 1997.

204. 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 855-858, Lille, France, April 1997. Springer-Verlag LNCS 1214. System abstract.

205. Kolyang, T. Santen, and B. Wolff. Correct and user-friendly implementation of transformation systems. In M.-C. Gaudel and J. Woodcock, editors, Symposium on Industrial Benefits and Advances in Formal Methods (FME'96), pages 629-648, Oxford, England, March 1996. Springer-Verlag LNCS 1051. Available in PostScript format.

206. 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 283-298, Turku, Finland, August 1996. Springer-Verlag LNCS 1125.

207. 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 359-393, Bologna, Italy, February 1993. Springer-Verlag LNAI 660. Available in DVI format.

208. 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 CS-1994-36. Available in PostScript format.

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

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

211. 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. Dezani-Ciancaglini and G. Plotkin, editors, Proceedings of the International Conference on Typed Lambda Calculi and Applications, pages 312-327, Edinburgh, Scotland, April 1995. Springer-Verlag LNCS 902.

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

213. D. Lester and S. Mintchev. Towards machine-checked compiler correctness for higher-order 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.

214. Jordi Levy. Linear second-order unification. In Harald Ganzinger, editor, Proceedings of the 7th International Conference on Rewriting Techniques and Applications, pages 332-346, New Brunswick, New Jersey, July 1996. Springer-Verlag LNCS 1103.

215. Chuck Liang. Object-Level Substitution, Unification and Generalization in Meta-Logic. PhD thesis, University of Pennsylvania, August 1995. Available in PostScript format.

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

217. D. Lugiez. Higher-order disunification: Some decidable cases. In J.-P. Jouannaud, editor, Proceedings of the First International Conference on Constraints in Computational Logics, pages 121-135, Munich, Germany, September 1994. Springer-Verlag LNCS 845.

218. Zhaohui Luo and Robert Pollack. The LEGO proof development system: A user's manual. Technical Report ECS-LFCS-92-211, University of Edinburgh, May 1992.

219. 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 26-40, Kaiserslautern, Germany, April 1995. Springer-Verlag LNCS 914.

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

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

222. 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 213-237. Springer-Verlag LNCS 806, 1994.

223. Narciso Martì-Oliet and Jose Meseguer. Rewriting logic as a logical and semantical framework. Technical Report SRI-CSL-93-05, SRI International, August 1993.

224. Per Martin-Löf. Constructive mathematics and computer programming. In Logic, Methodology and Philosophy of Science VI, pages 153-175. North-Holland, 1980.

225. Per Martin-Lö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.

226. Per Martin-Lö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.

227. Ian A. Mason. Hoare's logic in the LF. Technical Report ECS-LFCS-87-32, Laboratory for Foundations of Computer Science, University of Edinburgh, June 1987.

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

229. 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 61-82. Cambridge University Press, 1993.

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

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

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

233. 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 289-305. Springer-Verlag LNCS 664, March 1993.

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

235. 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. North-Holland, 1991.

236. 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. Springer-Verlag LNCS 663, 1993.

237. José Meseguer. General logics. In H.-D. Ebbinghaus, editor, Logic Colloquium '87, pages 275-329, Granada, Spain, July 1987. North-Holland.

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

239. Spiro Michaylov and Frank Pfenning. Natural semantics and some of its meta-theory in Elf. In L.-H. Eriksson, L. Hallnäs, and P. Schroeder-Heister, editors, Proceedings of the Second International Workshop on Extensions of Logic Programming, pages 299-344, Stockholm, Sweden, January 1991. Springer-Verlag LNAI 596. Available in DVI and PostScript formats.

240. Spiro Michaylov and Frank Pfenning. An empirical study of the runtime behavior of higher-order logic programs. In D. Miller, editor, Proceedings of the Workshop on the lambda Prolog Programming Language, pages 257-271, Philadelphia, Pennsylvania, July 1992. University of Pennsylvania. Available as Technical Report MS-CIS-92-86. Available in DVI and PostScript formats.

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

242. 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 263-290. Springer-Verlag LNCS 806, 1994.

243. Dale Miller. A theory of modules for logic programming. In Robert M. Keller, editor, Third Annual IEEE Symposium on Logic Programming, pages 106-114, Salt Lake City, Utah, September 1986.

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

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

246. Dale Miller. A logic programming language with lambda-abstraction, function variables, and simple unification. In Peter Schroeder-Heister, editor, Proceedings of the International Workshop on Extensions of Logic Programming, pages 253-281, Tübingen, Germany, 1989. Springer-Verlag LNAI 475.

247. Dale Miller. A logical analysis of modules in logic programming. Journal of Logic Programming, 6(1-2):79-108, January 1989.

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

249. Dale Miller. A logic programming language with lambda-abstraction, function variables, and simple unification. Journal of Logic and Computation, 1(4):497-536, 1991. Available in DVI format.

250. Dale Miller. Unification of simply typed lambda-terms as logic programming. In Koichi Furukawa, editor, Eighth International Logic Programming Conference, pages 255-269, Paris, France, June 1991. MIT Press. Available in DVI format.

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

252. Dale Miller, editor. Proceedings of the Workshop on the lambda Prolog Programming Language, Philadelphia, Pennsylvania, July 1992. Available as University of Pennsylvania Technical Report MS-CIS-92-86.

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

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

255. Dale Miller. A multiple-conclusion meta-logic. In S. Abramsky, editor, Ninth Annual IEEE Symposium on Logic in Computer Science, pages 272-281, Paris, France, July 1994. Available in DVI format.

256. Dale Miller and Gopalan Nadathur. Higher-order logic programming. In Ehud Shapiro, editor, Proceedings of the Third International Logic Programming Conference, pages 448-462, London, June 1986.

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

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

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

260. 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 98-105, Ithaca, NY, June 1987.

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

262. Olaf Müller and Tobias Nipkow. Combining model checking and deduction of I/O-automata. 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. Springer-Verlag LNCS 1019.

263. Olaf Müller and Tobias Nipkow. Traces of I/O-automata 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. Springer-Verlag LNCS 1214.

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

265. Gopalan Nadathur. A Higher-Order Logic as the Basis for Logic Programming. PhD thesis, University of Pennsylvania, May 1987. Available as Technical Report MS-CIS-87-48.

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

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

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

269. 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 TR-98-01, Department of Computer Science, University of Chicago. Available in PostScript format.

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

271. 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 1180-1198, Cleveland, Ohio, October 1989.

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

273. Gopalan Nadathur, Bharat Jayaraman, and Debra Sue Wilson. Implementation considerations for higher-order features in logic programming. Technical Report CS-1993-16, Department of Computer Science, Duke University, June 1993. Available in DVI format.

274. 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 148-155, San Diego, California, June 1995. IEEE Computer Society Press. Available as Technical Report CS-1994-40, Department of Computer Science, Duke University, December 1994. Available in PostScript format.

275. 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 810-827, Seattle, Washington, August 1988. MIT Press.

276. Gopalan Nadathur and Dale Miller. Higher-order Horn clauses. Journal of the ACM, 37(4):777-814, October 1990. Available in DVI format.

277. Gopalan Nadathur and Dale Miller. Higher-order 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.

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

279. Gopalan Nadathur and Frank Pfenning. The type system of a higher-order logic programming language. In Frank Pfenning, editor, Types in Logic Programming, pages 245-283. MIT Press, 1992.

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

281. 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 341-348, 1990.

282. Gopalan Nadathur and Debra Sue Wilson. A notation for lambda terms: A generalization of environments. Theoretical Computer Science, 198(1-2):49-98, May 1998. Previous version available as Technical Report TR-97-01, Department of Computer Science, University of Chicago. Available in PostScript format.

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

284. 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. Springer-Verlag LNCS 1125.

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

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

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

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

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

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

291. 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. North-Holland, 1994.

292. Tobias Nipkow. Equational reasoning in Isabelle. Science of Computer Programming, 12:123-149, 1989.

293. Tobias Nipkow. Term rewriting and beyond - theorem proving in Isabelle. Formal Aspects of Computing, 1:320-338, 1989.

294. 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 561-591. Springer-Verlag LNCS 430, 1990.

295. Tobias Nipkow. Higher-order unification, polymorphism, and subsorts. In S. Kaplan and M. Okada, editors, Proceedings of the 2nd International Workshop on Conditional and Typed Rewriting Systems, pages 436-447, Montreal, Canada, June 1990. Springer-Verlag LNCS 516.

296. Tobias Nipkow. Constructive rewriting. Computer Journal, 34:34-41, 1991.

297. Tobias Nipkow. Higher-order critical pairs. In G. Kahn, editor, Sixth Annual IEEE Symposium on Logic in Computer Science, pages 342-349, Amsterdam, The Netherlands, July 1991.

298. Tobias Nipkow. Functional unification of higher-order patterns. In M. Vardi, editor, Eighth Annual IEEE Symposium on Logic in Computer Science, pages 64-74, Montreal, Canada, June 1993.

299. Tobias Nipkow. Order-sorted polymorphism in Isabelle. In G. Huet and G. Plotkin, editors, Logical Environments, pages 164-188. Cambridge University Press, 1993.

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

301. Tobias Nipkow. More Church-Rosser proofs (in Isabelle/HOL). In M.A. McRobbie and J.K. Slaney, editors, Proceedings of the 13th International Conference on Automated Deduction (CADE-13), pages 733-747, New Brunswick, New Jersey, July 1996. Springer-Verlag LNAI 1104.

302. 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 180-192. Springer-Verlag LNCS 1180, 1996.

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

304. Tobias Nipkow. Winskel is (almost) right: Towards a mechanized semantics textbook. Formal Aspects of Computing, 10:171-186, 1998.

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

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

307. Tobias Nipkow and Lawrence C. Paulson. Isabelle-91. In D. Kapur, editor, Proceedings of the 11th International Conference on Automated Deduction, pages 673-676, Saratoga Springs, NY, 1992. Springer-Verlag LNAI 607. System abstract. Available in DVI format.

308. 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 101-119, Båstad, Sweden, June 1994. Springer-Verlag LNCS 996.

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

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

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

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

313. 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 373-389, Jerusalem, Israel, June 1990. MIT Press. Available in DVI format.

314. Lawrence C. Paulson. Natural deduction as higher-order resolution. Journal of Logic Programming, 3:237-258, 1986. Available in DVI format.

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

316. 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 772-773, Argonne, Illinois, 1988. Springer Verlag LNCS 310. System abstract. Available in DVI format.

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

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

319. 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 415-475. Oxford University Press, 1992. Available in DVI format.

320. Lawrence C. Paulson. Co-induction and co-recursion in higher-order logic. Technical Report 304, University of Cambridge, Computer Laboratory, July 1993. Available in PostScript format.

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

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

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

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

325. 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 148-161, Nancy, France, June 1994. Springer-Verlag LNAI 814. Available in DVI format.

326. Lawrence C. Paulson. Isabelle: A Generic Theorem Prover. Springer-Verlag LNCS 828, 1994.

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

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

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

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

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

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

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

334. Lawrence C. Paulson. Mechanizing coinduction and corecursion in higher-order logic. Journal of Logic and Computation, 7(2):175-204, March 1997.

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

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

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

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

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

340. Patricia Peratto. Course-of-values recursion in Martin-Löf's type theory. Master's thesis, Instituto de Computación, Facultad de Ingenieria, Universidad de la Republica Oriental del Uruguay, Montevideo, Uruguay, 1991.

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

342. Patricia Peratto. Course-of-values 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.

343. Frank Pfenning. Partial polymorphic type inference and higher-order unification. In Proceedings of the 1988 ACM Conference on Lisp and Functional Programming, pages 153-163, Snowbird, Utah, July 1988. ACM Press.

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

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

346. Frank Pfenning. Unification and anti-unification in the Calculus of Constructions. In Sixth Annual IEEE Symposium on Logic in Computer Science, pages 74-85, Amsterdam, The Netherlands, July 1991. Available in DVI and PostScript formats.

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

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

349. Frank Pfenning. A proof of the Church-Rosser 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 CMU-CS-92-186, September 1992. Available in DVI and PostScript formats.

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

351. Frank Pfenning. Elf: A meta-language for deductive systems. In A. Bundy, editor, Proceedings of the 12th International Conference on Automated Deduction, pages 811-815, Nancy, France, June 1994. Springer-Verlag LNAI 814. System abstract. Available in DVI and PostScript formats.

352. Frank Pfenning. Structural cut elimination in linear logic. Technical Report CMU-CS-94-222, Department of Computer Science, Carnegie Mellon University, December 1994. Available in PostScript format.

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

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

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

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

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

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

359. Frank Pfenning and Conal Elliott. Higher-order abstract syntax. In Proceedings of the ACM SIGPLAN '88 Symposium on Language Design and Implementation, pages 199-208, Atlanta, Georgia, June 1988. Available in PostScript format.

360. Frank Pfenning and Ekkehard Rohwedder. Implementing the meta-theory of deductive systems. In D. Kapur, editor, Proceedings of the 11th International Conference on Automated Deduction, pages 537-551, Saratoga Springs, New York, June 1992. Springer-Verlag LNAI 607. Available in DVI and PostScript formats.

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

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

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

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

365. Frank Pfenning and Hao-Chi Wong. On a modal lambda-calculus 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.

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

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

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

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

370. Robert Pollack. Closure under alpha-conversion. In Henk Barendregt and Tobias Nipkow, editors, Proceedings of the Workshop on Types for Proofs and Programs, pages 313-332, Nijmegen, The Netherlands, May 1993. Springer-Verlag LNCS 806.

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

372. Robert Pollack. Polishing up the Tait-Martin-Löf proof of the Church-Rosser theorem. Unpublished note, January 1995. Available in PostScript format.

373. Robert Pollack. A verified typechecker. In M. Dezani-Ciancaglini and G. Plotkin, editors, Proceedings of the International Conference on Typed Lambda Calculi and Applications, pages 365-380, Edinburgh, Scotland, April 1995. Springer-Verlag LNCS 902.

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

375. 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 140-161, Båstad, Sweden, June 1994. Springer-Verlag LNCS 996.

376. Christian Prehofer. Decidable higher-order unification problems. In Proceedings of the 12th International Conference on Automated Deduction, pages 635-649, Nancy, France, June 1994. Springer LNAI 814.

377. Christian Prehofer. Higher-order narrowing. In Proceedings of the Ninth Annual IEEE Symposium on Logic in Computer Science, pages 507-516, Paris, France, July 1994. IEEE Computer Society Press.

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

379. Thomas Puls. Annotation Logic for Standard ML. PhD thesis, Technical University of Denmark, Lyngby, October 1990. Department of Computer Science Report ID-TR:1990-74.

380. 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. Springer-Verlag LNCS 1125. Available in DVI format.

381. 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 Type-Theoretic Languages, pages 101-108, New Brunswick, New Jersey, July 1996.

382. David Pym. Proofs, Search and Computation in General Logic. PhD thesis, University of Edinburgh, 1990. Available as CST-69-90, also published as ECS-LFCS-90-125.

383. David Pym. A unification algorithm for the lambda-pi-calculus. International Journal of Foundations of Computer Science, 3(3):333-378, September 1992.

384. David Pym and Lincoln Wallen. Investigations into proof-search in a system of first-order dependent function types. In M.E. Stickel, editor, Proceedings of the 10th International Conference on Automated Deduction, pages 236-250, Kaiserslautern, Germany, July 1990. Springer-Verlag LNCS 449.

385. David Pym and Lincoln A. Wallen. Proof search in the lambda-pi-calculus. In Gérard Huet and Gordon Plotkin, editors, Logical Frameworks, pages 309-340. Cambridge University Press, 1991.

386. David Pym and Lincoln A. Wallen. Logic programming via proof-valued computations. In K. Broda, editor, Proceedings of the 4th UK Annual Conference on Logic Programming, London, March 1992. Springer-Verlag.

387. David J. Pym. A note on the proof theory of the lambda-pi-calculus. Studia Logica, 54(2):199-230, 1995.

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

389. David J. Pym and James A. Harland. The uniform proof-theoretic foundation of linear logic programming. Journal of Logic and Computation, 4(2):175-207, April 1994.

390. Zhenyu Qian. Linear unification of higher-order patterns. In M.-C. Gaudel and J.-P. Jouannaud, editors, Proceedings of the Colloquium on Trees in Algebra and Programming, pages 391-405, Orsay, France, April 1993. Springer-Verlag LNCS 668.

391. Zhenyu Qian. Unification of higher-order patterns in linear time and space. Journal of Logic and Computation, 6(3):315-341, 1995.

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

393. 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 186-200, New Brunswick, New Jersey, July 1996. Springer-Verlag LNAI 1104.

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

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

396. Ekkehard Rohwedder. Verifying the meta-theory of deductive systems. Thesis Proposal, February 1994.

397. Ekkehard Rohwedder. Verifying the Meta-Theory of Deductive Systems. PhD thesis, School of Computer Science, Carnegie Mellon University, 1996. Forthcoming.

398. Ekkehard Rohwedder and Frank Pfenning. Mode and termination checking for higher-order logic programs. In Hanne Riis Nielson, editor, Proceedings of the European Symposium on Programming, pages 296-310, Linköping, Sweden, April 1996. Springer-Verlag LNCS 1058. Available in PostScript format.

399. 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 173-187. MIT Press, 1991.

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

401. Lars Rossen. Proving (facts about) Ruby. In G. Birtwistle, editor, IV Higher Order Workshop, pages 265-283, Banff, Alberta, September 1990. Springer-Verlag Workshops in Computing.

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

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

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

405. 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 628-642, New Brunswick, New Jersey, July 1996. Springer-Verlag LNAI 1104.

406. 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. Springer-Verlag LNCS.

407. Amokrane Saïbi. Formalization of a lambda-calculus 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 183-202, Båstad, Sweden, June 1994. Springer-Verlag LNCS 996.

408. Anne Salvesen. The Church-Rosser theorem for LF with beta-eta-reduction. Unpublished notes to a talk given at the First Workshop on Logical Frameworks in Antibes, France, May 1990.

409. 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 351-365, Enschede, The Netherlands, April 1997. Springer-Verlag LNCS 1217.

410. Peter Schroeder-Heister. Structural frameworks, substructural logics, and the role of elimination inferences. In Gérard Huet and Gordon Plotkin, editors, Logical Frameworks, pages 385-403. Cambridge University Press, 1991.

411. Peter Schroeder-Heister. Definitional reflection and the completion. In R. Dyckhoff, editor, Proceedings of the 4th International Workshop on Extensions of Logic Programming, pages 333-347. Springer-Verlag LNAI 798, 1993.

412. Peter Schroeder-Heister. Rules of definitional reflection. In M. Vardi, editor, Proceedings of the Eighth Annual IEEE Symposium on Logic in Computer Science, pages 222-232, Montreal, Canada, June 1993.

413. 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 CMU-CS-95-218.

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

415. N. Shankar. A mechanical proof of the Church-Rosser theorem. Journal of the Association for Computing Machinery, 35(3):475-522, July 1988.

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

417. 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 259-274, Murray Hill, New Jersey, August 1997.

418. 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 291-306, Murray Hill, New Jersey, August 1997.

419. Wayne Snyder and Jean H. Gallier. Higher order unification revisited: Complete sets of transformations. Journal of Symbolic Computation, 8(1-2):101-140, 1989.

420. 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. Springer-Verlag LNCS.

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

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

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

424. H. Tej and B. Wolff. A corrected failure-divergence 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.

425. 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 230-244, Montreal, Canada, July 1995. Springer-Verlag LNCS 936.

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

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

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

429. J. van de Pol and H. Schwichtenberg. Strict functionals for termination proofs. In M. Dezani-Ciancaglini and G. Plotkin, editors, Proceedings of the International Conference on Typed Lambda Calculi and Applications, pages 350-364, Edinburgh, Scotland, April 1995. Springer-Verlag LNCS 902.

430. Vincent van Oostrom. Higher-order families. In Harald Ganzinger, editor, Proceedings of the 7th International Conference on Rewriting Techniques and Applications, pages 392-407, New Brunswick, New Jersey, July 1996. Springer-Verlag LNCS 1103.

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

432. Myra VanInwegen. The Machine-Assisted Proof of Programming Language Properties. PhD thesis, University of Pennsylvania, August 1996.

433. Luca Viganò. A Framework for Non-Classical Logics. PhD thesis, Universität des Saarlandes, September 1997.

434. Roberto Virga. Higher-order superposition for dependent types. In Harald Ganzinger, editor, Proceedings of the 7th International Conference on Rewriting Techniques and Applications, pages 123-137, New Brunswick, New Jersey, July 1996. Springer-Verlag LNCS 1103. Extended version available as Technical Report CMU-CS-95-150, May 1995. Available in PostScript format.

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

436. 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 154-168, New Brunswick, New Jersey, July 1996. Springer-Verlag LNCS 1103.

437. David von Oheimb and Thomas F. Gritzner. RALL: Machine-supported proofs for relational algebra. In W. McCune, editor, Proceedings of the 14th International Conference on Automated Deduction, pages 380-394, Townsville, Australia, July 1997. Springer-Verlag LNCS 1249.

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

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

440. Lincoln A. Wallen. Automated Deduction in Non-Classical Logics. MIT Press, 1990.

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

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

443. David A. Wolfram. Intractable unifiability problems and backtracking. Journal of Automated Reasoning, 5:37-47, 1989.

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

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

446. David A. Wolfram. Rewriting, and equational unification: The higher-order cases. In Ronald V. Book, editor, Proceedings of the Fourth International Conference on Rewriting Techniques and Applications, pages 25-36, Como, Italy, April 1991. Springer-Verlag LNCS 488.

447. 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 366-383, Nijmegen, The Netherlands, May 1993. Springer-Verlag LNCS 806.

448. David A. Wolfram. A semantics for lambda Prolog. Theoretical Computer Science, 136(1):277-289, 1994.

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