zbMATH — the first resource for mathematics

Type checking and inference are equivalent in lambda calculi with existential types. (English) Zbl 1274.03027
Escobar, Santiago (ed.), Functional and constraint logic programming. 18th international workshop, WFLP 2009, Brasilia, Brazil, June 28, 2009. Revised selected papers. Berlin: Springer (ISBN 978-3-642-11998-9/pbk). Lecture Notes in Computer Science 5979, 96-110 (2010).
Summary: 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 type-inference 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.
For the entire collection see [Zbl 1185.68006].
03B40 Combinatory logic and lambda calculus
68N18 Functional programming and lambda calculus
Full Text: DOI