pl-docs

pl-docs copied to clipboard

实际上它是一个演化版本叫 computational type theory。 Martin-Löf 直觉类型论是没有 Nuprl 里面那些 quotient、equality reflection 之类的东西的。你看怎么翻译比较好吧 ：)

ice1000

我自己也找不到那个文章了，可以用 https://zhuanlan.zhihu.com/p/50792280 替代

ice1000

类型轮

1

https://github.com/FrankHB/pl-docs/blob/a557739d00300f83c8d8111d85786f04ed2cf5e4/zh-CN/typing-vs-typechecking.md?plain=1#L69

ice1000

文本处理

31

先加一个列表。部分内容待合并。 - [ ] 体例 - [ ] 内容结构 - [ ] 优化内容划分 - [ ] 新建页面？ - [ ] 如何链接[现有页面](https://github.com/FrankHB/pl-docs/blob/master/zh-CN/string-and-string-length.md)？ - [ ] 进度计划 - [x] 感兴趣的优先重点？（iAsiby：[先讲一讲基本概念](https://github.com/FrankHB/pl-docs/issues/6#issuecomment-491193399)。） - [...

FrankHB

关于类型安全

2

https://github.com/FrankHB/pl-docs/blob/master/zh-CN/typing-vs-typechecking.md#%E7%B1%BB%E5%9E%8B%E5%AE%89%E5%85%A8type-safety 这里写的类型安全感觉应该更准确地叙述为 语义的可靠性 (semantic soundness)。 类型安全的一个版本的定义 (又叫 type soundness) 是 progress and preservation。

ice1000