Mon 8 Jan 2018 14:30 - 15:00 at Crocker - Session 1-2 Chair(s): Kenichi Asai

Embedding a domain-specific language (DSL) in a general purpose host language is an efficient way to develop a new DSL. Various kinds of languages and paradigms can be used as host languages, including object-oriented, functional, statically typed, and dynamically typed variants, all having their pros and cons. For deep embedding, statically typed languages enable early checking and potentially good DSL error messages, instead of reporting runtime errors. Dynamically typed languages, on the other hand, enable flexible transformations, thus avoiding extensive boilerplate code. In this paper, we introduce the concept of gradually typed symbolic expressions that mix static and dynamic typing for symbolic data. The key idea is to combine the strengths of dynamic and static typing in the context of deep embedding of DSLs. We define a gradually typed calculus $\lambda^{<\star>}$, formalize its type system and dynamic semantics, and prove type safety. We introduce a host language called Modelyze that is based on $\lambda^{<\star>}$, and evaluate the approach by embedding a series of equation-based domain-specific modeling languages, all within the domain of physical modeling and simulation.

Mon 8 Jan

Displayed time zone: Tijuana, Baja California change

14:00 - 15:30
Session 1-2PEPM at Crocker
Chair(s): Kenichi Asai Ochanomizu University
14:00
30m
Talk
A Guess-and-Assume Approach to Loop Fusion for Program Verification
PEPM
Akifumi Imanishi Kyoto University, Kohei Suenaga Graduate School of Informatics, Kyoto University, Atsushi Igarashi Kyoto University, Japan
DOI
14:30
30m
Talk
Gradually Typed Symbolic Expressions
PEPM
David Broman KTH Royal Institute of Technology, Jeremy G. Siek Indiana University, USA
DOI
15:00
30m
Talk
On the Cost of Type-Tag Soundness
PEPM
Ben Greenman Northeastern University, Zeina Migeed University of California, Los Angeles
DOI