http://as305.dyndns.org/wiki/index.php?Coq

http://d.hatena.ne.jp/ku-ma-me/20070529/で「G」はなくてもPefungeで記述できるので無駄ではないかとまめにいったら、 スタックの先頭しか入れ替えられないので、無理ではないかというので、 とりあえず画期的な方法で実装してみる。 "Hello, world!" v ge…

なんかいろんな言語で FizzBuzz が書かれているようなので、Coq でも書いてみる。Coq の FizzBuzz は他のとは一味違う！なんとプログラムが正しく動くことが証明できるのだ！とりあえず、書いたプログラム Require Import Arith. Require Import List. (* Fi…

方程式の解のことを根と呼ぶ人々がいる。 昔はそう習ったんだから、そのように呼ぶ人が残っていることはしかたのないことだ。微分方程式の解のことを根と呼ぶ人はいない。何か不思議な語感があって、これは根とは呼ばないっぽい。 方程式の解のうちで根と呼…

VC++が定数による除算を乗算に変換する最適化をしてるのは、吐いたコードを見たことある人なら知ってることだと思うけど、なんとなくhttp://www.wikihouse.com/x86clocker/index.php?plugin=attach&refer=%B2%E1%B5%EE%A5%ED%A5%B0&openfile=x86%CC%BF%CE%E1…