スライド: プログラミング言語の意味論とCoqで証明
この辺の話題の調査というかまとめというか。発表で使ったLaTeXで作ったスライドを少し追加修正。想定時間とか大幅に間違えてるので、バランス的な面でいろいろ中途半端かもしれない。
Survey around Semantics for Programming Languages, and Machine Proof using Coq
view presentation (tags: coq)
LaTeXの緑色文字は縮小すると画面上でも読みにくいなあ。。。説明をコード中のコメントとして書いたの失敗だったかな。