#proofsummit2012 の公開済み資料をまとめてみました。
PARTAKEのページのプログラムからリンクを貼れないでしょうか >  +Miyamoto Takashi 

時刻 内容
10:00-10:10 挨拶、連絡事項など

10:15-10:45 @yoshihiro503さん：「型推論のない静的型付け言語へのCoq ExtractionのためのアルゴリズムM'_{annot}(coq2scala について)」
http://proofcafe.org/~yoshihiro503/proofsummit2012.pdf

10:55-11:25 @mzpさん：「どこでもCoq」
http://www.slideshare.net/mzpi/coq-14148210

11:30-12:00 @chiguriさん：内容未定
http://www.slideshare.net/chiguri/proof-summit-2012

12:00-13:30 昼休み

13:35-14:05 @masahiro_sakaiさん：OmegaTest and beyond (仮題)(30分)
http://www.slideshare.net/sakai/omega-test-and-beyond

14:15-14:45 @pi8027さん：「Coqでスタック指向プログラミング」（30分）
14:50-15:20 @erutuf13さん：「グレブナー道場 Coq 流」（30分）
15:30-16:00 @ksknacさん：「Shall we juggle, coinductively?」 (30分)
16:05-16:35 @kikxさん：「宇宙CIC」 (30分)

16:45-17:15 @maophiliaさん：homotopy type theoryの紹介 (30分)
https://docs.google.com/open?id=0B19G9yllQLdTSHQyRlA4UEFNX1k

17:20-17:30 LT
@katayama_kさん：SF日本語版の話
http://www.randmax.jp/upload/sfja2012_katayama_k.pdf

@kaizen_nagoyaさん : 定理証明できない人による定理証明系教育
http://researchmap.jp/mubdmgcm0-45645/#_45645