Gradual typing enables both static and dynamic typing in the same program, and makes it convenient to migrate code regions between the two typing disciplines. One goal of gradual typing is to provide all the benefits of static typing, such as efficiency, in statically-typed regions. However, this goal is elusive: the standard approach to mutable references imposes run-time overhead in statically-typed regions and alternative approaches are too conservative, either statically or at run-time. In this paper we present a new semantics called monotonic references which imposes none of the run-time overhead of dynamic typing in statically typed regions. With this design, casting a reference may cause a heap cell to become more statically typed. Retaining type safety is challenging with strong updates to the heap.
Wed 15 AprDisplayed time zone: Azores change
14:00 - 16:00 | |||
14:00 30mTalk | Making Random Judgments: Automatically Generating Well-Typed Terms from the Definition of a Type-System ESOP Burke Fetscher Northwestern University, Koen Claessen Chalmers University of Technology, Michał Pałka Chalmers University of Technology, John Hughes Chalmers University of Technology, Robert Bruce Findler Northwestern University | ||
14:30 30mTalk | Refinement Types for Incremental Computational Complexity ESOP | ||
15:00 30mTalk | Monotonic References for Efficient Gradual Typing ESOP Jeremy G. Siek Indiana University, Michael M. Vitousek Indiana University, Matteo Cimini Indiana University, Sam Tobin-Hochstadt Indiana University, Ronald Garcia University of British Columbia | ||
15:30 30mTalk | Inter-procedural Two-Variable Herbrand Equalities ESOP Stefan Schulze Frielinghaus Technische Universität München, Michael Petter Technische Universität München, Helmut Seidl Technische Universität München | ||