Name
Abstract | ||
|---|---|---|
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. |
Year | DOI | Venue |
|---|---|---|
2008 | 10.1007/978-3-540-87531-4_34 | CSL |
Keywords | Field | DocType |
type-inference problem,style translation,implicational fragment,domain-free typed lambda-calculi,domain-free polymorphic,existential type,conjunction fragment,typed lambda calculus,type system,continuation passing style,type inference,polymorphism | Discrete mathematics,Simply typed lambda calculus,Typed lambda calculus,System F,Type inference,Type inhabitation,Pure type system,Dependent type,Type constructor,Mathematics | Conference |
Volume | ISSN | Citations |
5213 | 0302-9743 | 10 |
PageRank | References | Authors |
0.61 | 12 | 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 |