Title
The Disjunctive Constrained Lambda Calculus
Abstract
In previous works 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 an extension of that calculus is presented, which is obtained by adding existential quantifiers and new rules for handling disjunctive terms and multiple solutions. The problem of shared variables is avoided by choosing a call-by-value application policy. The overall result is a very smoothly working language. The calculus satisfies the Church-Rosser property; the normal forms are given. Finally typical examples are presented.
Year
DOI
Venue
1996
10.1007/3-540-62064-8_25
Ershov Memorial Conference
Keywords
Field
DocType
lambda calculus,disjunctive constrained lambda calculus,denotational semantics,constraints,functional programming.,multiple solutions,satisfiability,functional programming,normal form
Simply typed lambda calculus,Typed lambda calculus,Normalisation by evaluation,Natural deduction,Computer science,Lambda cube,System F,Algorithm,Church encoding,Pure type system,Calculus
Conference
ISBN
Citations 
PageRank 
3-540-62064-8
1
0.38
References 
Authors
6
2
Name
Order
Citations
PageRank
Luis Mandel1456.78
María Victoria Cengarle217517.82