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

Universes and Axioms adam@326:

Proof Search by Logic Programming adamc@132:

Proof Search in Ltac adamc@142:

Proof by Reflection adamc@235:

Proving in the Large adamc@153:

First-Order Abstract Syntax adamc@265:

Dependent De Bruijn Indices adamc@158:

Higher-Order Abstract Syntax adamc@170:

Type-Theoretic Interpreters adamc@181:

Extensional Transformations adamc@182:

Intensional Transformations adamc@262:

Higher-Order Operational Semantics adamc@39: adamc@39: