• Search Research Projects
  • Search Researchers
  • How to Use
  1. Back to previous page

Mathematical Structures for Effect Systems

Research Project

Project/Area Number 15K00014
Research Category

Grant-in-Aid for Scientific Research (C)

Allocation TypeMulti-year Fund
Section一般
Research Field Theory of informatics
Research InstitutionNational 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)
  • 2019 Annual Research Report
  • 2018 Research-status Report
  • 2017 Research-status Report
  • 2016 Research-status Report
  • 2015 Research-status Report

Research Products

(20 results)

All 2019 2018 2017 2016 Other

All Int'l Joint Research Journal Article Presentation Remarks

  • [Int'l Joint Research] University at Buffalo/University of Wisconsin-Madison/Carnegie Mellon University(米国)

    • Related Report
      2019 Annual Research Report
  • [Int'l Joint Research] IMDEA Software Institute(スペイン)

    • Related Report
      2019 Annual Research Report
  • [Int'l Joint Research] University at Buffalo/Carnegie Mellon University/University of Wisconsin-Madison(米国)

    • Related Report
      2018 Research-status Report
  • [Int'l Joint Research] ニューヨーク州立大学バッファロー校(アメリカ合衆国)

    • Related Report
      2017 Research-status Report
  • [Int'l Joint Research] バッファロー大学/ペンシルバニア大学(アメリカ)

    • Related Report
      2016 Research-status Report
  • [Int'l Joint Research] インペリアル・カレッジ・ロンドン(イギリス)

    • Related Report
      2016 Research-status Report
  • [Int'l Joint Research] タリン工科大学(エストニア)

    • Related Report
      2016 Research-status Report
  • [Int'l Joint Research] 高等師範学校/パリディドロ大学(フランス)

    • Related Report
      2016 Research-status Report
  • [Int'l Joint Research] Universite Paris Denis Diderot(フランス共和国)

    • Related Report
      2015 Research-status Report
  • [Journal Article] Probabilistic Relational Reasoning via Metrics2019

    • 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

    • Related Report
      2019 Annual Research Report
    • Peer Reviewed / Int'l Joint Research
  • [Journal Article] Approximate Span Liftings: Compositional Semantics for Relaxations of Differential Privacy2019

    • 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

    • Related Report
      2019 Annual Research Report
    • Peer Reviewed / Int'l Joint Research
  • [Journal Article] A Double Category Theoretic Analysis of Graded Linear Exponential Comonads2018

    • 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

    • Related Report
      2018 Research-status Report 2017 Research-status Report
    • Peer Reviewed / Open Access
  • [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

      10.1145/3009837.3009890

    • Related Report
      2016 Research-status 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

      10.1145/2951913.2951939

    • Related Report
      2016 Research-status 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

      10.1007/978-3-662-49630-5_30

    • Related Report
      2015 Research-status Report
    • Peer Reviewed / Int'l Joint Research / Acknowledgement Compliant
  • [Presentation] A Double Category Theoretic Analysis of Graded Linear Exponential Comonads2019

    • Author(s)
      勝股 審也
    • Organizer
      理論計算機科学と圏論ワークショップ CSCAT 2019
    • Related Report
      2018 Research-status Report
  • [Presentation] A Double Category Theoretic Analysis of Graded Linear Exponential Comonads2018

    • Author(s)
      勝股 審也
    • Organizer
      Foundations of Software Science and Computation Structures FoSSaCS 2018
    • Related Report
      2018 Research-status Report
    • Int'l Joint Research
  • [Presentation] A Double Category Theoretic Analysis of Graded Linear Exponential Comonads2018

    • Author(s)
      Shin-ya Katsumata
    • Organizer
      Foundations of Software Science and Computation Structures FoSSaCS 2018
    • Related Report
      2017 Research-status Report
    • Int'l Joint Research
  • [Remarks] 勝股 審也のページ

    • URL

      http://group-mmm.org/~s-katsumata/

    • Related Report
      2018 Research-status Report
  • [Remarks] http://group-mmm.org/~s-katsumata/research.html

    • Related Report
      2017 Research-status Report

URL: 

Published: 2015-04-16   Modified: 2021-01-27  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi