Papers on lambda-calculus, constructive logic, unification,
automated theorem proving

• Linear-time algorithms for testing the satisfiability of propositional Horn Formulae. (With William Dowling).
  Journal of Logic Programming, 1(3), 267-284 (1984) (pdf)

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

• 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).
  (pdf)

• Snyder, W. and Gallier, J. Higher-Order Unification Revisited: Complete Sets of Transformations.
  Journal of Symbolic Computation, 8(5), 101--140 (1989).
  (pdf)

• Snyder, W. and Gallier, J. Complete Sets of Transformations for General E-Unification.
  Theoretical Computer Science, 67, 203-260 (1989).
  (pdf),  

• On Girard's "Candidats de Reductibilite'."
  In Logic and Computer Science. P. Odifreddi, Editor, Academic Press, 123-203 (1989).
  (pdf)  

• Gallier, J., Narendran, P., Plaisted, D. and Snyder, W. Rigid E-Unification: NP-Completeness and Applications to Equational Matings.
  Information and Computation, 87(5), 129-195 (1990).
  (pdf)

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

• Tannen Val and Gallier, J. Polymorphic rewriting conserves algebraic strong normalization.
  Theoretical Computer Science, 83(2), 3-28 (1991).
  (pdf)

• Gallier, J., Narendran, P., Raatz, S. and Snyder, W. Theorem Proving Using Equational Matings and
  Rigid E-Unification.
  J. ACM, 39(2), 377-429 (1992).
  (pdf)

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

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

• Snyder, W., Narendran, P., Plaisted, D., Raatz, S. and Snyder. W.
  An Algorithm for Finding Canonical Sets of Ground Rewrite Rules in Polynomial Time.
  Journal of the ACM, 40(1), 1-16 (1993).
  (pdf)

• Tannen Val. and Gallier, J. Polymorphic rewriting conserves algebraic confluence.
  Information and Computation, 114, 1-29 (1994).
  (pdf)
  

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

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

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

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

• A proof of strong normalization for the theory of constructions using a Kripke-like interpretation.
  First Annual Workshop on Logical Frameworks, Antibes, May 1990.
  (pdf)

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

• Unification in Automated Theorem Proving. Matings,
  Equational Matings. Rigid E-Unification. A Tutorial. (2025)
  Revised version of a paper published in
  Tree automata and languages, Edited by M. Nivat and A. Podelski, Elsevier, 439-485 (1992).
  (pdf)

• The completeness of propositional resolution, A simple constructive proof.
  LMCS, 2(5), pp. 1-7, (November, 2006).
  (pdf)

Back to Gallier's books (complete list)

Back to Gallier Homepage