[Coq] Coq Tutorial on 1/12, 2/2, 2/9, and 2/16

イベントレポート：「Coqチュートリアル#1」 @ InfoQ

今回、豆蔵様より会場を提供していただけることになって、前々から計画していた平日夜の複数回開催のCoqチュートリアルを 1/12, 2/2, 2/9, 2/16 という予定で開催します。
参加申し込みについては上記リンクから辿って頂ければと思います。

[Coq] itoa in Coq

https://github.com/tmiya/coq/blob/master/Radix/Radix.v

自然数$n$を$p \ge 2$で割って余りを求め、商をまた割って、と繰り返すことで$n$の$p$進表示を得られますが、そのencode/decodeをCoqで書きました。勿論、encodeとdecodeが逆関数になっていることも証明済みです。
encode関数を使って、C言語にあるitoa関数を書きました。これがあれば、数字を文字列に変換出来ますからFizzBuzzもCoqで書けます。
そのうちCoq user contributionに登録しよう。