类型论驿站写作计划
0. 基础概念介绍
1. 无类型 \lambda 演算学习笔记(进度:100%)
- 无类型Lambda演算笔记-1(附Haskell实例)
- 无类型Lambda演算笔记-2(Lambda可定义性,附Haskell实例)
- 无类型Lambda演算笔记-3(归约和Church-Rosser定理)
2. 有类型 \lambda 演算 à la Curry学习笔记(进度:100%)
- 有类型 λ 演算 à la Curry 学习笔记-1(λ→系统)
- 有类型 λ 演算 à la Curry 学习笔记-2(λ→系统的扩展)
- 有类型 λ 演算 à la Curry 学习笔记-3(主语归约和转换)
- 有类型 λ 演算 à la Curry 学习笔记-4(强正规性)
- 有类型 λ 演算 à la Curry 学习笔记-5(类型指定的可判定性)
3.有类型 \lambda 演算 à la Church学习笔记(进度:100%)
- 有类型 λ 演算 à la Church 学习笔记-1(λ→系统)
- 有类型 λ 演算 à la Church 学习笔记-2(有类型 λ 演算立方体)
- 有类型 λ 演算 à la Church 学习笔记-3(纯类型系统PTS)
- 有类型 λ 演算 à la Church 学习笔记-4(纯类型系统的特性)
- 有类型 λ 演算 à la Church 学习笔记-5(λ立方体的强正规性)
- 有类型 λ 演算 à la Church 学习笔记-6(逻辑的表示)
- 有类型 λ 演算 à la Church 学习笔记-7(数据类型的表示)
4. Luo's UTT 学习笔记(进度:90%,继续更新)
- Luo的 UTT 学习笔记之一:UTT背景简介
- Luo的 UTT学习笔记之二:扩充构造演算(ECC)简介
- Luo's UTT学习笔记之三:元理论特性
- Luo's UTT 学习笔记之四:强[可]正规性-上
- Luo's UTT 学习笔记之五:强[可]正规性-下
- Luo's UTT 学习笔记之六:ECC 的内部逻辑
- Luo's UTT 学习笔记之七:集合论模型
- Luo's UTT 学习笔记之八:计算和逻辑理论
- Luo's UTT 学习笔记之九:说明和程序开发
- UTT
5. HoTT 学习笔记(进度:16.7%,等待拓扑学笔记开工再更新)
- HoTT学习笔记1:类型论基础
- 同伦类型论
- 集合与逻辑
- 同伦论
- 范畴论
- 集合论
6. Coq 学习笔记(进度:100%)
- Coq学习笔记1:综览 Un bref tour d'horizon
- Coq学习笔记2:类型和表达式 Types et expresssions
- Coq学习笔记3:命题和证明-1 Propositions et preuves -1
- Coq学习笔记4:命题和证明-2 Propositions et preuves -2
- Coq学习笔记5:潘多拉魔盒——依赖类型 Le produit dépendant
- Coq学习笔记6:依赖乘积类型的表达力 Puissance d'expression du produit dépendant
- Coq学习笔记7:日常逻辑 Logique de tous les jours
- Coq学习笔记8:非直谓性定义 Définitions imprédicatives
- Coq学习笔记9:归纳数据结构-1Structures de données inductives -1
- Coq学习笔记10:归纳数据结构-2 Structures de données inductives -2
- Coq学习笔记11:策略和证明自动化 Tactiques et automatisation
- Coq学习笔记12:归纳谓词 Prédicats inductifs
7. MTT语义学学习笔记(进度:14%,继续慢速更新)
- MTT语义学简介
- 判断和 \Pi -多形
- 子类型
- 命题作为类型
- 依赖事件类型
- MTT语义学既是模型论语义学也是证明论语义学
- 依赖范畴语法
8. 泛代数学习笔记
- 泛代数学习笔记1:定义和一些例子
- 代数和态射
- 构造
- 代数类
9. 范畴论学习笔记(进度:100%)
- 范畴论学习笔记1:基本概念
- 范畴论学习笔记2:范畴生范畴
- 范畴论学习笔记3:箭头的种类
- 范畴论学习笔记4:初始和终结对象、广义元素
- 范畴论学习笔记5:积和余积
- 范畴论学习笔记6:等化子和余等化子
- 范畴论学习笔记7:极限和余极限
- 范畴论学习笔记8:子对象和指数
- 范畴论学习笔记9:群对象和自然数对象
- 范畴论学习笔记10:函子
- 范畴论学习笔记11:范畴的范畴
- 范畴论学习笔记12:函子和极限
- 范畴论学习笔记13:Hom-函子
- 范畴论学习笔记14:逗号范畴
- 范畴论学习笔记15:自然变换
- 范畴论学习笔记16:函子范畴、范畴的等价
- 范畴论学习笔记17:米田引理
- 范畴论学习笔记18:可表函子和普遍元素
- 范畴论学习笔记19:伽罗瓦连接
- 范畴论学习笔记20:伴随
- 范畴论学习笔记21:单子(Monad)
10. 拓扑学学习笔记(正在更新,但不在本专栏发布)
11. 模型论学习笔记
12. 递归论学习笔记(预计暑期以视频方式发布)
13. 证明论学习笔记
14. 格论学习笔记(进度:50%)
编辑于 2019-03-19 19:53