Coq関係の講演

面白かった・・・と言えれば私も研究者としてそれなりってところだと思うが。
いかんせん英語なので半分くらいしかわからない。
わかる範囲を言えば、CoqのtermとCoqで定義されたラムダ項（ただしwell-typedに限る）の相互変換をしようとして、何が問題で何が速度のボトルネックになるか、という話。
こんなの書いても誰も興味持てないと思うけど、まあ気にしない。
しかし、あの圧迫感のようなものに対抗できなければ研究者にはなれそうもないなあ。