** 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)
    Technical Report, December 1998.