Title :
λ-calculi with decidable ∩-type checking
Author_Institution :
Dept. of Comput. Sci., North Dakota Univ., Grand Forks, ND, USA
Abstract :
The typed lambda calculus is extended to accommodate the type intersection operator ∩ of Coppo (1980). The extensions, L2 and L3, capture the expressive power of the intersection operator with respect to typeable closed lambda expressions, but do not sacrifice decidability of type checking. Type checking algorithms for L2 and L3 are given. It is shown that, although decidable, type checking in the extensions is NP-hard
Keywords :
decidability; lambda calculus; type theory; decidable ∩-type checking; expressive power; lambda-calculi; type intersection operator; typed lambda calculus; Calculus; Constraint theory; Inference algorithms; Reactive power; TV;
Conference_Titel :
Computing and Information, 1993. Proceedings ICCI '93., Fifth International Conference on
Conference_Location :
Sudbury, Ont.
Print_ISBN :
0-8186-4212-2
DOI :
10.1109/ICCI.1993.315410
