Undecidability of type-checking in domain-free typed lambda-calculi with existence. (English) Zbl 1156.03316

Nakazawa, Koji; Tatsuta, Makoto; Kameyama, Yukiyoshi; Nakano, Hiroshi

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].

MSC:

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

Keywords:

undecidability; existential type; CPS-translation; domain-free type system