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 Mandel | 1 | 45 | 6.78 |
María Victoria Cengarle | 2 | 175 | 17.82 |