先日のメモを詳しくしてみた。ほとんど introduction しか読んでないので正しくないことを書いている可能性もそこそこあります。そういえば 2000 年代前半の文献をあまり見かけないのはなんでだろう。ここに挙げた文献の参考文献リストとか homotopy type th…

http://lkozima.hatenablog.com/entry/2014/09/15/013735 の続き。ホーア論理の健全性の証明をやろうとしていたのでした。一箇所ちょっと難しいところがあるような気がしたのでそれについて書こうとしていたのですが，あれこれ調べているうちに簡単な解決策…

プログラミング言語の理論を計算機上で記述する際にほとんど常に問題になることの一つに，対象言語の変数の扱い方があります。特に変数を束縛する構文を含む言語（関数型言語はほとんどそう）を扱いたい場合には避けて通れない問題です。何が難しいのか，ど…

モデルがないとよくわからない気がしたのでモデルを知りたい，ということで参考になりそうな文献を探してみました(まだ読んでない)。新しい順。 Awodey: Natural models of homotopy type theory (2014) http://arxiv.org/abs/1406.3219 van den Berg, Garne…