Partial types and intervals. (English) Zbl 0697.03005

Summary: The main idea of this paper is to develop an inference system to assign partial types to terms of the untyped lambda calculus. A term can either be necessarily or possibly of a certain type; these notions of necessity and possibility are incorporated into the type inference system as modalities. A subclass of types are the total types, for which necessity and possibility are equivalent. In the semantics the meaning of a total type is a set of values in the domain, the meaning of a type being, in general, an interval (a set of sets of values). This is a generalization of R. Cartwright’s semantics [Conf. Rec. 12th Ann. ACM Symp. Princ. Programm. Lang., Assoc. Comput. Mach., New York, 22-36 (1984)]. The main results are the soundness and completeness of the type inference system with respect to interval semantics.


03B40 Combinatory logic and lambda calculus
68Q55 Semantics in the theory of computing
03B45 Modal logic (including the logic of norms)
68P05 Data structures
Full Text: DOI