>>906
型付きラムダ計算の背後にある数学的理論として、圏論的セマンティクスは古くから知られた基本的な理論である。
実際、両者はある意味等価であり、そのことからいろいろな結果が得られる。
しかし、このときの等価性はラムダ計算における計算規則を等式として見たときのものである。
最近の研究では計算規則を動的、すなわち操作的にとらえたときにも、カテゴリカルセマンティクスとの等価性が成り立っているのではないかと考えられている。
その検証の流れでいろいろ発表されてきているけど一般的なプログラミング言語では無いと思う。