ProofSummit 2011 で『CoqによるMsgPackシリアライザの証明と実装』という話をしました。
ProofSummit2011でMsgPackを証明したときの話をしてきました。内容は名古屋Reject会議で話したことを膨らませた感じになっています。
話の趣旨としては「バグって怖いじゃん → じゃあ証明しようぜ → やってみた」みたいな感じです。
スライド
CoqによるMsgPackの証明
View more presentations from Hiroki Mizuno
感想
- 新宿ダンジョンこわい
- [twitter:@ikegami__]さんと[twitter:@masahiro_sakai]さんにAgdaを教えてもらえたので、とてもよかった
- Software Foundationsの和訳プロジェクト、気になります
