Proof Summit 2012
定理証明支援系(Coq,Agda,Isabelle/HOL,ACL2などなど)や自動証明器などを中心に集まるお祭り Proof Summit 2012 関係のTweetを集めました。
http://partake.in/events/3df37687-ccf7-440c-865c-3ddb1409f5df
- masahiro_sakai
- 5575
- 0
- 2
- 0
ヽ|・∀・|ノ
@i_am_a_youkan
めんどくさくなったので、Google docsでいいやという結論になった。今日のスライド:homotopy type theory for coq programmers https://t.co/uiLglI5I ちなみに贈与税の基本控除は110万円らしい
2012-09-02 19:26:23
ヽ|・∀・|ノ
@i_am_a_youkan
今日口頭で話したbicategoryのcoherenceとか。多分書いてる人あんまりいないので。ついでに、さかいさんに質問された"=="の定義も合わせて https://t.co/j89JVHSs
2012-09-02 21:20:58
ヽ|・∀・|ノ
@i_am_a_youkan
次はdifferential geometry for Coq programmersとかいうネタを RT@oto_oto_oto リベンジHoTT
2012-09-02 22:07:14
Κeіsuke Νakanο
@ksknac
@erutuf13 @masahiro_sakai 私も素因数分解というよりは,Knuth-Bendix みたいなものだと認識しています.その方が一意性の意味が理解しやすいですし.
2012-09-02 22:32:50