Preface

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)

Simple Imperative Programs    (Imp)

A Streamlined Treatment of Automation    (AltAuto)

Postscript

Bibliography    (Bib)