Blogs (1) >>
POPL 2019
Sun 13 - Sat 19 January 2019 Cascais, Portugal
Thu 17 Jan 2019 10:58 - 11:20 at Sala I - Gradual Types Chair(s): Nikhil Swamy

Gradually typed languages are designed to support both dynamically typed and statically typed programming styles while preserving the benefits of each. While existing gradual type soundness theorems for these languages aim to show that type-based reasoning is preserved when moving from the fully static setting to a gradual one, these theorems do not imply that correctness of type-based refactorings and optimizations is preserved. Establishing correctness of program transformations is technically difficult, because it requires reasoning about program equivalence, and is often neglected in the metatheory of gradual languages.

In this paper, we propose an axiomatic account of program equivalence in a gradual cast calculus, which we formalize in a logic we call gradual type theory (GTT). Based on Levy’s call-by-push-value, GTT gives an axiomatic account of both call-by-value and call-by-name gradual languages. Based on our axiomatic account we prove many theorems that justify optimizations and refactorings in gradually typed languages. For example, uniqueness principles for gradual type connectives show that if the $\beta\eta$ laws hold for a connective, then casts between that connective must be equivalent to the so-called “lazy” cast semantics. Contrapositively, this shows that “eager” cast semantics violates the extensionality of function types. As another example, we show that gradual upcasts are pure functions and, dually, gradual downcasts are strict functions. We show the consistency and applicability of our axiomatic theory by proving that a contract-based implementation using the lazy cast semantics gives a logical relations model of our type theory, where equivalence in GTT implies contextual equivalence of the programs. Since GTT also axiomatizes the dynamic gradual guarantee, our model also establishes this central theorem of gradual typing. The model is parametrized by the implementation of the dynamic types, and so gives a family of implementations that validate type-based optimization and the gradual guarantee.

Thu 17 Jan

Displayed time zone: Belfast change

10:36 - 12:04
Gradual TypesResearch Papers at Sala I
Chair(s): Nikhil Swamy Microsoft Research
10:36
22m
Talk
Type-Driven Gradual Security with ReferencesTOPLAS
Research Papers
Matías Toro University of Chile, Ronald Garcia University of British Columbia, Éric Tanter University of Chile & Inria Paris
DOI Media Attached File Attached
10:58
22m
Talk
Gradual Type Theory
Research Papers
Max S. New Northeastern University, Daniel R. Licata Wesleyan University, Amal Ahmed Northeastern University, USA
Link to publication DOI Media Attached File Attached
11:20
22m
Talk
Gradual Parametricity, RevisitedDistinguished Paper
Research Papers
Matías Toro University of Chile, Elizabeth Labrada University of Chile, Éric Tanter University of Chile & Inria Paris
Link to publication DOI Pre-print Media Attached File Attached
11:42
22m
Talk
Live Functional Programming with Typed Holes
Research Papers
Cyrus Omar University of Chicago, Ian Voysey Carnegie Mellon University, Ravi Chugh University of Chicago, Matthew Hammer None
Link to publication DOI Pre-print Media Attached File Attached