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 adam@353:

Subset Types and Variations adam@350:

General Recursion 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 adam@381:

A Taste of Reasoning About Programming Language Syntax adam@383:

Conclusion adamc@39: adamc@39: