Higher-order Geometry of Interaction and Program Semantic
| Project/Area Number |
20500010
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Single-year Grants |
|---|
| Section | 一般 |
|---|
| Research Field |
Fundamental theory of informatics
|
|---|
| Research Institution | Kyoto University |
|---|
Principal Investigator |
HASEGAWA Masahito Kyoto University, 数理解析研究所, 教授 (50293973)
|
|---|
| Co-Investigator(Renkei-kenkyūsha) |
KATSUMATA Shin-ya 京都大学, 数理解析研究所, 助教 (30378963)
|
|---|
| Research Collaborator |
NAKATA Keiko タリン工科大学, サイバネティックス研究所, 上級研究員
|
|---|
| Project Period (FY) |
2008 – 2010
|
| Project Status |
Completed (Fiscal Year 2010)
|
| Budget Amount *help |
¥4,550,000 (Direct Cost: ¥3,500,000、Indirect Cost: ¥1,050,000)
Fiscal Year 2010: ¥1,300,000 (Direct Cost: ¥1,000,000、Indirect Cost: ¥300,000)
Fiscal Year 2009: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000)
Fiscal Year 2008: ¥1,820,000 (Direct Cost: ¥1,400,000、Indirect Cost: ¥420,000)
|
|---|
| Keywords | プログラム理論 / プログラム意味論 / 数理論理学 / 圏論 / トポロジー |
|---|
| Research Abstract |
Geometry of Interaction is a mathematical theory of bi-directional interactive computation. Recently, the principal investigator noticed that, by adding higher-order constructs (monoidal closed structure) to Geometry of Interaction, one obtains a rich mathematical structure which can be used for modeling non-linear usage of computational resource. Starting from this observation, this project aimed at providing a theory of Higher-order Geometry of Interaction which combines higher-order computation and cyclic structure in a neat way, together with applications in theory of programming languages. As outcome, we established basic results on traced monoidal closed categories, gave a correction of an error in the structure theorem for traced monoidal categories by Joyal et al., and provided a basic result on the operational semantics of the cyclic call-by-need lambda calculus.
|
Report
(4 results)
Research Products
(28 results)
