POPL 2026
Sun 11 - Sat 17 January 2026 Rennes, France
Tue 13 Jan 2026 09:35 - 10:05 at Salle 19 - Types and logics Chair(s): Yukiyoshi Kameyama

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 Jan

Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

09:00 - 10:30
Types and logicsPEPM at Salle 19
Chair(s): Yukiyoshi Kameyama University of Tsukuba
09:00
5m
Day opening
Welcome
PEPM
Yukiyoshi Kameyama University of Tsukuba, Ningning Xie University of Toronto
09:05
30m
Research 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
30m
Research 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
15m
Short-paper
S4 modal sequent calculus as intermediate logic and intermediate language (Short Paper)
PEPM
Jean Caspar École normale supérieure – PSL, INRIA, LS2N, CNRS, Guillaume Munch-Maccagnoni INRIA
File Attached
10:20
15m
Short-paper
Epistemic Logic for Polyglots (Short Paper)
PEPM
Luis Garcia , Chris Martens Northeastern University
File Attached