Jean Gallier

A corrected version of the original Wiley edition (pp. 511, 1986), published by Dover, June 2015.

---

DOVER EDITION (June 2015)

Terms and Conditions

• By downloading these files you are agreeing to the following conditions of use: Copyright 2015 by Jean Gallier. This material may be reproduced for any educational purpose, multiple copies may be made for classes, etc. Charges, if any, for reproduced copies must be no more than enough to recover reasonable costs of reproduction. Reproduction for commercial purposes is prohibited. The cover page, which contains these terms and conditions, must be included in all distributed copies. It is not permitted to post this book for downloading in any other web location, though links to this page may be freely given.

• Book (pdf)

---

OTHER LOGIC PAPERS OF INTEREST

• 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)

• 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)
  

• 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)

• 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

---

Jean Gallier
2003年6月6日