エフェクトシステムの表示的意味論にまつわる数学的構造

2019 年度 研究成果報告書

• 研究課題/領域番号: 15K00014
• 研究種目: 基盤研究(C)
• 配分区分: 基金
• 応募区分: 一般
• 研究分野: 情報学基礎理論
• 研究機関: 国立情報学研究所 (2017-2019); 京都大学 (2015-2016)
• 研究代表者: 勝股 審也 国立情報学研究所, アーキテクチャ科学研究系, 特任研究員 (30378963)
• 研究期間 (年度): 2015-04-01 – 2020-03-31
• キーワード: 次数付きモナド / 表示的意味論 / エフェクトシステム / 型理論

研究成果の概要

LucassenとGiffordらはプログラムの挙動の静的な分析を型理論的に行う手法としてエフェクトシステムを導入した。本研究は次数付きモナドによるエフェクトシステムの表示的意味論をもとに、エフェクトシステムにまつわる様々な数学的構造とその応用について研究を行った。その結果、1)次数付きモナドの圏論的性質(特に随伴への分解)、2) 次数付きモナドと次数付きコモナドの分配束、3) 線形べきコモナドの二重圏による定義、4) モナドの次数付き!-持ち上げの導入と差分プライバシーの検証への応用といった研究成果を得た。

自由記述の分野

プログラミング言語理論

研究成果の学術的意義や社会的意義

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