talk done

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?
+*** DONE Pop Quiz: How does this program run?
     - (lambda (f : ? -> ?). true)  3
       - dynamic typing: evaluates to true
       - almost every gradual language: error: 3 is not ? -> ?
@@ -37,7 +37,9 @@
    - 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
+*** DONE What to present?
+    - Examples
+    - beta-eta as ctx equivalences
+    - graduality as ctx approximation
+    - casts as lubs/glbs
+    - "headline theorem": derive contracts from soundness