〜 絶対にバグのないプログラムの書き方 〜

はじめまして。今回、Coq のチュートリアルを執筆させていただくことになった池渕未来(いけぶちみらい)です。IIJ-II のアルバイトとして、山本和彦先生のもとで、この連載を書きます。

私はこの春から女子大生になります。Coq のエライ人でもスゴイ人でもありません。そうであるからこそ、読者の皆さんと同じ視線に立って一緒に楽しく Coq を学んでいけるのではないかな? と思います。

これからの連載、よろしくお願いします!

1. Coq を始めよう (公開 2011/04/05)
2. Proof-editing mode であそぼう (公開 2011/04/19)
3. リストを扱う (公開 2011/05/10)
4. 自然数を扱う (公開 2011/05/24)
5. 使えるタクティク集 (公開 2011/08/23)
6. 証明ができない! こんなとき (公開 2011/09/06)
7. 停止性が明らかでない関数を定義するには (公開 2011/09/20)
8. 証明駆動開発入門(1) (公開 2011/10/06)
9. 証明駆動開発入門(2) (公開 2011/10/25) (最終回)

@m_ike_neko というアカウントで Twitter やってます。感想やコメントは、twitter で #coqt というハッシュタグとともに、つぶやいていただくようお願いします。