PEPM '26: "Inferring Typing Rules for ..."
Inferring Typing Rules for Contextual Sugars
Tailai Yu, Zhichao Guan, Di Wang, and Zhenjiang Hu
(Peking University, China)
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.
@InProceedings{PEPM26p61,
author = {Tailai Yu and Zhichao Guan and Di Wang and Zhenjiang Hu},
title = {Inferring Typing Rules for Contextual Sugars},
booktitle = {Proc.\ PEPM},
publisher = {ACM},
pages = {61-75},
doi = {10.1145/3779209.3779538},
year = {2026},
}
Publisher's Version
PEPM '26: "Computation-Tree Semantics: ..."
Computation-Tree Semantics: An Algorithmic Approach to Structurally Defined Relations
Sean Kristian Remond Harbo and Hans Hüttel
(Aalborg University, Denmark)
Structural operational semantics (SOS) is one of the most common formalisms for specifying language semantics. There has been much interest in automatically deriving small-step SOS definitions from big-step definitions and vice versa, as well as towards extrapolating language implementations from these inductive, declarative definitions. This work presents Computation-Tree Semantics (CTS) in which semantic configurations are tree-structured, unlike standard SOS-configurations which are “flat”. This tree-structure is key in making our approach algorithmic, meaning it is able to describe how a transition is produced, contrary to the traditional declarative approach taken by SOS. We show how one can -- in a straight-forward manner -- obtain a CTS from the big-step semantics of a simple arithmetic language, a simple while language, and the call-by-need lambda-calculus as given by Launchbury. From the resulting CTS, we then obtain a small-step understanding of all these languages. The arithmetic language example is formalised in Coq/Rocq.
@InProceedings{PEPM26p2,
author = {Sean Kristian Remond Harbo and Hans Hüttel},
title = {Computation-Tree Semantics: An Algorithmic Approach to Structurally Defined Relations},
booktitle = {Proc.\ PEPM},
publisher = {ACM},
pages = {2-16},
doi = {10.1145/3779209.3779534},
year = {2026},
}
Publisher's Version
PEPM '26: "Inferring Typing Rules for ..."
Inferring Typing Rules for Contextual Sugars
Tailai Yu, Zhichao Guan, Di Wang, and Zhenjiang Hu
(Peking University, China)
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.
@InProceedings{PEPM26p61,
author = {Tailai Yu and Zhichao Guan and Di Wang and Zhenjiang Hu},
title = {Inferring Typing Rules for Contextual Sugars},
booktitle = {Proc.\ PEPM},
publisher = {ACM},
pages = {61-75},
doi = {10.1145/3779209.3779538},
year = {2026},
}
Publisher's Version
PEPM '26: "Computation-Tree Semantics: ..."
Computation-Tree Semantics: An Algorithmic Approach to Structurally Defined Relations
Sean Kristian Remond Harbo and Hans Hüttel
(Aalborg University, Denmark)
Structural operational semantics (SOS) is one of the most common formalisms for specifying language semantics. There has been much interest in automatically deriving small-step SOS definitions from big-step definitions and vice versa, as well as towards extrapolating language implementations from these inductive, declarative definitions. This work presents Computation-Tree Semantics (CTS) in which semantic configurations are tree-structured, unlike standard SOS-configurations which are “flat”. This tree-structure is key in making our approach algorithmic, meaning it is able to describe how a transition is produced, contrary to the traditional declarative approach taken by SOS. We show how one can -- in a straight-forward manner -- obtain a CTS from the big-step semantics of a simple arithmetic language, a simple while language, and the call-by-need lambda-calculus as given by Launchbury. From the resulting CTS, we then obtain a small-step understanding of all these languages. The arithmetic language example is formalised in Coq/Rocq.
@InProceedings{PEPM26p2,
author = {Sean Kristian Remond Harbo and Hans Hüttel},
title = {Computation-Tree Semantics: An Algorithmic Approach to Structurally Defined Relations},
booktitle = {Proc.\ PEPM},
publisher = {ACM},
pages = {2-16},
doi = {10.1145/3779209.3779534},
year = {2026},
}
Publisher's Version
PEPM '26: "Towards Lightweight and Efficient ..."
Towards Lightweight and Efficient Choreographic Cloud Services
Alex Ionescu and Alejandro Russo
(Chalmers University of Technology, Sweden; University of Gothenburg, Sweden)
Choreographic programming provides a high-level abstraction for writing distributed computations while ensuring deadlock-freedom by construction. HasChor, a Haskell-based choreographic programming framework, offers a practical implementation of these ideas but faces limitations in handling an arbitrary number of participants and optimizing the communication of branches. In this work, we introduce CloudChor, a set of extensions that enhance HasChor’s expressiveness and efficiency through the use of multiply-located values, allowing choreographies to distribute and collect data across multiple participants in a structured manner. Additionally, we refine HasChor’s branching mechanism through a lightweight static analysis, selectively propagating branching decisions only to relevant participants, reducing communication overhead. To strengthen theoretical guarantees, we establish a formal semantics for HasChor and our extensions, proving deadlock-freedom. Finally, we demonstrate the practicality of our enhancements by implementing a data clean room protocol using CloudChor. Our contributions improve the applicability of choreographic programming to cloud-based secure data collaborations, making it a stronger candidate for real-world deployments.
@InProceedings{PEPM26p45,
author = {Alex Ionescu and Alejandro Russo},
title = {Towards Lightweight and Efficient Choreographic Cloud Services},
booktitle = {Proc.\ PEPM},
publisher = {ACM},
pages = {45-60},
doi = {10.1145/3779209.3779537},
year = {2026},
}
Publisher's Version
Info
PEPM '26: "Hole Refinements for Polymorphic ..."
Hole Refinements for Polymorphic Type-and-Example Driven Synthesis
Niek Mulleners, Johan Jeuring, and Wouter Swierstra
(Utrecht University, Netherlands)
Many synthesizers implicitly benefit from using polymorphic types, since parametric polymorphism reduces the search space. Additional synthesis constraints may interfere with parametricity. In particular, a polymorphic type may cause otherwise feasible input-output examples to contradict each other. We present Taxi (type-and-example based inferencer), a tool for efficiently reasoning about the feasibility of polymorphic programs specified by input-output examples, and Driver, a tactic language for top-down program synthesis that uses feasibility reasoning to prune the search space. Taxi guarantees that every search state corresponds to a correct (albeit possibly partial) implementation. In addition, it allows for shortcutting the synthesis when a subspecification covers all cases. We show that these techniques have the potential to speed up top-down enumerative type-and-example driven synthesizers.
@InProceedings{PEPM26p17,
author = {Niek Mulleners and Johan Jeuring and Wouter Swierstra},
title = {Hole Refinements for Polymorphic Type-and-Example Driven Synthesis},
booktitle = {Proc.\ PEPM},
publisher = {ACM},
pages = {17-30},
doi = {10.1145/3779209.3779535},
year = {2026},
}
Publisher's Version
PEPM '26: "Hole Refinements for Polymorphic ..."
Hole Refinements for Polymorphic Type-and-Example Driven Synthesis
Niek Mulleners, Johan Jeuring, and Wouter Swierstra
(Utrecht University, Netherlands)
Many synthesizers implicitly benefit from using polymorphic types, since parametric polymorphism reduces the search space. Additional synthesis constraints may interfere with parametricity. In particular, a polymorphic type may cause otherwise feasible input-output examples to contradict each other. We present Taxi (type-and-example based inferencer), a tool for efficiently reasoning about the feasibility of polymorphic programs specified by input-output examples, and Driver, a tactic language for top-down program synthesis that uses feasibility reasoning to prune the search space. Taxi guarantees that every search state corresponds to a correct (albeit possibly partial) implementation. In addition, it allows for shortcutting the synthesis when a subspecification covers all cases. We show that these techniques have the potential to speed up top-down enumerative type-and-example driven synthesizers.
@InProceedings{PEPM26p17,
author = {Niek Mulleners and Johan Jeuring and Wouter Swierstra},
title = {Hole Refinements for Polymorphic Type-and-Example Driven Synthesis},
booktitle = {Proc.\ PEPM},
publisher = {ACM},
pages = {17-30},
doi = {10.1145/3779209.3779535},
year = {2026},
}
Publisher's Version
PEPM '26: "Towards Lightweight and Efficient ..."
Towards Lightweight and Efficient Choreographic Cloud Services
Alex Ionescu and Alejandro Russo
(Chalmers University of Technology, Sweden; University of Gothenburg, Sweden)
Choreographic programming provides a high-level abstraction for writing distributed computations while ensuring deadlock-freedom by construction. HasChor, a Haskell-based choreographic programming framework, offers a practical implementation of these ideas but faces limitations in handling an arbitrary number of participants and optimizing the communication of branches. In this work, we introduce CloudChor, a set of extensions that enhance HasChor’s expressiveness and efficiency through the use of multiply-located values, allowing choreographies to distribute and collect data across multiple participants in a structured manner. Additionally, we refine HasChor’s branching mechanism through a lightweight static analysis, selectively propagating branching decisions only to relevant participants, reducing communication overhead. To strengthen theoretical guarantees, we establish a formal semantics for HasChor and our extensions, proving deadlock-freedom. Finally, we demonstrate the practicality of our enhancements by implementing a data clean room protocol using CloudChor. Our contributions improve the applicability of choreographic programming to cloud-based secure data collaborations, making it a stronger candidate for real-world deployments.
@InProceedings{PEPM26p45,
author = {Alex Ionescu and Alejandro Russo},
title = {Towards Lightweight and Efficient Choreographic Cloud Services},
booktitle = {Proc.\ PEPM},
publisher = {ACM},
pages = {45-60},
doi = {10.1145/3779209.3779537},
year = {2026},
}
Publisher's Version
Info
PEPM '26: "Staging Effect Handlers for ..."
Staging Effect Handlers for Modular Search
Alexandru Trifanov and Tom Schrijvers
(Independent, Romania; KU Leuven, Belgium)
Constraint Programming (CP) is a declarative paradigm where a programmer models a problem in terms of constraints over some set of variables. Monadic Constraint Programming (MCP) integrates CP with functional programming by modeling the constraint solver as a monad threaded through a monadic search tree. This abstraction allows us to define search as a first-class object which can be constructed from composable search transformers.
We introduce Effectful Constraint Programming (ECP), a re-imagining of monadic constraint programming using the increasingly-popular framework of algebraic effects and handlers. To overcome the performance drawbacks of effects, we use multi-stage programming to generate efficient search procedures from high-level, abstract descriptions.
@InProceedings{PEPM26p31,
author = {Alexandru Trifanov and Tom Schrijvers},
title = {Staging Effect Handlers for Modular Search},
booktitle = {Proc.\ PEPM},
publisher = {ACM},
pages = {31-44},
doi = {10.1145/3779209.3779536},
year = {2026},
}
Publisher's Version
PEPM '26: "Hole Refinements for Polymorphic ..."
Hole Refinements for Polymorphic Type-and-Example Driven Synthesis
Niek Mulleners, Johan Jeuring, and Wouter Swierstra
(Utrecht University, Netherlands)
Many synthesizers implicitly benefit from using polymorphic types, since parametric polymorphism reduces the search space. Additional synthesis constraints may interfere with parametricity. In particular, a polymorphic type may cause otherwise feasible input-output examples to contradict each other. We present Taxi (type-and-example based inferencer), a tool for efficiently reasoning about the feasibility of polymorphic programs specified by input-output examples, and Driver, a tactic language for top-down program synthesis that uses feasibility reasoning to prune the search space. Taxi guarantees that every search state corresponds to a correct (albeit possibly partial) implementation. In addition, it allows for shortcutting the synthesis when a subspecification covers all cases. We show that these techniques have the potential to speed up top-down enumerative type-and-example driven synthesizers.
@InProceedings{PEPM26p17,
author = {Niek Mulleners and Johan Jeuring and Wouter Swierstra},
title = {Hole Refinements for Polymorphic Type-and-Example Driven Synthesis},
booktitle = {Proc.\ PEPM},
publisher = {ACM},
pages = {17-30},
doi = {10.1145/3779209.3779535},
year = {2026},
}
Publisher's Version
PEPM '26: "Staging Effect Handlers for ..."
Staging Effect Handlers for Modular Search
Alexandru Trifanov and Tom Schrijvers
(Independent, Romania; KU Leuven, Belgium)
Constraint Programming (CP) is a declarative paradigm where a programmer models a problem in terms of constraints over some set of variables. Monadic Constraint Programming (MCP) integrates CP with functional programming by modeling the constraint solver as a monad threaded through a monadic search tree. This abstraction allows us to define search as a first-class object which can be constructed from composable search transformers.
We introduce Effectful Constraint Programming (ECP), a re-imagining of monadic constraint programming using the increasingly-popular framework of algebraic effects and handlers. To overcome the performance drawbacks of effects, we use multi-stage programming to generate efficient search procedures from high-level, abstract descriptions.
@InProceedings{PEPM26p31,
author = {Alexandru Trifanov and Tom Schrijvers},
title = {Staging Effect Handlers for Modular Search},
booktitle = {Proc.\ PEPM},
publisher = {ACM},
pages = {31-44},
doi = {10.1145/3779209.3779536},
year = {2026},
}
Publisher's Version
PEPM '26: "Inferring Typing Rules for ..."
Inferring Typing Rules for Contextual Sugars
Tailai Yu, Zhichao Guan, Di Wang, and Zhenjiang Hu
(Peking University, China)
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.
@InProceedings{PEPM26p61,
author = {Tailai Yu and Zhichao Guan and Di Wang and Zhenjiang Hu},
title = {Inferring Typing Rules for Contextual Sugars},
booktitle = {Proc.\ PEPM},
publisher = {ACM},
pages = {61-75},
doi = {10.1145/3779209.3779538},
year = {2026},
}
Publisher's Version
PEPM '26: "Revisiting the Evolution of ..."
Revisiting the Evolution of Effects (Invited Talk)
Nicolas Wu
(Imperial College London, UK)
Functional programming is often associated with pure functions, offering referential transparency and a principled basis for reasoning about programs. In practice, however, most programs must interact with their environment, introducing effects such as input/output, mutable state, and exceptions. Reconciling these requirements with purity has been a longstanding concern in the design of functional languages.
Monads provided an early and influential approach, offering a disciplined way to sequence effectful computations while retaining a pure core. Although successful, this approach exposed limitations in modularity: combining multiple effects in a flexible manner proved difficult. Monad transformers addressed this to some extent by allowing effects to be layered.
More recent work has explored algebraic effects as an alternative framework, supporting extensibility and a more modular treatment of effects, particularly in the construction of domain-specific abstractions. Experience with algebraic effects has, in turn, revealed limitations of first-order formulations, motivating the development of scoped and higher-order effects. These extensions broaden the range of effectful behaviour that can be expressed, and help clarify the relationship between monadic and algebraic approaches.
This talk revisits these developments, following the evolution from monads and monad transformers to algebraic and higher-order effects, and discussing the trade-offs that arise in structuring effectful programs.
@InProceedings{PEPM26p1,
author = {Nicolas Wu},
title = {Revisiting the Evolution of Effects (Invited Talk)},
booktitle = {Proc.\ PEPM},
publisher = {ACM},
pages = {1-1},
doi = {10.1145/3779209.3787154},
year = {2026},
}
Publisher's Version
PEPM '26: "Inferring Typing Rules for ..."
Inferring Typing Rules for Contextual Sugars
Tailai Yu, Zhichao Guan, Di Wang, and Zhenjiang Hu
(Peking University, China)
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.
@InProceedings{PEPM26p61,
author = {Tailai Yu and Zhichao Guan and Di Wang and Zhenjiang Hu},
title = {Inferring Typing Rules for Contextual Sugars},
booktitle = {Proc.\ PEPM},
publisher = {ACM},
pages = {61-75},
doi = {10.1145/3779209.3779538},
year = {2026},
}
Publisher's Version