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