Name
Abstract | ||
|---|---|---|
Provable realizability with untyped lambda-terms as realizers of formulas of the propositional language with implication and the so called "strong conjunction" is proved to be equivalent to type inference in the system with intersection types of Coppo and Dezani. A similar equivalence is proved if realizers are terms of Combinatory Logic. These results are used to derive properties of models of lambda-calculus and Combinatory Logic. |
Year | DOI | Venue |
|---|---|---|
1991 | 10.1007/3-540-54345-7_49 | LECTURE NOTES IN COMPUTER SCIENCE |
Keywords | Field | DocType |
type inference | Discrete mathematics,Combinatory logic,Natural deduction,Computer science,Type inference,Intersection graph,Equivalence (measure theory),Intersection,Realizability | Conference |
Volume | ISSN | Citations |
520 | 0302-9743 | 12 |
PageRank | References | Authors |
1.66 | 2 | 2 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Fabio Alessi | 1 | 83 | 12.04 |
| Franco Barbanera | 2 | 357 | 35.14 |