研究課題
若手研究(B)
表示的意味論ではプログラムの多様な振る舞いを統一的に扱うためにモナドがしばしば用いられる。そのような表示的意味論の持つ性質を調べる数学的道具として、研究代表者は以前、意味論的TT-liftingを導入した。本研究ではこれを応用し、1. エフェクトシステムの表示的意味論におけるエフェクト健全性の一般的な証明と、2. モナド上の前順序の構成と特徴づけを与えた。また、TT-liftingをより一般的な圏論的状況で用いることができるよう拡張した。
プログラミング言語の意味論
