checkin slides just in case

talk/cmu-fall-2018/outline.org

+* Outline
+  1) The problem: gradual typing is good, but the state of the art is
+     questionable. Cast semantics is in flux. Re-use old slides
+     - Introduce graduality as a key 
+  2) CBN GTT: simple axiomatics, show the proof for function types,
+     mention category theoretic connections. Re-use old slides
+     - Mention double category semantics briefly, which are closely
+       related to parametricity
+  3) CBPV GTT: captures CBV and CBN, refines analysis of casts:
+     upcasts are pure values, downcasts are stacks. Make new slides!
+* TODO Today
+  - [ ] (Before the talk). Re-org for parts 1 and 2 of the talk. Merge
+    NEU and FSCD talks
+  - [ ] (This afternoon) flesh out intro
+  - [ ] (This afternoon) Add some CBPV slides at the end
+  - [ ] (Sundary) Finish slides, practice.
+* Expanded Outline
+** Intro
+   - Gradual typing is about migration from dynamic to static typing
+     styles
+     - the "dynamics" of GT
+   - Very basic account of mechanics
+     - very simple overview of the "mechanics" of GT, no details
+   - But the state of the art is *nasty*
+     - many different cast semantics have been proposed
+     - just present a pile of rules
+   - Our approach: type theoretic, axiomatic. Take the properties of
+     types and casts that we want, decompose complex structures,
+     *derive* the complex definitions from a small type-theoretic core
+     - Key ingredient: *graduality*
+     - Key obstacle: dynamic typing inherently involves *effects*, so
+       we need equational theories that are sound even in the presence
+       of effects
+** CBN GTT
+   - Motivate:
+     - Based on FSCD 2018
+     - start with a simple, CBN lambda calculus, only do the negative
+       types. This works even with effects, but not 
+   - Syntax
+     - types, type precision
+     - terms, term precision
+     - Casts
+   - Theorems
+     - Casts form galois connections, in practice strengthen this to
+       ep pair
+     - Uniqueness theorems: casts must be their functorial actions
+   - Semantics
+     - Category internal to preorders: well-studied under the name
+       "double categories"
+     - A double category that has all upcasts/downcasts is called a
+       "proarrow equipment" or a "framed bicategory", some nice work
+       by Mike Shulman on this
+** CBPV GTT (conditionally accepted to POPL 2019)
+   - Motivate:
+     - most gradual typing is CBV
+     - want to prove program equivalences in the presence of effects
+   - Intro to CBPV
+   - Casts as values/stacks
+     - same definition(!)
+     - recover 
+   - Used non-gradual CBPV as a metalanguage for defining models
+     - Dynamic type for Scheme in CBPV
+   - Experience
+     - CBPV rocks: keep the nice equational theory, but handle effects
+     - The syntax guided us naturally to the right solution
+     - type theoretic approach plays nicely with others

talk/cmu-fall-2018/talk-defs.tex

+\usepackage{stmaryrd}
+\usepackage{graphicx}
+
+\newcommand{\preciser}{\sqsubseteq}
+\newcommand{\dynr}{\sqsubseteq}
+\newcommand{\equiprecise}{\mathrel{\sqsupseteq\sqsubseteq}}
+\newcommand{\equidyn}{\mathrel{\sqsupseteq\sqsubseteq}}
+\newcommand{\vpreciser}{\rotatebox[origin=c]{-90}{$\preciser$}}
+
+\newcommand{\dyn}{{?}}
+\newcommand{\obcast}[2]{\langle{#2}\Leftarrow{#1}\rangle}
+\newcommand{\upcast}[2]{\langle{#2}\leftarrowtail{#1}\rangle}
+\newcommand{\upcastpr}[2]{\langle{#2}\hookleftarrow{#1}\rangle}
+\newcommand{\dncast}[2]{\langle{#1}\twoheadleftarrow{#2}\rangle}
+
+\newcommand{\type}{\,\text{type}}
+\newcommand{\ctx}{\,\text{ctx}}
+\newcommand{\dom}{\text{dom}}
+
+\newcommand{\cat}{\mathbb}
+\newcommand{\Ctx}{\text{Ctx}}
+\newcommand{\Multi}{\text{Multi}}
+\newcommand{\PTT}{\text{PTT}}
+\newcommand{\PTTS}{PttS }
+\newcommand{\CPM}{CPM }
+\newcommand{\GTT}{\text{GTT}}
+\newcommand{\pocat}{\text{PoCat}}
+\newcommand{\sem}[1]{\llbracket{#1}\rrbracket}
+\newcommand{\interp}[1]{\llparenthesis{#1}\rrparenthesis}
+\newcommand{\floor}[1]{\lfloor{#1}\rfloor}
+
+\newcommand{\err}{\mho}
+\newcommand{\id}{\text{id}}
+\newcommand{\app}{\text{app}}
+\newcommand{\pair}{\text{pair}}
+\newcommand{\unit}{\text{unit}}
+\newcommand{\tl}{\triangleleft}
+
+\newcommand{\coreflection}{\text{CoReflect}}
+
+% mathpartir hacks
+\newcommand{\axiom}[2]{\inferrule*[Right=#1]{~}{#2}}
+\newcommand{\invinferrule}{{\mprset}{fraction={===}}\inferrule}
+
+\newcommand{\funupcast}[6]{\lambda #6 : #3. \upcast{#2}{#4}{(#5 (\dncast{#1}{#3}{#6}))}}
+\newcommand{\fundncast}[6]{\lambda #6 : #3. \dncast{#2}{#4}{(#5 (\upcast{#1}{#3}{#6}))}}
+
+\newcommand{\produpcast}[5]{(\upcast{#1}{#3}\pi_0{#5}, \upcast{#2}{#4}\pi_0{#5})}
+
+\newcommand{\bnfalt}{\mathrel{\bf \,\mid\,}}
+\newcommand{\bnfdef}{\mathrel{\bf ::=}}
+
+%% Local Variables:
+%% compile-command: "latexmk -c main.tex; latexmk -pdf main.tex"
+%% End:

talk/popl-winter-2019/outline.org

+* Technical Bits
+  - How much CBPV do we discuss? (little)
+  - Do we show the specification for casts (yes)
+  - Do we show the dynamic computation type? (maybe)
+* Outline
+** Intro
+   - Goals of GT (copy the ICFP slides here)
+   - Issue: what should the dynamic semantics be? We want the types to
+     remain meaningful
+   - This paper: Axiomatize our desires: typed reasoning/optimization
+     and gradual evolution. Explore the consequences
+     - Main result: Strong typed based reasoning *uniquely determines*
+       most of the cast semantics.
+     - Prove for CBV, CBN and mix of these semantics for simple types.
+** Background
+*** Graduality
+    - Graduality says that changing the types of a program to be more
+      *precise* means that the resulting program should have more
+      refined behavior.
+*** CBPV
+    - Gradual Typing inherently involves
+      - Higher-order dynamic types ? -> ? <| ? so we have recursion
+      - Runtime errors
+      - Need an axiomatic framework that accommodates effects
+      - Our savior: CBPV
+      - subsumes CBV and CBN in a strong sense
+    - What is CBPV?
+      - An effect calculus into which call-by-value and call-by-name
+        languages can be embedded
+      - Based on beta, eta axioms: lambda calculus for effects
+      - Generalizes Moggi's metalanguage from (strong) monads to
+        adjunctions
+** Axioms (Theory)
+** Theorems (Consequences)
+** Models?
+** Conclusion
+* Real Outline
+** Intro
+*** What is Gradual Typing for?
+*** The problem: many different semantics, trade off soundness
+*** Design Principles have emerged
+*** Our Contribution: Axiomatize these design principles, show that some of them have *unique solutions*
+** What are the Principles?
+*** Graduality
+*** Type Based Reasoning
+**** The Humble Eta Principle(s)
+     - Naive Eta Principle
+     - CBV Eta Principle for functions
+     - Show Sum or Bool Eta principle
+       - fails in CBN
+** Axiomatizing the Principles
+*** Extend CBPV
+    - 3 ingredients: ordering, dynamic and casts
+    - For each type add congruence, beta, eta
+    - Emphasize *modularity*
+** Consequences of the Axioms
+*** Laundry List of Theorems
+    - Purity of upcasts/dual purity of downcsats (related to
+      Wadler-Findler/TH-Felleisen's blame soundness property)
+      - applications to optimization?
+    - Compositionality
+      - identity, composition
+    - EP Pairs
+    - Uniqueness Principles
+    - End on a bang: this works for call-by-value, call-by-name, etc
+** More Inside
+   - More theorems
+   - Soundness of the axioms
+     - We construct (many) models by translation to CBPV. Implement
+       the dynamic types using recursive value/computation types
+     - Dynamic value type as a sum, Dynamic comp type as a product
+     - Logical Relation to prove soundness of the ordering wrt an
+       operational semantics
+** Related/Future Work
+   - AGT: doesn't satisfy eta principles, can it be modified to do so?
+   - Greenman-Felleisen: show weakened principles but not blah
+   - Degen-Thiemmann?
+** Future Work
+   - Inductive, Coinductive, Recursive types should all have a similar
+     theorem.
+   - One of our models is quite similar to Scheme, maybe CBPV should
+     be taken more seriously as an intermediate lang?
+** Conclusions
+   - Axiomatic Approach shows us the strength of the graduality concept
+     - but also that it is a reimagining of EP pairs
+   - CBPV is a convenient metalanguage to prove results for many
+     different evaluation orders
+     - Our models suggest new