Abstract | ||
---|---|---|
It is well known that the simple types of closed lambda terms or combinators can be interpreted as the theorems of intuitionistic implicational logic (H→). Venneri, using an equivalence between the intersection type system for lambda calculus, without the universal type ω, TA∧λ, and a similar system for combinators, TA∧, shows that the types of TA∧λ are the theorems of a Hilbert-style sublogic of ... |
Year | DOI | Venue |
---|---|---|
2002 | 10.1093/jigpal/10.4.357 | Logic Journal of the IGPL |
Field | DocType | Volume |
Discrete mathematics,Combinatory logic,Mathematics,Lambda | Journal | 10 |
Issue | ISSN | Citations |
4 | 1367-0751 | 2 |
PageRank | References | Authors |
0.40 | 0 | 1 |
Name | Order | Citations | PageRank |
---|---|---|---|
Martin W. Bunder | 1 | 64 | 16.78 |