CP Dependent Types

Whence This Book? We would all like to have programs check that our programs are correct. Due in no small part to

I will start off by jumping right in to a fully worked set of examples, building certified compilers from increasingly c

The logical foundation of Coq is the Calculus of Inductive Constructions, or CIC. In a sense, CIC is built from just tw

The so-called "Curry-Howard correspondence" states a formal connection between functional programs and mathematical proo

In lazy functional programming languages like Haskell, infinite data structures are everywhere. Infinite lists and more

So far, we have seen many examples of what we might call "classical program verification." We write programs, write the

Termination of all programs is a crucial property of Gallina. Non-terminating programs introduce logical inconsistency,

Subset types and their relatives help us integrate verification with programming. Though they reorganize the certified

Our red-black tree example from the last chapter illustrated how dependent types enable static enforcement of data struc

In traditional mathematics, the concept of equality is usually taken as a given. On the other hand, in type theory, equ

Generic programming makes it possible to write functions that operate over different types of data. Parametric polymorp

Many traditional theorems can be proved in Coq without special knowledge of CIC, the logic behind the prover. A develop

The Curry-Howard correspondence tells us that proving is "just" programming, but the pragmatics of the two activities ar

We have seen many examples of proof automation so far, some with tantalizing code snippets from Ltac, Coq's domain-speci

The last chapter highlighted a very heuristic approach to proving. In this chapter, we will study an alternative techni

It is somewhat unfortunate that the term "theorem proving" looks so much like the word "theory." Most researchers and p

Reasoning about the syntax and semantics of programming languages is a popular application of proof assistants. Before

I have designed this book to present the key ideas needed to get started with productive use of Coq. Many people have l