• On type theory, lambda calculus and explicit substitutions
• On termination of term rewrite systems
• On confluence
• On inference
• On syntax

• The Decision of Equality in Recursive Types, an early proof. Concerning the Syntax of ALGOL 68 by Claude Pair, in Algol Bulletin n. 31, March 1970. This file contains copies of a paper written in 1969 by Claude Pair that shows that the equality in recursive types is decidable.
• The first calculus of explicit substitutions A namefree lambda calculus with facilities for internal definition of expressions and segments by N. G. de Bruijn. Technological University Eindhoven, Netherlands, Department of Mathematics, (1978), (TH-Report), Number 78-WSK-03. This report is probably the first presentation ever of a calculus of explicit substitutions.
• Une généralisation de la théorie des types en lambda-calcul (A generalization of type theory in lambda-calcul) by Patrick Sallé, in R.A.I.R.O Informatique théorique/Thoeretical Informatics, vol 4, n°3&4, (1980), one of the first paper on intersection types.
• Alcune proprieta delle forme beta-eta normali nel lambda-K calculo (Some properties of beta-eta-normal formal in lambda-K calculus) (1968) by Corrado Böhm (in Italian). The famous paper where Böhm's seperability theorem is presented for the first time (see Barendregt  "The lambda calculus"  1984, Elsevier, § 10.4)
• Vincent Danos Ph.D. thesis (20 June 1990), one of the first PhD on linear logic, La Logique linéaire appliquée à divers processus de normalisation (principalment du lambda-calcul). (Thanks to Russ Hammer).
• Robin Gandy Ph.D. thesis (September 1952) On axiomatic systems in Mathematics and theories in physics. (Thanks to Russ Hammer).

On termination of term rewrite systems

• On the termination of Markov algorithms Zohar Manna and Steven Ness, Proc. of the Third Hawaii International Conference on System Science, Honolulu, HI, pp. 789-792 (January 1970)

  Despite its name, it is a paper on termination of term rewriting systems, the second (after Saul Gorn's paper. (1967), Handling the growth by definition of mechanical languages, Proceedings of the AFIPS 1967 Spring Joint Computer Conference, Philadelphia, PA, Vol. 30, AFIPS Press, pages 213--224, thanks to Nachum Dershowitz for the reference) proposing a method for proving termination of term rewrite systems, actually a method based on linear function (i. e., polynomial of degree 1).

• On the Uniform Halting Problem for Term Rewriting Systems Gerard Huet and Dallas Lankford (March 1978) Rapport IRIA Laboria N° 283, Rocquencourt, France.

  The reference for the undecidability of the termination of Term Rewriting Systems and the decidability of the termination of Ground Term Rewriting Systems.

• Well-founded Orderings for Proving Termination of Term Rewriting Systems David Plaisted (July 1978), Dept. of Computer Science Report, Research Report 78-932 University of Illinois At Urbana-Champaign

  An ancestor of the famous recursive path ordering.

• A Recursively Defined Ordering for Proving Termination of Term Rewriting Systems by David Plaisted (September 1978), Dept. of Computer Science Report, Research Report 78-943 University of Illinois At Urbana-Champaign

  A sibling of the recursive path ordering.

• On Proving term rewriting systems are Noetherian by Dallas Lankford (May 1979).

  This folk paper presents methods for proving termination of TRS based on interpretations, especially on polynomial interpretations.

• Attempts for generalizing the recursive path orderings by Sam Kamin and Jean-Jacques Levy (February 1st 1980).

  This folk handwritten paper by Sam Kamin and Jean-Jacques Lévy is the first reference to the semantic path ordering and the lexicographic path ordering

• Dershowitzeries by Jean-Jacques Levy (Oct 1981).

  Those are handwritten lecture notes, in French, of a talk that Jean-Jacques Levy gave on October 23 1981 about what is known now as the semantic path ordering and which he calls rpo.

• Kruskaleries by Jean-Jacques Levy (Oct 1981).

  Those are handwritten lecture notes, in French, of a talk that Jean-Jacques Levy gave on October 15 1981 about Nash-William proof of Kruskal theorem. This paper was the origin of the following paper: J. Gallier. What's so special about Kruskal's Theorem and the ordinal Gamma_0 ? A survey of some results in proof theory. Annals of Pure and Applied Logic 53 (1991), 199-260.

• On Multiset Orderings, by Jean-Pierre Jouannaud and Pierrre Lescanne, preliminary version of a paper published in Inf. Process. Lett. 15(2) 57-63 (1982).

• Contribution to Mechanical Mathematics by Renato Iturriaga.   Iturriaga's PhD where methods for proving termination of Term Rewriting systems were first proposed.

On confluence

• On Theories with a Combinatorial Definition of "Equivalence" by M. H. A. Newman Annals of Mathematics, Vol. 43, N. 2, April, 1942. This paper is also available here.

  The proof of the famous Newman Lemma.

  An analysis of Newman's proof has been made by the Vincent van Oostrom

• A General Church-Rosser Theorem by Peter Aczel and its corrections, (July 1978)

  The last section of this paper introduces contraction schemes that were latter on generalized by Klop. It also includes a parallel reduction that extends the one of Tait and Martin-Löf and that corresponds to superdevelopmennts as it was defined by Femke van Raamsdonk.

• The Church-Rosser property and a result in Combinatory Logic. A Thesis submitted for the Degree of Doctor of Philosophy in the Faculty of Science, in the University of Newcastle upon Tyne, by James Roger Hindley, July, 1964. 8.5 Mb.

  The historical PhD of Roger Hindley (see also this), which establishes the Church-Rosser property of lambda-calculus. Notice that the less interesting chapter 6 has been removed.

• Canonical Inference by Dallas Lankford, 1975 

  Presentation of a refutation complete method in presence of rewrite rules based on paramodulation.

• David Schroer's Ph.D. thesis (June 1965), entitled The Church-Rosser Theorem contains probably the first detailed correct proof of the Church-Rosser Theorem. (Thanks to J. Roger Hindley).

On syntax

• Automata in General Algebra Samuel Eilenberg, Jesse B. Wright, Information and Control 11(4): 452-470 (1967).

  This paper is by one of the founders of category theory and might deserve to be better known at the time people look at syntax with a new eye.

Thanks to Peter Aczel, Frédéric Blanqui, Nachum Dershowitz, Mariangiola Dezani, Roger Hindley, Russ Hammer, Gérard Huet, Luca Paolini, Claude Pair, David Plaisted, and Damien Pous for their contribution to this page and to Jean-Jacques Levy for his support.