,j;;;;;j,. ---一､ ｀ ―--‐､_ l;;;;;; ｛;;;;;;ゝ T辷iﾌ i f'辷jァ !i;;;;; Haskell使ったら負けかな ヾ;;;ﾊ ﾉ .::!lﾘ;;rﾞ `Z;i 〈.,_..,. ﾉ;;;;;;;;> そんなふうに考えていた時期が ,;ぇﾊ、 ､_,.ｰ-､_',. ,ｆﾞ: Y;;f 俺にもありました ~''戈ヽ ｀二´ r'´:::.…

Action Semanticsはちらっと見た感じで、センスなさげだったので放置。Modular SOSも斬新な感じはしないので、放置。抽象機械で意味論与えるのは、なんか違うよなーって感じなので、放置。というわけで、Monadic Semanticsが残ったとりあえず、ここらへんが…

A正規形(ANF)の最初の論文らしい。 http://citeseer.ist.psu.edu/flanagan-essence.html を読んでみた。1/3くらいしか理解できん。CPS変換して、"administrative lambda"をベータ簡約して、逆CPS変換したものが、ANFということらしい。勿論、実際のA正規化は…

普通にプログラムするより、Coqで証明書くほうが大変だから、実用的でないというのは外した意見だった。つまり、大変だけど、「正しい」コードが得られるということが重要。生成されたコードがバカすぎるというのは、その通りだけど、そのへんは大富豪的プロ…