A type theory with infinitary intersection and union types for an extension of the λ-calculus is introduced. Types are viewed as upper closed subsets of a Scott domain and 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 logic of domains. Finally we apply the framework to applicative transition systems, obtaining a sound a complete infinitary intersection type assignment system for the lazy λ-calculus. © 2003 Elsevier Science (USA). All rights reserved.
Bonsangue, M. M., & Kok, J. N. (2003). Infinite intersection types. In Information and Computation (Vol. 186, pp. 285–318). Academic Press. https://doi.org/10.1016/S0890-5401(03)00143-3