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

Gradual typing allows programmers to use both static and dynamic typing in a single program. However, a well-known problem with sound gradual typing is that the interactions between static and dynamic code can cause significant performance degradation. These performance pitfalls are hard to predict and resolve, and discourage users from using gradual typing features. For example, when migrating to a more statically typed program, often adding a type annotation will trigger a slowdown that can be resolved by adding more annotations elsewhere, but since it’s not clear where the additional annotations must be added, the easier solution is to simply remove the annotation.

To address these problems, we develop: (1) a static cost semantics that accurately predicts the overhead of static-dynamic interactions in a gradually typed program, (2) a technique for efficiently inferring such costs for all combinations of inferrable type assignments in a program, and (3) a method for translating the results of this analysis into specific recommendations and explanations that can help programmers understand, debug, and optimize the performance of gradually typed programs. We have implemented our approach in Herder, a tool for statically analyzing the performance of different typing configurations for Reticulated Python programs. An evaluation on 15 Python programs shows that Herder can use this analysis to accurately and efficiently recommend type assignments that optimize the performance of these programs without sacrificing type safety.

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