今日はProofCafeでCPDTの三章を読み進めたが、そこでCoqではInductive型のコンストラクタの引数が関数のとき、その関数の左側に自分自身が現れてはいけないということを学んだ。もしそれを可能にしてしまうと無限ループが定義でき、公理系が矛盾してしまうか…

TDD Boot Camp名古屋に参加しました。id:t-wadaさんの講演はすばらしく、TDDをずっと推し進めている経験に基づく具体的な知見は大変わかりやすく勉強になりました。 当日のスライドはid:t-wadaさんのブログで見ることができます。TDD Boot Camp 名古屋に登壇…

7/12に名古屋市工業技術研究所で行われた id:kencobaさんによる Alloyセミナーに、講師補佐としてお手伝いさせてもらいました。当日の資料はこちらから辿れます。Alloy Analyzer入門セミナー - kencobaの日記TDDBC名古屋で2日間テスト駆動開発を行った直後で…

http://d.hatena.ne.jp/kikx/20100629#1277831079 の素晴らしい足し算の存在証明を見つけたので、その存在が一意(ユニーク)であることを証明した。元々のネタはこちら http://d.hatena.ne.jp/m-hiyama/20100629/1277774676まずは集合AとA上の掛け算とサクセ…