2012 Fiscal Year Final Research Report
Algebraic and coalgebraic proof theories
| Project/Area Number |
21700014
|
|---|
| 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 |
|
|---|
| Project Period (FY) |
2009 – 2012
|
| Keywords | 数理論理学 / 線形論理 / 部分構造論理 / ルディクス / 再帰型 |
|---|
| Research Abstract |
(1) A research program called algebraic proof theory for substructural logics is developed. It is shown that axioms of substructural logics form a hierarchy, and for logics at a lower level, the cut elimination theorem precisely corresponds to the closure under completions in the algebraic sense.
(2) The theory of ludics, a variant of game semantics that originates in linear logic, is reformulated from a computational and coalgebraic point of view. An interactive completeness theorem is proved for a proof system that corresponds to constructive classical propositional logic, and is applied to an interpretation of general recursive types in the sense of the type theory for programming languages
|
