类型论学习笔记 (1) Dependent Type 与 Lambda Cube

这篇 Blog 里我会继续介绍 Typed Lambda Calculus 相关,包括 Denpendent Type 和 Lambda Cube 等,会稍微提一下 PTS;之后解释 Lambda-Cube 在 CH 同构意义下对应什么样的逻辑系统。 ...

2019 年 10 月 13 日

类型论学习笔记 (0) 入门科普

大概从这篇 Blog 开始会写一系列学习笔记,以 Type Theory 为中心写一些学习时的问题和得到的解答,也可能会作为半科普or入门读物。术语的中文翻译基本上都是从 Software-Foundation 那里看来的。 在此感谢 千里冰封 耐心解答我的问题。 作为第 0 篇 Blog,这里是科普文章。求 dalao 轻喷。 ...

2019 年 10 月 13 日