First-order constrained lambda calculus

In (Crossley et al., 1993a; Crossley et al., 1993b; Mandel, 1995) 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 problem and gives a very smoothly working language. We present a proof of the Church-Rosser property and the denotational semantics of the whole calculus.