ヒビルテ経由、ここからダウンロード。先々週に8割読んでいて、残り数ページを本日やっと読了。 LawvereやHuwig-Poigne' の結果（各種の対角線論法を圏論の言葉で書き直し一般化する）を、圏論の言葉を使わずに紹介したもの。圏論の用語を使わずに同じ形のダ…

16時より18時まで、参加者10人ぐらい。本日が最終回、Universeの導入、Jan Smithの結果の説明とmonomorphic type theory。

16時より18時まで、参加者10人ぐらい。Identityやinductionなどのruleをどうタイプで表現するのか。

この講演の冒頭でH. Huwig and A. PoigneのA note on inconsistencies caused by fixpoints in a cartesian closed categoryを引用しましたが、ヒビルテさんの2006年11月のエントリーでこの論文を知り、またと2007年2月のエントリーも参考にさせて頂きました…

開始時間は10時、参加者は10人程度。1時間の予定が、質問等が加熱して30分近くオーバー。基本的には皆さんに興味を持って頂けた様子。pdfファイルを大学のサイトにおいてあります。興味のある方はどうぞご覧ください。発表要旨は以下の通り。 本発表では、曖…

ヒビルテ経由、集中講義での講義ノート。原稿はこちら。とてもわかりやすいです。発表のための再確認のために最適。 ここのお薦め通り、次はこれでも読もう。

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

備忘のためメモ。Bengt Nordstrom教授特別連続講義@産総研。構成的Type理論について。

15時10分より16時40分まで。partial recursive functionをMartin-Lof type theoryで表現する。inductive definitionをtypeで表現するとき、普通にやるとstrictlyにpositiveなindexed definition でなくなるものが出てくるので、”indexed inductive recursive…