HOPE 2025
who it's for
programming language researchers, language designers, type theorists, compiler engineers, functional programmers, formal methods researchers, PL tool and runtime implementers
topics
effectful lenses and polymonads; selection monad in handlers; algebraic effect handlers for optimisation; contraction-based region collapsing; region and effect inference for ReML; soundness for SSA refinements; directed substructural effect systems; graded effects with relevance types; finite-support relations for Datalog-style tables; modal encodings of rows and capabilities
| title | author | length |
|---|---|---|
| Compositions for Free: Reasoning about Effectful Lenses | Ruifeng Xie, Tom Schrijvers, Zhenjiang Hu | 21m |
Presents a construction that composes two different monads into a free polymonad so effects run in two staged layers and most roundtrip laws become theorems… | ||
| Smart Handlers: Handling the selection monad | Ningning Xie | 01h 17m |
Introduces selection monad ideas into algebraic effect handlers to add choice continuations that compute future losses; prototypes in a Haskell-like Huscoll… | ||
| Contractions Are Abstractions - Towards Effective Memory Management in ReML | Martin Elsman | 37m |
Work in progress extends ReML and the MLKit region/effect inference backend to let programmers write abstract region annotations that map to many concrete… | ||
| Sound and Complete Refinement for SSA with Substructural Effects | Jad Elkhaleq Ghalayini, Neel Krishnaswami | 36m |
A denotational model for SSA is given and a syntactic refinement relation is defined that is proven sound and complete against postset-enriched categories, so… | ||
| Finite functional programming via graded effects and relevance types | Michael Arntzenius | 49m |
Proposes treating relations as functions equipped with their support so Datalog-style relations become finitely supported maps that can be represented as… | ||
| Rows and Capabilities as Modal Effects | Wenhao Tang, Sam Lindley | 55m |
Effect systems for handlers get a concrete bridge: a multimodal target MX encodes Koka-style row effects by translating each annotated arrow to an absolute… | ||
| nothing matches | ||