|
プログラミング言語の実装モデルに焦点を当てたプログラム意味論を研究した．特に，圏論的な意味論の整備を行った．主な結果は以下のとおりである．（１）計算資源の共有・複製を表現する線形冪余モナドを非可換なテンソル圏において定式化した．（２）巡回共有や再帰計算，および相互作用の幾何の実装レベルの意味論に必要なトレース付きテンソル圏の理論を研究し，トレース付きテンソル圏への埋め込み可能性等について，新しい結果を得た．３）トレース付きテンソル圏からコンパクト閉圏への埋め込みに関する新しい定理を示し，それを用いて古典線形論理に対応する線形ラムダ計算から巡回共有構造を持つラムダ計算への翻訳を与えた．
|
