Abstract, Journal of Functional Programming, vol.34, issue.04, pp.375-416, 1991. ,
DOI : 10.1016/0304-3975(86)90035-6
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
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
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
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
The Constraint Language for Lambda Structures, Journal of Logic, Language, and Information, 2001. ,
URL : https://hal.archives-ouvertes.fr/inria-00536795
Constraints over lambda-structures in semantic underspecification, Proceedings COLING/ACL'98, 1998. ,
URL : https://hal.archives-ouvertes.fr/inria-00536807
Processing underspecified semantic descriptions in CLLS, Journal of Language & Computation, 2001. ,
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
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
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
Linear second-order unification, 7th Int. Conference on Rewriting Techniques and Applications, pp.332-346, 1996. ,
DOI : 10.1007/3-540-61464-8_63
D-theory, Proceedings of the 21st annual meeting on Association for Computational Linguistics -, pp.129-136, 1983. ,
DOI : 10.3115/981311.981337
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
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 ? ? ,
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 ,
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 ,