Functional Programming in Coq    (Basics)

Proof by Induction    (Induction)

Working with Structured Data    (Lists)

Polymorphism and Higher-Order Functions    (Poly)

More Basic Tactics    (Tactics)

Logic in Coq    (Logic)

Inductively Defined Propositions    (IndProp)

Total and Partial Maps    (Maps)

The Curry-Howard Correspondence    (ProofObjects)

Induction Principles    (IndPrinciples)

Properties of Relations    (Rel)

Simple Imperative Programs    (Imp)

Lexing and Parsing in Coq    (ImpParser)

An Evaluation Function for Imp    (ImpCEvalFun)

Extracting OCaml from Coq    (Extraction)

More Automation    (Auto)

A Streamlined Treatment of Automation    (AltAuto)


Bibliography    (Bib)