Syntactic sugars ease the definition of new language constructs by transforming them into an existing core language. Previous works lift independent typing rules and other semantics for these new constructs from the core language. The lifted semantics preserve the abstraction boundary of syntactic sugars, freeing users from inspecting desugared code that they did not write. While sugars may interact with contextual information during desugaring in general, these works are limited to simple sugars that do not. We identify a class of contextual sugars and present an extended algorithm for lifting their typing rules. With the addition of contexts, naïvely representing desugaring results in the core language may cause unexpected behavior and break hygiene. We introduce anchored terms that can point to the provenance of their contexts to represent desugaring results, which is similar to mechanisms used in Racket macros. Anchored terms need not concern authors or users of contextual sugars, but enable local reasoning. The lifted typing rules are sound with respect to the typing of anchored core language terms.
Tue 13 JanDisplayed time zone: Brussels, Copenhagen, Madrid, Paris change
09:00 - 10:30 | |||
09:00 5mDay opening | Welcome PEPM | ||
09:05 30mResearch paper | Hole Refinements for Polymorphic Type-and-Example Driven Synthesis PEPM Niek Mulleners Utrecht University, Johan Jeuring Utrecht University, Wouter Swierstra Utrecht University, Netherlands DOI | ||
09:35 30mResearch paper | Inferring Typing Rules for Contextual Sugars PEPM Tailai Yu Peking University, Zhichao Guan Peking University, Di Wang Peking University, Zhenjiang Hu Peking University DOI | ||
10:05 15mShort-paper | S4 modal sequent calculus as intermediate logic and intermediate language (Short Paper) PEPM File Attached | ||
10:20 15mShort-paper | Epistemic Logic for Polyglots (Short Paper) PEPM File Attached | ||