* Abstract
* Intro
** Why Gradual Typing
** Why Axiomatic Gradual Typing?
** Why These Axioms?
*** beta, eta
*** graduality
** Axioms to Implementation
** Inequalities to Observational Approximation
* Axioms of GTT
* Theorems in GTT
* GTT to CBPV Contracts
** Interpreting the Dynamic Types
*** Extending GTT
** Contracts as EP Pairs
** High-level Lemmas
* Axiomatic CBPV to Operational CBPV
** Thunkability and Linearity
** High-level Statement
* Graduality logical relation for CBPV
** Ordering Results
** Step-Indexed Logical Relation
** High-Level statement of Result
* Discussion