"An introduction to type theoretical ideas" (1) Bengt Nordstrom

「研究集会」ではないけれど他に適切なカテゴリーがないので。16時より18時まで。参加者20人ぐらい?
本日は初歩の初歩、直観主義のBHK解釈・direct/indirect proof・Curry-Howard対応。HaskelでType checkingを実演して見せた。第一回目なので特に語ることも無し。

梅田でhint-mintとプリンを買ってから19時半に帰宅、夕食はシチュー。食後、Cと録画したタモリ倶楽部を見る。京急線萌え。