Write a Blog >>
ICFP 2018
Sun 23 - Sat 29 September 2018 St. Louis, Missouri, United States
Wed 26 Sep 2018 13:45 - 14:07 at Stifel Theatre - Gradual Typing and Proving Chair(s): Éric Tanter

Gradually typed languages allow statically typed and dynamically typed code to interact while maintaining benefits of both styles. The key to reasoning about about these mixed programs is Siek-Vitousek-Cimini-Boyland’s (dynamic) gradual guarantee, which says that giving one piece of a program a more precise type only adds runtime type checking, and does not otherwise change behavior. In this paper, we give a semantic reformulation of the gradual guarantee called graduality.

We change the name to promote the analogy that graduality is to gradual typing what parametricity is to polymorphism. Each gives a local-to-global, syntactic-to-semantic reasoning principle that is formulated in terms of a kind of observational approximation. Utilizing the analogy, we propose a novel logical relation for proving graduality.

Furthermore, we show that embedding-projection pairs (ep pairs) are to graduality what relations are to parametricity. We argue that casts between two types where one is “more dynamic” (less precise) than the other necessarily form an ep pair, and we use this to cleanly prove the graduality cases for casts from the ep-pair property. To construct ep pairs, we give an analysis of the type dynamism relation—also known as type precision or naïve subtyping—that interprets the rules for type dynamism as compositional constructions on ep pairs, analogous to the coercion interpretation of subtyping.

Wed 26 Sep

Displayed time zone: Guadalajara, Mexico City, Monterrey change

13:00 - 14:30
Gradual Typing and ProvingResearch Papers at Stifel Theatre
Chair(s): Éric Tanter University of Chile & Inria Paris
13:00
22m
Talk
A Spectrum of Type Soundness and Performance
Research Papers
Ben Greenman Northeastern University, USA, Matthias Felleisen Northeastern University, USA
DOI
13:22
22m
Talk
Casts and Costs: Harmonizing Safety and Performance in Gradual Typing
Research Papers
John Peter Campora ULL Lafayette, Sheng Chen University of Louisiana at Lafayette, Eric Walkingshaw Oregon State University
DOI
13:45
22m
Talk
Graduality from Embedding-Projection Pairs
Research Papers
Max S. New Northeastern University, Amal Ahmed Northeastern University, USA
DOI
14:07
22m
Talk
Ready, Set, Verify! Applying hs-to-coq to Real-World Haskell Code (Experience Report)
Research Papers
Joachim Breitner DFINITY Foundation, Antal Spector-Zabusky , Yao Li University of Pennsylvania, Christine Rizkallah University of New South Wales, John Wiegley BAE Systems, Stephanie Weirich University of Pennsylvania, USA
DOI