Disjunctive Constraint Lambda Calculi

Earlier we introduced Constraint Lambda Calculi which integrate constraint solving with functional programming for the simple case where the constraint solver produces no more than one solution to a set of constraints. We now introduce two forms of Constraint Lambda Calculi which allow for multiple constraint solutions. Moreover, the language also permits the use of disjunctions between constraints rather than just conjunction. These calculi are the Unrestricted, and the Restricted, Disjunctive Constraint-Lambda Calculi. We establish a limited form of confluence for the unrestricted calculus and a stronger form for the restricted one. We also discuss the denotational semantics of our calculi and some implementation issues.