Study note

Certified Programming with Dependent Types

View original Back to list

Properties

Type: Books
Status: 想读
Domain: Compilers / PL
Category: 类型系统、形式化与定理证明
Source: adam.chlipala.net
Vault note: library/books/compilers/Certified-Programming-with-Dependent-Types-04102db4ba0c2bf0.md

用 Coq 学习依赖类型和认证程序开发的进阶教材，讲如何用类型表达规格、构造证明，并把程序、证明和自动化 tactic 结合起来。

适合接在 Software Foundations 之后，用来从“证明小语言性质”推进到“写可认证的程序和库”，是程序验证方向的硬核材料。

Adam Chlipala。

Categorical Logic and Type Theory (Studies in Logic and the Foundations of Mathematics) Books · 类型系统、形式化与定理证明
Metaprogramming in Lean 4 Books · 类型系统、形式化与定理证明
Software Foundations Books · 类型系统、形式化与定理证明
Theorem Proving in Lean 4 Books · 类型系统、形式化与定理证明
Type Theory and Formal Proof : An Introduction Books · 类型系统、形式化与定理证明
Types and Programming Languages Books · 类型系统、形式化与定理证明

Loading comments...