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

Certified Programming with Dependent Types

adamc@39: adam@543:

Introduction adam@543:

Some Quick Examples adam@543:

Introducing Inductive Types adam@543:

Inductive Predicates adam@543:

Infinite Data and Proofs adam@543:

Subset Types and Variations adam@543:

General Recursion adam@543:

More Dependent Types adam@543:

Dependent Data Structures adam@543:

Reasoning About Equality Proofs adam@543:

Generic Programming adam@543:

Universes and Axioms adam@543:

Proof Search by Logic Programming adam@543:

Proof Search in Ltac adam@543:

Proof by Reflection adam@543:

Proving in the Large adam@543:

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

Conclusion adamc@39: adamc@39: