Name
Abstract | ||
|---|---|---|
Type assignment systems with intersection and union types are introduced. Although the subject reduction property with respect to β-reduction does not hold for a natural deduction-like system, we manage to overcome this problem in two, different ways. The first is to adopt a notion of parallel reduction, which is a refinement of Gross-Knuth reduction. The second is to introduce type theories to refine the system, among which is the theory called Π that induces an assignment system preserving β-reduction. This type assignment system further clarifies the relation with the intersection discipline through the decomposition, first, of a disjunctive type into a set of conjunctive types and, second, of a derivation in the new type assignment system into a set of derivations in the intersection type assignment system. For this system we propose three semantics and prove soundness and completeness theorems. |
Year | DOI | Venue |
|---|---|---|
1995 | 10.1006/inco.1995.1086 | Inf. Comput. |
Keywords | DocType | Volume |
union type,type theory,natural deduction,weed management | Journal | 119 |
Issue | ISSN | Citations |
2 | Information and Computation | 61 |
PageRank | References | Authors |
3.56 | 1 | 3 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Franco Barbanera | 1 | 357 | 35.14 |
| Mariangiola Dezani-Ciancaglini | 2 | 1615 | 193.57 |
| Ugo de'Liguoro | 3 | 251 | 23.50 |