2014 Fiscal Year Final Research Report
Reasoning about computational effects by TT-lifting
| Project/Area Number |
24700012
|
|---|
| Research Category |
Grant-in-Aid for Young Scientists (B)
|
| Allocation Type | Multi-year Fund |
|---|
| Research Field |
Fundamental theory of informatics
|
|---|
| Research Institution | Kyoto University |
|---|
Principal Investigator |
|
|---|
| Research Collaborator |
SATO Tetsuya
|
|---|
| Project Period (FY) |
2012-04-01 – 2015-03-31
|
| Keywords | モナド / 論理関係 / 表示的意味論 / エフェクトシステム / ファイブレーション / 余代数 |
|---|
| Outline of Final Research Achievements |
In the denotational semantics of programming languages, monads are a widely used mathematical structure to give a unified model of various kinds of side-effects. Previously, Katsumata introduced the semantic TT-lifting as a mathematical tool to study the properties of monadic semantics of programming languages. In this research, we apply the semantic TT-lifting 1) to show a generic effect soundness in the denotational semantics of general effect systems, and 2) to give a construction and a characterisation of preorders on monads. We also extend the semantic TT-lifting so that it works with wider categorical situations.
|
| Free Research Field |
プログラミング言語の意味論
|
