アルゴリズムの正しさを証明するためのシステムとしてWhyをいうのがある。 こいつはoccaml風のアルゴリズム＋アサーションを入力として、各種定理証明器向けの入力を 出力するという代物です。下はsqrtの例ですが、ここまで書かないと正しさを証明はできない…

http://www.diku.dk/~yokoyama/TetsuoYokoyamaOld.htmlさんの論文Deterministic Higher-order Patterns for Program Transformationというのがあった、どうもパターン（ルール）をつかって言語変換するといいうフレームワークの理論的な論文らしい。 Higher-…