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: Katsumata Shin-ya 国立情報学研究所, アーキテクチャ科学研究系, 特任研究員 (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 Final Research Achievements

Lucassen and Gifford introduced a type-theoretic approach, called effect system, to statically estimate computational effects of programs. Based on the categorical semantics of effect systems using graded monads, this research pursues various mathematical structures around effect systems. The obtained results are: 1) formal categorical properties of graded monads (especially the decomposition of graded monads into adjunctions) 2) introducing a distributive law between graded monads and graded linear exponential comonads 3) a double-category theoretic analysis of the linear exponential comonad, 4) introduing graded !-lifting of monads, with application to the differential privacy.

Academic Significance and Societal Importance of the Research Achievements

エフェクトシステムはプログラムの安全性や効率を高めるためのプログラム解析技術として様々な形で用いられてきた。本研究はエフェクトシステムの背後にある様々な数学的構造の理解を追求し、エフェクトシステムが実用上の技法というだけでなく、理論的な広がりを持つことを示した。また、本研究で得られた理論的な知見はプログラム解析やホーア論理などのプログラム論理の正しさに応用され、安全なソフトウェアの開発に貢献するものである。

Research Products

• [Int'l Joint Research] University at Buffalo/University of Wisconsin-Madison/Carnegie Mellon University(米国)
  • Country Name: U.S.A.
  • Counterpart Institution: University at Buffalo/University of Wisconsin-Madison/Carnegie Mellon University
• [Int'l Joint Research] IMDEA Software Institute(スペイン)
  • Country Name: SPAIN
  • Counterpart Institution: IMDEA Software Institute
• [Int'l Joint Research] University at Buffalo/Carnegie Mellon University/University of Wisconsin-Madison(米国)
  • Country Name: U.S.A.
  • Counterpart Institution: University at Buffalo/Carnegie Mellon University/University of Wisconsin-Madison
• [Int'l Joint Research] ニューヨーク州立大学バッファロー校(米国)
  • Country Name: U.S.A.
  • Counterpart Institution: ニューヨーク州立大学バッファロー校
• [Int'l Joint Research] バッファロー大学/ペンシルバニア大学(米国)
  • Country Name: U.S.A.
  • Counterpart Institution: バッファロー大学/ペンシルバニア大学
• [Int'l Joint Research] インペリアル・カレッジ・ロンドン(英国)
  • Country Name: UNITED KINGDOM
  • Counterpart Institution: インペリアル・カレッジ・ロンドン
• [Int'l Joint Research] タリン工科大学(エストニア)
  • Country Name: ESTONIA
  • Counterpart Institution: タリン工科大学
• [Int'l Joint Research] 高等師範学校/パリディドロ大学(フランス)
  • Country Name: FRANCE
  • Counterpart Institution: 高等師範学校/パリディドロ大学
• [Int'l Joint Research] Universite Paris Denis Diderot(フランス)
  • Country Name: FRANCE
  • Counterpart Institution: 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: https://doi.org/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: Lecture Notes in Computer Science 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