Preface

Basics: Functional Programming in Coq

Induction: Proof by Induction

Lists: Working with Structured Data

Poly: Polymorphism and Higher-Order Functions

Tactics: More Basic Tactics

Logic: Logic in Coq

IndProp: Inductively Defined Propositions

Maps: Total and Partial Maps

ProofObjects: The Curry-Howard Correspondence

IndPrinciples: Induction Principles

Rel: Properties of Relations

Imp: Simple Imperative Programs

ImpParser: Lexing and Parsing in Coq

ImpCEvalFun: Evaluation Function for Imp

Extraction: Extracting ML from Coq

Equiv: Program Equivalence

Hoare: Hoare Logic, Part I

Hoare2: Hoare Logic, Part II

HoareAsLogic: Hoare Logic as a Logic

Smallstep: Small-step Operational Semantics

Auto: More Automation

Types: Type Systems

Stlc: The Simply Typed Lambda-Calculus

StlcProp: Properties of STLC

MoreStlc: More on the Simply Typed Lambda-Calculus

Sub: Subtyping

Typechecking: A Typechecker for STLC

Records: Adding Records to STLC

References: Typing Mutable References

RecordSub: Subtyping with Records

Norm: Normalization of STLC

LibTactics: A Collection of Handy General-Purpose Tactics

UseTactics: Tactic Library for Coq: A Gentle Introduction

UseAuto: Theory and Practice of Automation in Coq Proofs

PE: Partial Evaluation

Postscript

Bib: Bibliography