ProofSummit 2011 で『CoqによるMsgPackシリアライザの証明と実装』という話をしました。 - みずぴー日記

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

[mzp]

MsgPack for OCamlの裏側について話してきました。

[nminoru]

やはりシステム検証の学ばなければならない。