zbMATH — the first resource for mathematics

Undecidability of type-checking in domain-free typed lambda-calculi with existence. (English) Zbl 1156.03316
Kaminski, Michael (ed.) et al., Computer science logic. 22nd international workshop, CSL 2008, 17th annual conference of the EACSL, Bertinoro, Italy, September 16–19, 2008. Proceedings. Berlin: Springer (ISBN 978-3-540-87530-7/pbk). Lecture Notes in Computer Science 5213, 478-492 (2008).
Summary: This paper shows undecidability of type-checking and type-inference problems in domain-free typed lambda-calculi with existential types: a negation and conjunction fragment, and an implicational fragment. These are proved by reducing type-checking and type-inference problems of the domain-free polymorphic typed lambda-calculus to those of the lambda-calculi with existential types by continuation passing style translations.
For the entire collection see [Zbl 1148.68004].

03B40 Combinatory logic and lambda calculus
03B25 Decidability of theories and sets of sentences
03B70 Logic in computer science
68N18 Functional programming and lambda calculus
Full Text: DOI