adamc@39: adamc@39: Certified Programming with Dependent Types adamc@39: adamc@39: adamc@39:

Certified Programming with Dependent Types

adamc@39: adamc@39:

Introduction adamc@39:

Some Quick Examples adamc@57:

Introducing Inductive Types adamc@56:

Inductive Predicates adamc@62:

Infinite Data and Proofs adamc@70:

Subset Types and Variations adamc@83:

More Dependent Types adamc@105:

Dependent Data Structures adamc@118:

Reasoning About Equality Proofs adamc@132:

Proof Search in Ltac adamc@142:

Proof by Reflection adamc@152:

First-Order Variable Representations adamc@39: adamc@39: