Joint work with J.N. Kok

A type theory with infinitary intersection and union types for the lazy lambda calculus is introduced. The meaning of types are subsets of a universe of discourse. 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 lambda-terms extends naturally the basic type assignment system. For this system we prove soundness and completeness theorems by generalizing the connection between Abramsky's finitary domain logic for applicative transition systems and the Scott domain obtained as solution of the equation $X cong (X to X)_bot$.