M. Abadi, L. Cardelli, P. Curien, and J. Lévy, Abstract, Journal of Functional Programming, vol.34, issue.04, pp.375-416, 1991.
DOI : 10.1016/0304-3975(86)90035-6

R. Backofen, J. Rogers, and K. Vijay-shanker, A first-order axiomatization of the theory of finite trees, Journal of Logic, Language and Information, vol.18, issue.4, pp.5-39, 1995.
DOI : 10.1007/BF01048403

M. Bodirsky, K. Erk, A. Koller, and J. Niehren, Beta reduction constraints Full version, 2001.
DOI : 10.1007/3-540-45127-7_5
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.116.6634

M. Bodirsky, K. Erk, A. Koller, and J. Niehren, Underspecified beta reduction, Proceedings of the 39th Annual Meeting on Association for Computational Linguistics , ACL '01, 2001.
DOI : 10.3115/1073012.1073023
URL : https://hal.archives-ouvertes.fr/inria-00536805

D. Duchier and J. Niehren, Dominance Constraints with Set Operators, First International Conference on Computational Logic (CL2000), 2000.
DOI : 10.1007/3-540-44957-4_22
URL : https://hal.archives-ouvertes.fr/inria-00536806

M. Egg, A. Koller, and J. Niehren, The Constraint Language for Lambda Structures, Journal of Logic, Language, and Information, 2001.
URL : https://hal.archives-ouvertes.fr/inria-00536795

M. Egg, J. Niehren, P. Ruhrberg, and F. Xu, Constraints over lambda-structures in semantic underspecification, Proceedings COLING/ACL'98, 1998.
URL : https://hal.archives-ouvertes.fr/inria-00536807

K. Erk, A. Koller, and J. Niehren, Processing underspecified semantic descriptions in CLLS, Journal of Language & Computation, 2001.

K. Erk and J. Niehren, Parallelism Constraints, Int. Conference on Rewriting Techniques and Applications, pp.110-126, 2000.
DOI : 10.1007/10721975_8
URL : https://hal.archives-ouvertes.fr/inria-00536808

G. P. Huet, A unification algorithm for typed ??-calculus, Theoretical Computer Science, vol.1, issue.1, pp.27-57, 1975.
DOI : 10.1016/0304-3975(75)90011-0

J. Lamping, An algorithm for optimal lambda calculus reduction, Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '90, pp.16-30, 1990.
DOI : 10.1145/96709.96711

J. Lévy, Linear second-order unification, 7th Int. Conference on Rewriting Techniques and Applications, pp.332-346, 1996.
DOI : 10.1007/3-540-61464-8_63

M. P. Marcus, D. Hindle, and M. M. Fleck, D-theory, Proceedings of the 21st annual meeting on Association for Computational Linguistics -, pp.129-136, 1983.
DOI : 10.3115/981311.981337

U. Reyle, Dealing with Ambiguities by Underspecification: Construction, Representation and Deduction, Journal of Semantics, vol.10, issue.2, pp.123-179, 1993.
DOI : 10.1093/jos/10.2.123

1. and .. ?. {1, B m ) ? ? with Y ?b(A k ), Z?b(A k ) in ? for some k, m}. By closure under (P.distr.eq), we have either Z=Y ? ? or Z =Y ? ?

(. P. Distr, eq): No new variables have been added. (P.trans.h), P.trans.v), (P.diff.1), (P.diff.2): Now new path equalities have been added

(. L. Same, seg), (L.diff.seg), (L.outside): We have not added any lambda binding literals. It remains to show that we have not recently acquired new information on whether a binder or a bound variable is situated in a group