Crossley, John N.; Mandel, Luis; Wirsing, Martin First-order constrained lambda calculus. (English) Zbl 0893.03002 Baader, Franz (ed.) et al., Frontiers of combining systems. First international workshop, Munich, Germany, March 26–29, 1996. Dordrecht: Kluwer Academic Publishers. Appl. Log. Ser. 3, 339-356 (1996). Summary: In earlier publications of the authors a calculus which extends the traditional lambda calculus by the addition of constraints was presented. The constraints can be used passively for restricting the range of variables and actively for computing solutions of goals. Here we present an extension of that calculus obtained by adding existential quantifiers and new rules for handling the new terms. This avoids the problem of shared variables and gives a very smoothly working language. We present a proof of the Church-Rosser property and the denotational semantics of the whole calculus.For the entire collection see [Zbl 0885.00046]. MSC: 03B40 Combinatory logic and lambda calculus 03B70 Logic in computer science 68Q55 Semantics in the theory of computing 68N01 General topics in the theory of software Keywords:constraint programming; lambda calculus; constraints; existential quantifiers; Church-Rosser property; denotational semantics Citations:Zbl 0864.68062 PDFBibTeX XMLCite \textit{J. N. Crossley} et al., Appl. Log. Ser. 3, 339--356 (1996; Zbl 0893.03002)