×

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.

MSC:

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