Mathematical Structures for Effect Systems

2019 Fiscal Year Final Research Report

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

Free Research Field

プログラミング言語理論

Academic Significance and Societal Importance of the Research Achievements

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