Mathematical Structures for Effect Systems
Project/Area Number |
15K00014
|
Research Category |
Grant-in-Aid for Scientific Research (C)
|
Allocation Type | Multi-year Fund |
Section | 一般 |
Research Field |
Theory of informatics
|
Research Institution | National Institute of Informatics (2017-2019) Kyoto University (2015-2016) |
Principal Investigator |
勝股 審也 国立情報学研究所, アーキテクチャ科学研究系, 特任研究員 (30378963)
|
Project Period (FY) |
2015-04-01 – 2020-03-31
|
Project Status |
Completed (Fiscal Year 2019)
|
Budget Amount *help |
¥4,680,000 (Direct Cost: ¥3,600,000、Indirect Cost: ¥1,080,000)
Fiscal Year 2018: ¥1,170,000 (Direct Cost: ¥900,000、Indirect Cost: ¥270,000)
Fiscal Year 2017: ¥1,170,000 (Direct Cost: ¥900,000、Indirect Cost: ¥270,000)
Fiscal Year 2016: ¥1,170,000 (Direct Cost: ¥900,000、Indirect Cost: ¥270,000)
Fiscal Year 2015: ¥1,170,000 (Direct Cost: ¥900,000、Indirect Cost: ¥270,000)
|
Keywords | 次数付きモナド / エフェクトシステム / 差分プライバシー / ホーア論理 / 次数付きコモナド / 計算効果 / プログラミング言語の意味論 / 線形論理 |
Outline of Annual Research Achievements |
1. アルゴリズムの差分プライバシーの型理論的検証に関する研究をまとめた論文が、理論計算機科学のトップ国際会議であるLICS2019にて採択された。 2. 計算効果に関する距離の概念と、そのような距離から次数付きモナドを構成する方法について研究を行った。BartheらはPOPL2012で差分プライバシーの検証のためのホーア論理apRHLを導入した。その意味論は、確率分布間の距離の概念から構成される次数付きモナドにより与えられる。このシナリオを一般化し、モナドTによって記述される計算効果の間の距離の概念を導入し、それらを余稠密持ち上げにより次数付きモナドに拡張する方法を与えた。そして計算効果の距離を測ることのできるホーア論理と、その健全な意味論を与えた。 3. 与えられたシグネチャから次数付きモナドを生成する方法を研究した。モナドと代数理論の間の数学的な対応関係は1960年代頃に確立されている。これを次数付きモナドについて拡張することで、体系的に次数付きモナドを得ることが可能となると考察した。本研究では、研究代表者がPOPL2014で導入した代数的演算の概念をもとに、次数付きモナドを生成する方法を考察した。 4. ホーア論理をエフェクトシステムで拡張した論理に対する意味論を次数付き圏により与える方法を研究した。次数付き圏は次数付きモナドおよびコモナドのKleisli圏として自然に得られる、一般的な圏のクラスである。拡張されたホーア論理が自然に解釈できるよう、計算効果のモデルとして用いられるFreyd圏を次数付き圏に拡張する研究も行った。
|
Report
(5 results)
Research Products
(20 results)
-
-
-
-
-
-
-
-
-
-
-
-
-
[Journal Article] A semantic account of metric preservation2017
Author(s)
Arthur Azevedo de Amorim, Marco Gaboardi, Justin Hsu, Shin-ya Katsumata, Ikram Cherigui
-
Journal Title
Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017
Volume: -
Pages: 545-556
DOI
Related Report
Peer Reviewed / Int'l Joint Research / Acknowledgement Compliant
-
[Journal Article] Combining effects and coeffects via grading2016
Author(s)
Marco Gaboardi, Shin-ya Katsumata, Dominic A. Orchard, Flavien Breuvart, Tarmo Uustalu
-
Journal Title
Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016
Volume: -
Pages: 476-489
DOI
Related Report
Peer Reviewed / Int'l Joint Research / Acknowledgement Compliant
-
[Journal Article] Towards a Formal Theory of Graded Monads2016
Author(s)
Soichiro Fujii, Shin-ya Katsumata, and Paul-Andre Mellies
-
Journal Title
Foundations of Software Science and Computation Structures (FoSSaCS 2016)
Volume: 9634
Pages: 513-530
DOI
Related Report
Peer Reviewed / Int'l Joint Research / Acknowledgement Compliant
-
-
-
-
-