文件名称：Certified Programming with Dependent Types
文件大小：3.88MB
文件格式：PDF
更新时间：2013-07-13 13:34:05
ProofAssistants DependentTypes AdvancedProgramming
This is a book that, from my knowledge, is the best practice book to talk about programing in the industry-strength proof assistant Coq which a dependent type system. It is good start to understand how a dependent type system works, and how a proof assistant helps in program verifications. It gives both theoretical analysis and handy examples.