** Selected Writings of Jean Gallier

1. Nondeterministic Flow Chart Programs with Recursive Procedures: Semantics and Correctness I. Theoretical Computer Science, 13(2), 193-224 (1981).

2. Nondeterministic Flow Chart Programs with Recursive Procedures: Semantics and Correctness II. Theoretical Computer Science, 13(3), 239-270 (1981).

3. DPDA's in "Atomic Normal Form" and Application to Equivalence Problems. Special issue of Theoretical Computer Science, 14(2), 155-186 (1981).

4. n-Rational Algebras, Part I: Basic Properties and Free Algebras. SIAM on Computing, 13(4), 750-775 (1984).

5. n-Rational Algebras, Part II: Varieties and Logic of Inequalities. SIAM on Computing, 13(4), 776-794 (1984).

6. Linear-time algorithms for testing the satisfiability of propositional Horn Formulae. (With William Dowling).

7. HORNLOG: A Graph Based Interpreter for General Horn Clauses. (With Stan Raatz). Journal of Logic Programming, 4(2), 119-155 (1987).

8. Extending SLD-Resolution to Equational Horn Clauses using E-Unification. (With Stan Raatz). Special issue of Journal of Logic Programming, 6(1-2), 3-56 (1989).

9. Complete Sets of Transformations For General E-Unification. (With Wayne Snyder). Special issue of Theoretical Computer Science, 67(2-3), 203-260 (1989).

10. Higher-Order Unification Revisited: Complete Sets of Transformations. (With Wayne Snyder). Special issue of Journal of Symbolic Computation, 8(1-2), 101-140 (1989).

11. Rigid E-Unification: NP-completeness and Applications to Theorem Proving. (With P. Narendran, David Plaisted, and Wayne Snyder). Special issue of Information and Computation, 87(1/2), 129-195 (1990).

12. 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, Vol. 53, 199-260 (1991). (pdf)

13. Theorem Proving Using Equational Matings and Rigid E-Unification. (with Paliath Narendran, Stan Raatz, and Wayne Snyder). J.ACM, Vol. 39, No. 2, 377-429 (April 1992).

14. Polymorphic Rewriting Conserves Algebraic Strong Normalization. (With Val Breazu-Tannen). Special issue of Theoretical Computer Science, 83(1), 3-28 (1991).

15. An Algorithm for Finding Canonical Sets of Ground Rewrite Rules in Polynomial Time. (With Paliath Narendran, David Plaisted, Stan Raatz, and Wayne Snyder). J.ACM, Vol. 40, No. 1, 1-16 (1993).

16. Constructive Logics. Part I: A Tutorial on Proof Systems and Typed lambda-Calculi. (pdf)
    Theoretical Computer Science, 110(2), 249-239 (1993).

17. Constructive Logics. Part II: Linear Logic and Proof Nets. (pdf)
    Technical Report, CIS Department, University of Pennsylvania, 1991.

18. Polymorphic Rewriting Conserves Algebraic Confluence. (With Val Breazu-Tannen). Information and Computation, Vol. 14, No. 1, 1-29, (1994).

19. Proving Properties of Typed lambda-Terms Using Realizability, Covers, and Sheaves. (pdf)
    Theoretical Computer Science, 142(2), 299-368, (1995).

20. Logic for Computer Science: Foundations of Automatic Theorem Proving. Wiley, pp. 511 (1986).

21. The Semantics of Recursive Programs with Function Parameters of Finite Types: n-rational Algebras and Logic of Inequalities. In Algebraic Methods in Semantics, Maurice Nivat and John Reynolds, editors, Cambridge University Press, 313-362 (1985).

22. On Girard's "Candidats de Reductibilité." In Logic and Computer Science, Odifreddi, editor, Academic Press, 123-203 (1990). (pdf)

23. Designing Unification Procedures Using Transformations: A Survey. (With Wayne Snyder). In Logic from Computer Science, Iannis Moschovakis, editor, Springer Verlag, 153-215 (1991).

24. On the Correspondence Between Proofs and lambda-Terms. (pdf)
    Cahiers du Centre de Logique, Philippe DeGroote, Editor, Université Catholique de Louvain, 1995.

25. Unification Procedures in Automated Deduction Methods Based on Matings: A Survey. (pdf)
    In Tree automata and languages, Edited by M. Nivat and A. Podelski, Elsevier, 439-485 (1992).

26. Kripke Models and the (in)equational logic of the second-order lambda-Calculus (pdf)
    Annals of Pure and Applied Logic , 84, 257-316, (1997)

27. Typing untyped lambda terms, or Reducibility Strikes Again! (pdf)
    Annals of Pure and Applied Logic , 91, 231-270, (1998)

28. A Note on Logical PERs and Reducibility. Logical Relations strike again! (pdf)
    Val Tannen Festschrift, 2024.