Name
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. |
Year | DOI | Venue |
|---|---|---|
2011 | 10.1016/j.tcs.2011.06.020 | Theor. Comput. Sci. |
Keywords | DocType | Volume |
typability problem,paper shows,type checking,domain-free lambda calculus,Type checking,key idea,CPS translation,domain-free polymorphic lambda calculus,Typability,existential type,Undecidability,Domain-free type system,Existential type | Journal | 412 |
Issue | ISSN | Citations |
44 | Theoretical Computer Science | 0 |
PageRank | References | Authors |
0.34 | 13 | 4 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Koji Nakazawa | 1 | 36 | 6.92 |
| Makoto Tatsuta | 2 | 111 | 22.36 |
| Yukiyoshi Kameyama | 3 | 171 | 17.29 |
| Hiroshi Nakano | 4 | 20 | 2.25 |