Sciweavers

Share
CSL
2008
Springer

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

9 years 5 days ago
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.
Koji Nakazawa, Makoto Tatsuta, Yukiyoshi Kameyama,
Added 09 Nov 2010
Updated 09 Nov 2010
Type Conference
Year 2008
Where CSL
Authors Koji Nakazawa, Makoto Tatsuta, Yukiyoshi Kameyama, Hiroshi Nakano
Comments (0)
books