From 7be98f42f2e34a39ef21772ce5e8e274695c5dce Mon Sep 17 00:00:00 2001
From: Max New <maxsnew@gmail.com>
Date: Tue, 19 Mar 2019 09:41:57 -0400
Subject: [PATCH] talk done
---
talk/amal-class-spring-2019/gtt-talk.org | 12 +++++++-----
1 file changed, 7 insertions(+), 5 deletions(-)
diff --git a/talk/amal-class-spring-2019/gtt-talk.org b/talk/amal-class-spring-2019/gtt-talk.org
index 27571d4..028c0da 100644
--- a/talk/amal-class-spring-2019/gtt-talk.org
+++ b/talk/amal-class-spring-2019/gtt-talk.org
@@ -1,6 +1,6 @@
* 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
--
GitLab