Proof Summit 2011
-
yoshihiro503
- 3998
- 0
- 0
- 0
-
- いいね！0
中村 良幸 (Nakamura Yoshiyuki)
@nakayoshix
CoqIdeですが、デフォルトの状態だと44歳の眼には辛いので、フォントサイズを14ptにしてだいぶ見やすくなりました。 #ProofSummit
2011-09-25 10:41:01
kenichi kobayashi
@kencoba
#proofsummit Now on Ustream! http://t.co/J4WZ8FnF&utm_source=9389178&utm_medium=social
2011-09-25 10:48:43
kenichi kobayashi
@kencoba
#proofsummit CoqでHaskellにextractしたいときは、末尾再帰にこだわらなくてよいかも、とのこと。
2011-09-25 10:54:20
mzp
@mzp
#proofsummit 研究室でCoqが流行ったときは「Haskellだったら停止しない関数も定義できるぜ」「まじで。すげぇ柔軟じゃん」という会話が冗談半分でかわされたものです。
2011-09-25 10:55:04
でこれき
@dico_leque
#proofsummit 末尾再帰版の方が証明が面倒なことが多いので、素直な再帰版についての証明書いて、それから末尾再帰版と素直な再帰のが等価なことを証明した方が楽 云々 #proofsummit
2011-09-25 10:55:40
Keigo Imai
@keigoi
#ProofSummit 今日の私の話は「スタートSEPLOG + COQ 2」です。内容はほぼ 以前 名古屋で話した内容→ http://t.co/XBqFoiRV になると思いますが、ICFPで聞いた話も一部入れられるかも
2011-09-25 10:57:42
でこれき
@dico_leque
cond {A : Set} (c : bool) (vt vf: A) の場合、 vt, vf から A は推論される。 { ... } で指定した引き数は暗黙に渡される。陽に渡したい場合は @ cond nat ... みたいに関数名の前に@をつける #proofsummit
2011-09-25 11:06:49
[1..100]＞＞=pen
@1to100pen
cabal install Agda-executable すると「不明な ID です: cabal」と言われるです。 #proofsummit
2011-09-25 11:08:25
mzp
@mzp
【再ポスト】#proofsummit docs.google.com/spreadsheet/cc… みんながつぶやいている席の位置をgoogle docsでまとめました。適当に追記してください
2011-09-25 11:12:53
[1..100]＞＞=pen
@1to100pen
ははは、 sudo cabal ... のつもりを su cabal ... と打ってたよ。あははは・・・・・・ orz。 #proofsummit
2011-09-25 11:14:42
rkyymmt
@rkyymmt
Coqについては個人的には確か３回目のチュートリアル受講だけど、かなり間が開いているので毎回すっかり忘れている #proofsummit
2011-09-25 11:17:30
Keigo Imai
@keigoi
{x:nat|x+n=m} は nat型で、さらに「nを足すとmになる」何かを表す型。依存型を使ってそういうことまで書けてしまうのが Coqのスゴいところ #ProofSummit
2011-09-25 11:22:28
ogawa kiyoshi
@kaizen_nagoya
実演開始: Agda 入門＠ProofSummit 2011 http://t.co/A1xdsvct #proofsummit
2011-09-25 11:27:50
νStream（ニューストリーム）
@v_stream
09/25 11:30 [kencoba] proofsummit／定理証明支援系(Coq,Agda,Isabelle/HOL,ACL2などなど)を中心に集まるお祭り http://t.co/rvMUBUlf
2011-09-25 11:31:05