Study note
Type Theory and Formal Proof : An Introduction
Properties
- Type
- Books
- Status
- 想读
- Domain
- Compilers / PL
- Category
- 类型系统、形式化与定理证明
- Source
- book.douban.com
- Vault note
library/books/compilers/Type-Theory-and-Formal-Proof-An-Introduction-11f3fd92774ab789.md
Summary
类型论与形式证明入门书，从无类型 lambda 演算出发，逐步进入若干基础类型系统，最终到 Calculus of Constructions，并讨论 proof checking、proof development 和用依赖类型形式化数学。
Highlights
面向需要理解逻辑规则、定义和结构化证明机制的研究生/研究者，每章都有总结、历史背景、延伸阅读和习题，适合作为类型论正规入口。
Notes
Rob Nederpelt、Herman Geuvers；2014-10-31。
Comments
Loading comments...