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@226:

Generic Programming adamc@132:

Proof Search in Ltac adamc@142:

Proof by Reflection adamc@153:

First-Order Abstract Syntax adamc@158:

Higher-Order Abstract Syntax adamc@170:

Type-Theoretic Interpreters adamc@181:

Extensional Transformations adamc@182:

Intensional Transformations adamc@190:

Modeling Impure Languages adamc@39: adamc@39: