checkin for saefty

talk/popl-winter-2019/outline.org

@@ -86,3 +86,77 @@
    - CBPV is a convenient metalanguage to prove results for many
      different evaluation orders
      - Our models suggest new 
+* DONE Slides
+** TODO Intro (Small)
+   - [ ] Our Approach/Contributions: make a diagram for
+     this. Semantics -> Soundness flips to Soundness -> Semantics
+** TODO (Small) Principles
+   - [ ] smooth out
+   - [ ] citation
+** TODO (Large) Axioms
+   - [ ] Term Precision
+   - [ ] Errors
+   - [ ] beta, eta using equidyn
+   - [ ] Specifying Casts
+** TODO (Large) Theorems
+   - [ ] Uniqueness Principles
+   - [ ] Explain the consequences of this.
+   - [ ] EP Pairs? Compositionality? Maybe just have a "and many more slide"
+** TODO (Small) Models
+   - [ ] Make own mini-section
+** TODO (Medium) Wrap-up
+   - [ ] Related Work: Thiemann?
+   - [ ] Future Work
+   - [ ] Better Conclusion slide
+
+Next: Axioms
+* TODO Practice
+** DONE Script Runthrough
+   - [X] Intro
+   - [X] Soundness
+   - [X] Axioms
+   - [X] Theorems
+   - [X] Wrapup
+** TODO Practice Practice Practice
+*** It's too long
+    - too much: details of call-by-push-value
+    - too much: eta laws?
+    - too much: intro, didn't get to what we do for like 11ish minutes?
+    - too much: talk about precision, congruence rules, beta-eta principles
+      - I don't think it's important to go over the typing for instance
+    - Combine F, U into one slide, then show the cbv/cbn translations
+      into CBPV
+    - transition from cast semantics to axiomatic semantics is not
+      clean
+*** Amal notes
+    - put these in final slide?
+      - emphasize the axioms to derivations more
+      - emphasize reasoning principles rather than type safety
+    - future work: more complex type features
+** Questions
+   - What about blame?
+     - We don't give a treatment of blame in the paper, but a paper by
+       Wadler & Findler suggests that we should make the upcasts
+       always blame negative party and downcasts always blame the
+       positive party
+     - And we argue in the paper that that is related to our proof
+       that upcasts are pure and downcasts are linear
+   - Even CBV Eta is violated by pointer/object equality?
+     - right, and for this reason the simple wrapping semantics of
+       contracts/casts doesn't work for those systems, and people
+       introduce proxies
+     - however I think there should be a kind of eta law for proxies
+       that justifies those implementations.
+   - What about Call-by-need?
+     - We discuss this in the related work section. In addition to
+       call-by-value and call-by-name, there is also a translation of
+       what Levy calls the "lazy paradigm" that is analogous to
+       Haskell's behavior in that it supports the "seq" operation. We
+       show that this too reproduces previous work on contracts for
+       Haskell.
+   - Does this help with parametricity?
+     - Not directly at least. Perhaps the axiomatic approach can help
+       but it wouldn't be the same theorem as here because
+       parametricity is stronger than eta principles. I.e., the forall
+       type can satisfy an eta principle without satisfying
+       parametricity.