Write a Blog >>
Sat 25 Jan 2020 12:00 - 12:30 at Orleans - Programming features Chair(s): Giuseppe Castagna

Integrating static typing and dynamic typing has been popular in academia and industry. Gradual typing is one approach to this integration that preserves type soundness by casting values at run-time. For higher order values such as functions and references, a cast typically wraps them in a proxy that performs casts at use sites. This approach suffers from two problems: (1) chains of proxies can grow and consume unbounded space, and (2) statically typed code regions need to check whether the value being used is proxied. Monotonic references [Siek et al. 2015c] solve the latter problem for mutable references by directly casting the heap cell instead of wrapping the reference in a proxy. In this paper we show that monotonic references can also solve the former problem. We present a space-efficient version of the semantics for monotonic references and prove an upper bound on space overhead. Furthermore, the prior semantics for monotonic references involved storing cast expressions (not yet values) on the heap and it is not obvious how to implement this behavior efficiently in a compiler and run-time system. In our new semantics, only values are written to the heap, making the semantics straightforward to implement.

Sat 25 Jan

Displayed time zone: Saskatchewan, Central America change

10:30 - 12:30
Programming featuresWGT at Orleans
Chair(s): Giuseppe Castagna CNRS - Université de Paris, France
10:30
30m
Talk
Gradual Algebraic Data Types
WGT
Michael Greenberg Pomona College, Stefan Malewski University of Santiago de Chile, Éric Tanter University of Chile
Pre-print File Attached
11:00
30m
Talk
Gradual Typing for Extensibility by Rows
WGT
Taro Sekiyama National Institute of Informatics, Atsushi Igarashi Kyoto University, Japan
Pre-print
11:30
30m
Talk
Foreign Function Typing: Semantic Type Soundness for FFIs
WGT
Daniel Patterson Northeastern University, Amal Ahmed Northeastern University, USA
Pre-print
12:00
30m
Talk
Space-Efficient Monotonic References
WGT
Deyaaeldeen Almahallawi Indiana University, Jeremy G. Siek Indiana University, USA
Pre-print