Wed 10 Jan 2018 13:40 - 14:05 at Watercourt - Interpretation and Evaluation Chair(s): Atsushi Igarashi

Metaprograms are programs that manipulate (generate, analyze and evaluate) other programs. These tasks are greatly facilitated by quasiquotation, a technique to construct and deconstruct program fragments using quoted code templates expressed in the syntax of the manipulated language. We argue that two main flavors of quasiquotes have existed so far: Lisp-style quasiquotes, which can both construct and deconstruct programs but may produce code that contains type mismatches and unbound variables; and MetaML-style quasiquotes, which rely on static typing to prevent these errors, but can only construct programs. In this paper, we show how to combine the advantages of both flavors into a unified framework: we allow the construction, deconstruction and evaluation of program fragments while ensuring that generated programs are well-typed and well-scoped, a combination unseen in previous work. We formalize our approach as λ{}, a multi-stage calculus with code pattern matching and rewriting, and prove its type safety. We also present its realization in Squid, a metaprogramming framework for Scala, leveraging Scala’s expressive type system. To demonstrate the usefulness of our approach, we introduce speculative rewrite rules, a novel code transformation technique that makes decisive use of these capabilities, and we outline how it simplifies the design of some crucial query compiler optimizations.

Squid is open source, available online at https://github.com/epfldata/squid/.

Wed 10 Jan

Displayed time zone: Tijuana, Baja California change

13:40 - 15:20
Interpretation and EvaluationResearch Papers at Watercourt
Chair(s): Atsushi Igarashi Kyoto University, Japan
13:40
25m
Talk
Unifying Analytic and Statically-Typed Quasiquotes
Research Papers
Lionel Parreaux EPFL, Antoine Voizard University of Pennsylvannia, Amir Shaikhha EPFL, Christoph E. Koch EPFL
Pre-print
14:05
25m
Talk
Jones-Optimal Partial Evaluation by Specialization-Safe Normalization
Research Papers
Matt Brown UCLA, Jens Palsberg University of California, Los Angeles (UCLA)
14:30
25m
Talk
Migrating Gradual Types
Research Papers
John Peter Campora ULL Lafayette, Sheng Chen University of Louisiana at Lafayette, Martin Erwig Oregon State University, Eric Walkingshaw Oregon State University
14:55
25m
Talk
Intrinsically-Typed Definitional Interpreters for Imperative Languages
Research Papers
Casper Bach Poulsen Delft University of Technology, Arjen Rouvoet Delft University of Technology, Andrew Tolmach Portland State University, Robbert Krebbers Delft University of Technology, Eelco Visser Delft University of Technology
DOI Pre-print