Type checking and typability in domain-free lambda calculi |
| |
| Authors: | Koji Nakazawa Makoto TatsutaYukiyoshi Kameyama Hiroshi Nakano |
| |
| Affiliation: | a Graduate School of Informatics, Kyoto University, Kyoto 606-8501, Japanb National Institute of Informatics, Japanc Department of Computer Science, University of Tsukuba, Japand Department of Applied Mathematics and Informatics, Ryukoku University, Japan |
| |
| Abstract: | This paper shows (1) the undecidability of the type checking and the typability problems in the domain-free lambda calculus with negation, product, and existential types, (2) the undecidability of the typability problem in the domain-free polymorphic lambda calculus, and (3) the undecidability of the type checking and the typability problems in the domain-free lambda calculus with function and existential types. The first and the third results are proved by the second result and CPS translations that reduce those problems in the domain-free polymorphic lambda calculus to those in the domain-free lambda calculi with existential types. The key idea is the conservativity of the domain-free lambda calculi with existential types over the images of the translations. |
| |
| Keywords: | Existential type Type checking Typability Undecidability CPS translation Domain-free type system |
| 本文献已被 ScienceDirect 等数据库收录！ |
|
