Sciweavers

Share
WFLP
2009
Springer

Type Checking and Inference Are Equivalent in Lambda Calculi with Existential Types

9 years 6 months ago
Type Checking and Inference Are Equivalent in Lambda Calculi with Existential Types
This paper shows that type-checking and type-inference problems are equivalent in domain-free lambda calculi with existential types, that is, type-checking problem is Turing reducible to typeinference problem and vice versa. In this paper, the equivalence is proved for two variants of domain-free lambda calculi with existential types: one is an implication and existence fragment, and the other is a negation, conjunction and existence fragment. This result gives another proof of undecidability of type inference in the domain-free calculi with existence. Keywords. undecidability, existential type, type checking, type inference, domain-free type system.
Yuki Kato, Koji Nakazawa
Added 25 May 2010
Updated 25 May 2010
Type Conference
Year 2009
Where WFLP
Authors Yuki Kato, Koji Nakazawa
Comments (0)
books