Name
Abstract | ||
|---|---|---|
A type theory with infinitary intersection and union types for the lazy 驴-calculus is introduced. Types are viewed as upper closed subsets of a Scott domain. Intersection and union type constructors are interpreted as the set-theoretic intersection and union, respectively, even when they are not finite. The assignment of types to 驴-terms extends naturally the basic type assignment system. We prove soundness and completeness using a generalization of Abramsky's finitary domain logic for applicative transition systems. |
Year | DOI | Venue |
|---|---|---|
2001 | 10.1007/3-540-45500-0_22 | TACS |
Keywords | DocType | ISBN |
union type constructor,union type,lazy lambda calculus,infinite intersection,infinitary intersection,basic type assignment system,type theory,upper closed subsets,applicative transition system,scott domain,union types,finitary domain logic,set-theoretic intersection,lambda calculus | Conference | 3-540-42736-8 |
Citations | PageRank | References |
0 | 0.34 | 12 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Marcello M. Bonsangue | 1 | 824 | 66.34 |
| Joost N. Kok | 2 | 1429 | 121.49 |