Name
Abstract | ||
|---|---|---|
In 1990, J. L. Krivine introduced the notion of storage operator to simulate, in lambda-calculus, the ''call by value'' in a context of a ''call by name''. J. L. Krivine has showed that, using Godel translation from classical to intuitionistic logic, we can find a simple type for storage operators in AF2 type system. In the present paper we give a general type for storage operators in a slight extension of AF2. At the end we give (without proof) a generalization of this result to other types. |
Year | DOI | Venue |
|---|---|---|
1995 | 10.1002/malq.19950410407 | MATHEMATICAL LOGIC QUARTERLY |
Keywords | Field | DocType |
STORAGE OPERATOR, TYPED LAMBDA-CALCULUS, TYPE SYSTEM, AF2 TYPE SYSTEM, CHURCH INTEGER, BETA-EQUIVALENCE, HEAD NORMAL FORM, HEAD REDUCTION, GODEL TRANSLATION, DATA TYPE | Intuitionistic logic,Discrete mathematics,Simply typed lambda calculus,Algebra,Type theory,Operator (computer programming),Type inhabitation,Pure type system,Dependent type,Mathematics,Curry–Howard correspondence | Journal |
Volume | Issue | ISSN |
41 | 4 | 0942-5616 |
Citations | PageRank | References |
3 | 0.59 | 0 |
Authors | ||
1 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Karim Nour | 1 | 65 | 15.07 |