prose outline

paper/outline.org

+* 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