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: ¥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圏を次数付き圏に拡張する研究も行った。

Research Products

• [Int'l Joint Research] University at Buffalo/University of Wisconsin-Madison/Carnegie Mellon University(米国)
• [Int'l Joint Research] IMDEA Software Institute(スペイン)
• [Int'l Joint Research] University at Buffalo/Carnegie Mellon University/University of Wisconsin-Madison(米国)
• [Int'l Joint Research] ニューヨーク州立大学バッファロー校(アメリカ合衆国)
• [Int'l Joint Research] バッファロー大学/ペンシルバニア大学(アメリカ)
• [Int'l Joint Research] インペリアル・カレッジ・ロンドン(イギリス)
• [Int'l Joint Research] タリン工科大学(エストニア)
• [Int'l Joint Research] 高等師範学校/パリディドロ大学(フランス)
• [Int'l Joint Research] Universite Paris Denis Diderot(フランス共和国)
• [Journal Article] Probabilistic Relational Reasoning via Metrics (2019)
  • Author(s): de Amorim Arthur Azevedo、Gaboardi Marco、Hsu Justin、Katsumata Shin-ya
  • Journal Title: Proc. 2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) Volume: - Pages: 1-19
  • DOI: 10.1109/lics.2019.8785715
  • Peer Reviewed / Int'l Joint Research
• [Journal Article] Approximate Span Liftings: Compositional Semantics for Relaxations of Differential Privacy (2019)
  • Author(s): Sato Tetsuya、Barthe Gilles、Gaboardi Marco、Hsu Justin、Katsumata Shin-ya
  • Journal Title: Proc. 2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) Volume: - Pages: 1-14
  • DOI: 10.1109/lics.2019.8785668
  • Peer Reviewed / Int'l Joint Research
• [Journal Article] A Double Category Theoretic Analysis of Graded Linear Exponential Comonads (2018)
  • Author(s): Katsumata Shin-ya
  • Journal Title: Proc. Foundations of Software Science and Computation Structures FoSSaCS 2018, Lecture Notes in Computer Science Volume: 10803 Pages: 110-127
  • DOI: 10.1007/978-3-319-89366-2_6
  • Peer Reviewed / Open Access
• [Journal Article] A semantic account of metric preservation (2017)
  • 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: 10.1145/3009837.3009890
  • Peer Reviewed / Int'l Joint Research / Acknowledgement Compliant
• [Journal Article] Combining effects and coeffects via grading (2016)
  • 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: 10.1145/2951913.2951939
  • Peer Reviewed / Int'l Joint Research / Acknowledgement Compliant
• [Journal Article] Towards a Formal Theory of Graded Monads (2016)
  • 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: 10.1007/978-3-662-49630-5_30
  • Peer Reviewed / Int'l Joint Research / Acknowledgement Compliant
• [Presentation] A Double Category Theoretic Analysis of Graded Linear Exponential Comonads (2019)
  • Author(s): 勝股 審也
  • Organizer: 理論計算機科学と圏論ワークショップ CSCAT 2019
• [Presentation] A Double Category Theoretic Analysis of Graded Linear Exponential Comonads (2018)
  • Author(s): 勝股 審也
  • Organizer: Foundations of Software Science and Computation Structures FoSSaCS 2018
  • Int'l Joint Research
• [Presentation] A Double Category Theoretic Analysis of Graded Linear Exponential Comonads (2018)
  • Author(s): Shin-ya Katsumata
  • Organizer: Foundations of Software Science and Computation Structures FoSSaCS 2018
  • Int'l Joint Research
• [Remarks] 勝股 審也のページ
  • URL: http://group-mmm.org/~s-katsumata/
• [Remarks] http://group-mmm.org/~s-katsumata/research.html