Type Theory of Existential Types
| Project/Area Number |
23500030
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Multi-year Fund |
|---|
| Section | 一般 |
|---|
| Research Field |
Fundamental theory of informatics
|
|---|
| Research Institution | National Institute of Informatics |
|---|
Principal Investigator |
TATSUTA Makoto 国立情報学研究所, 情報学プリンシプル研究系, 教授 (80216994)
|
|---|
| Co-Investigator(Renkei-kenkyūsha) |
NAKAZAWA Koji 京都大学, 情報学研究科, 助教 (80362581)
|
|---|
| Project Period (FY) |
2011-04-28 – 2015-03-31
|
| Project Status |
Completed (Fiscal Year 2014)
|
| Budget Amount *help |
¥4,940,000 (Direct Cost: ¥3,800,000、Indirect Cost: ¥1,140,000)
Fiscal Year 2014: ¥1,170,000 (Direct Cost: ¥900,000、Indirect Cost: ¥270,000)
Fiscal Year 2013: ¥1,170,000 (Direct Cost: ¥900,000、Indirect Cost: ¥270,000)
Fiscal Year 2012: ¥1,170,000 (Direct Cost: ¥900,000、Indirect Cost: ¥270,000)
Fiscal Year 2011: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000)
|
|---|
| Keywords | 型理論 / 存在型 / 国際情報交換 / シンガポール / イタリア |
|---|
| Outline of Final Research Achievements |
(1) Bimorphic recursion is restricted polymorphic recursion such that every recursive call in the body of a function definition has the same type. We showed bimorphic recursion has principal types and decidable type inference. (2) We extended the dual calculus with inductive types and coinductive types. We first introduced a non-deterministic dual calculus with inductive and coinductive types, and proved its strong normalization. Next we introduced a call-by-value system and a call-by-name system of the dual calculus with inductive and coinductive types, and showed their Church-Rosser property, and their strong normalization. (3) This paper proposes games with Sequential Backtracking, and proves that they provide a sound and complete semantics for subclassical logics.
|
Report
(5 results)
Research Products
(5 results)
