ジラール（Girard）のthe big picture

Esfandiar Haghverdiのプレゼンより：ジラールのGoIは次のようなアナロジーに基づくようだ。

証明的	ジラール曰く	手続き的	関数的
証明	アルゴリズム(algorithm)	プログラム	式
cut消去	計算(computation)	実行	評価／簡約
cutなし証明	データ(datum)	結果	値

大規模なカリー／ワハード対応みたいなもんか？

cut消去と計算の部分はトレースによって与えられる、ここが面白い。ただし、トレースは部分トレース（partial trace）。