diff --git a/talk/amal-class-spring-2019/gtt-talk.org b/talk/amal-class-spring-2019/gtt-talk.org index 27571d423963df25544dbc7911b75e92d0586a29..028c0da9160898243f1b9588b3f637e2d3b24776 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