- 帰納的型とリカーサー
- 帰納原理を完全に書き下す
- 複雑な定義の構文構造
- イプシロン計算ってなんですかぁ？ こんなもんですよぉ
- タルスキーの定理の実例と応用
- タルスキーの最小プレ不動点定理（訂正）
- ラムダ記法とイプシロン記法を組み合わせて関数を定義する
- 論理式内の名前の消去とイプシロン項a
- ε記号、μ記号、ν記号
- 型クラス述語とイプシロン型
- 確率的圏、存在命題とスコーレム・コンビネータ
- 圏論的述語論理とお絵描き
- まだある、カリー／ハワード／ランベック対応の辞書
- 圏論的宇宙と反転原理と次元付きの記法
- 最近の型理論： 宇宙と世界、そして銀河
- 最近の型理論： 宇宙・世界・銀河 もう少し
- 最近の型理論： 型理論の構文論と意味論
- 最近の型理論： 宇宙より銀河
- 最近の型理論： 具体的・構文的なコンテキスト
- 最近の型理論： 拡張包括構造を持ったインデックス付き圏
