outline of talk on monday

talk/amal-class-spring-2019/gtt-talk.org

+* Outline
+** Intro: What semantics of Gradual Typing is Right?
+*** URGENT Pop Quiz: How does this program run?
+    - x:
+    - ->:
+    - refactoring: lift a pattern match out of a lambda.
+*** Why do programs error?
+    - Type Safety, Blame safety? neither prevent dropping intermediate
+      casts
+    - Let's be positive: types are there to *help us*, to allow us to
+      refactor, optimize in a modular way
+** Relational Soundness Theorems
+*** Contextual Equivalence + βη-equivalence
+*** Graduality as Contextual Approximation
+** Gradual Type Theory
+   - Now that we have formulated what we *want* out of gradual
+     languages, we can ask: what are the consequences of the
+     definition? How much design freedom do we really have?
+   - We accomplish this by *axiomatizing* these properties in a type
+     theory we call Gradual Type Theory
+   - The result of this axiomatization is that we can *prove*
+     operational reductions follow from our relational soundness
+     theorems. So most of the semantics is totally determined.
+*** TODO What to present?
+    - [ ] Idea for syntax, just CBN? Or try to talk about CBPV?
+    - The "type" of the model construction theorem. No logical
+      relation