From 13ad35a74afafdce6cecaedddb6761f7ba856de9 Mon Sep 17 00:00:00 2001
From: Max New <maxsnew@gmail.com>
Date: Thu, 14 Mar 2019 17:34:31 -0400
Subject: [PATCH] outline of talk on monday

---
 talk/amal-class-spring-2019/gtt-talk.org | 27 ++++++++++++++++++++++++
 1 file changed, 27 insertions(+)
 create mode 100644 talk/amal-class-spring-2019/gtt-talk.org

diff --git a/talk/amal-class-spring-2019/gtt-talk.org b/talk/amal-class-spring-2019/gtt-talk.org
new file mode 100644
index 0000000..9bfbb9a
--- /dev/null
+++ b/talk/amal-class-spring-2019/gtt-talk.org
@@ -0,0 +1,27 @@
+* 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
-- 
GitLab