越えられない壁

意味論の勝ち組は明らかに操作的意味論かと。:-) 仮想機械による実行で定義していた頃は「汚い」とか言われましたが、small-stepにせよbig-stepにせよ、ただの帰納的定義で済むことがわかってしまったので。（参考：Types and Programming Languagesの3.4節や萩谷先生の「個人的な思い」など）

さらにCCSとかπ計算とか並行言語の表示的意味論がややこしすぎてトドメに。関数型言語ですらCPOやらCCCやらややこしいのに。公理的意味論は仕様検証などでやや復活気味ですが、高階関数を導入すると結局はLFやCCのような型理論になってしまうので。

というわけでTAPLだけ読めば、とりあえず事足ります。と身内の著書を宣伝。