git @ Cat's Eye Technologies The-Glosscubator / master by-topic / Coq / Books.md
master

Tree @master (Download .tar.gz)

Books.md @masterview markup · raw · history · blame

Coq Books

Software Foundations

.

Certified Programming with Dependent Types

  • subtitle: A Pragmatic Introduction to the Coq Proof Assistant
  • authors: Adam Chlipala
  • date: 2013
  • online @ archive.org
  • booksite: http://adam.chlipala.net/cpdt/

.

Modeling and Proving in Computational Type Theory Using the Coq Proof Assistant (Draft)

.