PEPM 2026
who it's for
programming language researchers, compiler and tool implementers, language designers, formal methods researchers, runtime engineers, dsl designers, software verification engineers
topics
choreographic cloud services; multiply-located values; scatter/gather choreography operators; putback-based bidirectional transformations; update-based edit lenses; partial evaluation for networks; algebraic effects and handlers; staging effect handlers; S4 modal sequent calculus; typing inference for contextual sugars; Python-to-SMT staged execution
| title | author | length |
|---|---|---|
| Towards Lightweight and Efficient Choreographic Cloud Services | Alex Ionescu, Alejandro Russo | 22m |
Extensions to HasChor called CloudChor add concrete primitives: multiply-located values (a type-level list + np proxies), scatter/gather operators and a… | ||
| Incrementalizing Haskell implementation of Putback-based Bidirectional Transformation(…) | Masaki Toyoda, Soichiro Hidaka | 18m |
Claims an update-based BiGUL (BigDelta) implemented in Haskell that replaces state-by-state propagation with edit operations adapted from X and Edit Lenses… | ||
| Partial Evaluation as a primitive in modern network troubleshooting (Talk Proposal) | Anduo Wang | 21m |
Partial evaluation compresses real network instances into a smaller residual network by compiling away SDN for-log conditions, BGP path computation, or INC… | ||
| Towards Cumulative Abstract Semantics via Handlers (Short Paper) | Cade Lueker, Andrew Fox, Bor-Yuh Evan Chang | 14m |
Proposes using algebraic effects to separate value creation and control flow: implement domain-specific introduction handlers (concrete ints, intervals with… | ||
| Hole Refinements for Polymorphic Type-and-Example Driven Synthesis | Niek Mulleners, Johan Jeuring, Wouter Swierstra | 32m |
Toolchain combines a parametricity-aware feasibility reasoner and a tactic-driven synthesizer: Taxi computes polymorphic input–output normal forms and… | ||
| S4 modal sequent calculus as intermediate logic and intermediate language (Short Paper) | Jean Caspar, Guillaume Munch-Maccagnoni | 16m |
Claims that second-class continuations correspond to a restricted S4 modal fragment where implications may only return modal types, and that this fragment sits… | ||
| Epistemic Logic for Polyglots (Short Paper) | Luis Garcia, Chris Martens | 18m |
Proposes using epistemic S4 modal logic as a propositions-as-types foundation for polyglot programs, mapping agents to languages and deriving a glue calculus… | ||
| Inferring Typing Rules for Contextual Sugars | Tailai Yu, Zhichao Guan, Di Wang, Zhenjiang Hu | 30m |
Algorithm infers typing rules for a class of contextual sugars by fusing sugaring rules with core-language typing and by performing early typing of templates… | ||
| Retargeting an Abstract Interpreter for a New Language by Partial Evaluation (Short Paper) | Jay Lee, Joongwon Ahn, Kwangkeun Yi | 09m |
Claims that partially evaluating a sound abstract interpreter for S with a definitional interpreter for T yields a sound abstract interpreter for T, and… | ||
| Holey: Staged Execution from Python to SMT (Talk Proposal) | Nada Amin | 22m |
Holey is a Python library that stages satisfiability predicates to SMT by dynamic operator overloading and light AST rewriting, emits portable SMT‑LIB, swaps… | ||
| Computation-Tree Semantics: An Algorithmic Approach to Structurally Defined Relations | Sean Kristian Remond Harbo, Hans Hüttel | 30m |
Proposes Computation-Tree Semantics where configurations are trees that encode evaluation contexts and continuations, making semantic rules algorithmic rather… | ||
| Revisiting the Evolution of Effects (Invited Talk) | Nicolas Wu | 54m |
Traces the technical line from monads through monad transformers to algebraic and higher‑order effects, arguing concrete tradeoffs: monads sequence effects but… | ||
| Staging Effect Handlers for Modular Search | Alexandru Trifanov, Tom Schrijvers | 29m |
Recasts monadic constraint programming as an algebraic effect handlers design where models are free‑monad effectful computations and solvers are handlers… | ||
| nothing matches | ||