Name: Certified Programming with Dependent Types
ISBN: 9780262317863

Certified Programming with Dependent Types

The technology of mechanized program verification can play a supporting role in many kinds of research projects in computer science, and related tools for formal proof-checking are seeing increasing adoption in mathematics and engineering. This book provides an introduction to the Coq software for writing and checking mathematical proofs. It takes a practical engineering focus throughout, emphasizing techniques that will help users to build, understand, and maintain large Coq developments and minimize the cost of code change over time. Two topics, rarely discussed elsewhere, are covered in detail: effective dependently typed programming (making productive use of a feature at the heart of the Coq system) and construction of domain-specific proof tactics. Almost every subject covered is also relevant to interactive computer theorem proving in general, not just program verification, demonstrated through examples of verified programs applied in many different sorts of formalizations. The book develops a unique automated proof style and applies it throughout; even experienced Coq users may benefit from reading about basic Coq concepts from this novel perspective. The book also offers a library of tactics, or programs that find proofs, designed for use with examples in the book. Readers will acquire the necessary skills to reimplement these tactics in other settings by the end of the book. All of the code appearing in the book is freely available online.

What Hacker News says

stepchowfunMar 2022

I highly recommend just downloading and playing with a language based on type theory, such as Coq/Lean/Agda. I know Coq well, so I can recommend Software Foundations and Certified Programming with Dependent Types. Write some simple proofs in one of those languages; for example you could try proving that addition of natural numbers is associative and commutative. At some point, it will start to click and you will feel like every other programming language you've ever used before is severely underpowered for not having dependent types.

If you don't have experience with typed functional programming (e.g., Haskell/OCaml/SML), you will probably want to start learning one of those languages first. These languages won't really teach you type theory (at least, not the powerful kind of type theory that lets you do mathematics), but they will help you get comfortable with the syntax that type theory-based languages tend to use.

I've written a Coq tutorial [1], but it assumes you already know functional programming. I'd appreciate any feedback on it if you decide to tackle it!

If you want to dive into the theory, you can try reading Chapter 1 of the Homotopy Type Theory book. But many people find that book to be impenetrable, so it might not be what you're looking for (I personally love it).

[1] https://github.com/stepchowfun/proofs/tree/main/proofs/Tutor...

thread

x13pixelsFeb 2022

If you are interested in building programs with proofs of correctness, one of the authors of A Tensor Language (ATL), Adam Chlipala, has a book called "Certified Programming with Dependent Types" that can be read at http://adam.chlipala.net/cpdt/

thread

ebingdomNov 2021

I'd say it's the recommended book for type systems. For type theory, I'd recommend "Certified Programming with Dependent Types" by Adam Chlipala or "Programming Language Foundations in Agda" by Philip Wadler.

thread

logicchainsJul 2021

There's an excellent online book that introduces Coq and how to use it for verification of programs: https://softwarefoundations.cis.upenn.edu/. There's also a more advanced book, http://adam.chlipala.net/cpdt/, that goes into more detail. In comparison, Lean has little teaching material for formal verification of programs.

thread

harveywiDec 2017

I started with Certified Programming with Dependent Types (http://adam.chlipala.net/cpdt/).

If you are more interested in programming, consider trying Idris (http://idris-lang.org/). Edwin Brady, the language designer, wrote a great book that I would recommend called Type-Driven Development with Idris (https://www.manning.com/books/type-driven-development-with-i...).

thread

jeremysalwenOct 2017

If you really want to build on "rock", check out Bedrock: http://plv.csail.mit.edu/bedrock/ . Don't just prove your program is memory safe, prove it satisfies arbitrary properties! (A bit tongue in cheek, but the tools are really cool). Check out http://adam.chlipala.net/cpdt/cpdt.pdf for a nice introduction.

thread