add penn talk

talk/penn-spring-2019/abstract.md

+# Type Theoretic Gradual Typing
+
+Gradually typed languages allow for the gradual addition of static
+types to dynamically typed programs, helping one-off scripts, quick
+prototypes and legacy codebases mature into robust, reasonable
+programs. A key design principle is that this process be incremental:
+statically typed programs must be allowed to interoperate with
+dynamically typed programs or else entire codebases would have to be
+re-written before using the typed programs. However, different gradual
+languages and calculi disagree on the semantics of this
+interoperability, specifically if and when any types are checked
+dynamically at runtime.
+
+We show that type theoretic βη reasoning principles, chiefly η,
+distinguish between different dynamic type checking
+schemes. Furthermore, when combined with the principle of graduality
+(a gradual analogue of parametricity) we show that almost all of the
+cast semantics can be derived from an equational theory. By using a
+gradual type theory based on call-by-push-value as a metalanguage, we
+can derive cast semantics for many different evaluation orders from
+the same basic type theoretic principles.
+
+# Bio
+
+Max S. New is a PhD candidate in computer science at Northeastern
+University. His PhD work focuses on semantic models and (in)equational
+reasoning principles for gradually typed programming languages. More
+broadly, he is interested in the use of type theory and category
+theory to understand program semantics and language design.

talk/penn-spring-2019/homework.org

+In gradually typed lambda calculus the following programs all pass the
+type checker because the dynamic type, called `?` is considered
+compatible with any type. However, dynamic type casts are inserted
+into the program when this occurs, and a runtime error is raised if
+the types are violated.
+
+In particular we get the following (derived) rule that says that
+annotating anything with the dynamic type gives it the dynamic type
+
+t : A
+------------
+(t :: ?) : ?
+
+Let t1,t2 be defined as follows.
+  t1 = (3,4) :: ?
+  t2 = (λ x:Int. x) :: ?
+
+How do you think each of the following programs should evaluate?
+
+Can you justify your answer from a type soundness principle?
+
+Does your answer change depending on whether the language is
+call-by-value or call-by-name?
+
+1. (λ x: (Int x Int). first x) t1
+2. (λ x: (Int x Int). first x) t2
+
+3. (λ x: (Int x Int). x) t1
+4. (λ x: (Int x Int). x) t2
+
+5. (λ x:(Int x Int). true) t1
+6. (λ x:(Int x Int). true) t2
+
+For more background, see the paper
+    Gradual Type Theory
+    New, Licata and Ahmed
+    POPL 2019

talk/penn-spring-2019/outline.org

+* TODO Expand
+  - [X] title/attribution
+  - [ ] More examples to illustrate other GT semantics
+  - [X] Contributions -> Main Results
+  - [ ] More about CBPV?
+  - [ ] More about Term Precision!
+  - [ ] A bit about operational models
+    - a gradual type is a pair of a static type and an ep pair.
+
+* Intro
+** Why Gradual Typing?
+** What is Gradual Typing?
+** Idea: Derive semantics from Properties
+* Properties of Gradual Typing
+* CBPV
+* Formalizing these in a type theory
+* Deriving semantics
+* Semantic Model?
+