Undecidability of Type-Checking in Domain-Free Typed Lambda-Calculi with Existence

Abstract. This paper shows undecidability of type-checking and typeinference 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.

• Type: Conference
• Year: 2008
• Where: CSL
• Authors: Koji Nakazawa, Makoto Tatsuta, Yukiyoshi Kameyama, Hiroshi Nakano
• Keywords: Automated Reasoning, CSL 2008, Existential Types, Polymorphic Typed Lambda-calculus, Type-checking