Calculi with Second-Order Existential Quantifier
| Project/Area Number |
21700013
|
|---|
| Research Category |
Grant-in-Aid for Young Scientists (B)
|
| Allocation Type | Single-year Grants |
|---|
| Research Field |
Fundamental theory of informatics
|
|---|
| Research Institution | Kyoto University |
|---|
Principal Investigator |
NAKAZAWA Koji 京都大学, 大学院・情報学研究科, 助教 (80362581)
|
|---|
| Project Period (FY) |
2009 – 2011
|
| Project Status |
Completed (Fiscal Year 2011)
|
| Budget Amount *help |
¥2,990,000 (Direct Cost: ¥2,300,000、Indirect Cost: ¥690,000)
Fiscal Year 2011: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000)
Fiscal Year 2010: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000)
Fiscal Year 2009: ¥1,170,000 (Direct Cost: ¥900,000、Indirect Cost: ¥270,000)
|
|---|
| Keywords | 型理論 / ラムダ計算 / 存在型 / 型検査 / 決定可能性 / 多相型 / 型検査問題 / 型推論問題 / 型付け可能性問題 / 決定不可能性 / ドメインフリー |
|---|
| Research Abstract |
We have got the following results on some type-related decision problems of calculi with second-order existential types :(1) for some typed lambda calculi where programs contain only partial type information, we have proved that type-checking and typability problems on polymorphic types are Turing reducible to those on existential types, and we have shown that those problems on existential types are undecidable,(2) we have proved the Turing equivalence between type-checking and typability problems in some fragments with existential type, and we have got new proofs of undecidability of typability in the domain-free lambda calculi with existential types, and(3) we have proved the Turing equivalence between the type-related problems in domain-free calculi with existential types and those in domain-free calculi with polymorphic types.
|
Report
(4 results)
Research Products
(8 results)
