• 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

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

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

Report

(6 results)
  • 2019 Annual Research Report   Final Research Report ( PDF )
  • 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 (9 results) Journal Article (6 results) (of which Int'l Joint Research: 5 results,  Peer Reviewed: 6 results,  Open Access: 1 results,  Acknowledgement Compliant: 3 results) Presentation (3 results) (of which Int'l Joint Research: 2 results) Remarks (2 results)

  • [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

    • ISBN
      9783319893655, 9783319893662
    • 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

      Lecture Notes in Computer Science

      Volume: 9634 Pages: 513-530

    • DOI

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

    • ISBN
      9783662496299, 9783662496305
    • 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: 2022-02-16  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi