テスト駆動開発から証明駆動開発へ #JTF2019 / July Tech Festa 2019July Tech Festa 2019 で使用したスライドです。 近年、テストを書く文化は広く普及しており、開発フローにおいて自動テストを組み込むことはもはや常識となりました。しかしよく考えてみると、有限個のテストケースが保証しているのは、所詮「特定の有限個の入力に対する出力」にしか過ぎません。…
Coqと少しの圏論が分かる人向けのhomotopy type theory(その1) -
The HoTT Book http://homotopytypetheory.org/book/ が完成したらしいけど、どっちかというと、数学者向けに書かれてて500ページもある。homotopy type theoryで今できてることって、CoqやAgdaで書いたら、せいぜい数千行とか、そんなもんじゃないかと思うので、長すぎる気がする 一応、HoTTに関わる知識は、型理論の他に、ホモトピー論や圏論(モナドとかHaskell関連で出てくる類の知識はあまり知らなくてもいいけど、higher categoryとか教科書に書いてなさそうな話題や、モデル圏とかを知ってるといい)があって、全部真面目に勉強しようと思うと、それぞれのテーマで一冊以上の本が書ける。ただ、実際には、ホモトピー論や圏論はアイデアや視点を提供しているだけで、あくまでCoqやAgdaで書かれてる部分が重要なので、ホモトピー論や
Feit-Thompson true —
Feit-Thompson true Feit-Thompson theorem has been totally checked in Coq Thursday 20 September 2012, 18:16. We received following mail from Georges Gonthier (see below). It concludes the proof in Coq of the Feit-Thompson theorem. This theorem, also named the Odd Order Theorem, is the first main result in the classification of finite groups. This work was achieved by the team formed by addressees o
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
処理を実行中です
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
http://blog.ezyang.com/2012/09/feit-thompson-true/
