| 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)
|
|---|
| 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.
|
