2008-11-12から1日間の記事一覧

"Calculus of Inductive Constructions and types-as-sets interpretation" (Gyesik Lee)

CICの集合論的解釈について。WernerとAczel、またMiquel at el の結果を概観し、またβ変換による等号の判定を体系の外側でやるCIC方式と、体系の内側でやるマーティン・レフ方式を比較した。

比較的暖かい。出勤して打ち合わせと原稿書き。談話会のあと、夕食に出てから所に戻り、原稿の準備を23時まで。24時半に帰宅。