2010 Fiscal Year Final Research Report
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
|
| 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.
|
