2006-10-03から1日間の記事一覧

CPSとSSA

http://citeseer.ist.psu.edu/kelsey95correspondence.html を眺めた。CPSはいいもので、80年代の関数型言語のコンパイラの中間表現としてよく使われたらしい。特に、継続も扱えるあたりがいい。一方のSSA(Static Single Assignment)というのは、変数への値…

Coq。証明中、Undo機能が欲しいなーと思ってたら、ちゃんとあった。前回の補足のような。Variableで大域変数を宣言したけど、 Coq < forall A B C:Prop , (A->B->C)->(A->B)->(A->C).みたく、forallでローカルに束縛しちゃっていいらしい。Propが型というの…

有名な数学の定理100個を様々な証明支援系で形式化している http://www.cs.ru.nl/~freek/100/ ProofPowerというのは初耳だけど、Coq , Isabelle , Mizarあたりは、どれも30個程度しか形式化できていないのに対して、HOL Lightだけが60個以上と飛びぬけている…