計算効果を持つ言語機構とソフトウェア契約の統合について，FindlerとFelleisenの契約計算やBlame計算の限定継続機構による拡張を行い，動的契約検査のアルゴリズムの形式化やBlame計算としての諸性質の証明を与えた．また，顕在的契約計算の代入機構による拡張を形式化し，その諸性質を示した．代数的データ型による顕在的契約計算を提案し，その上で，代数的データ型に対する契約記述のふたつの方法について比較し，一方から他方へは変換が可能であること示した．また，この計算体系の実装として OCaml 処理系の拡張を行った．ソフトウェア契約の代数的意味論としてトレース意味論を研究した．