HOPE 2023
as the organisers put it
Workshop The HOPE workshop series are intended to bring together researchers interested in the design, semantics, implementation, and verification of higher-order effectful programs. They are informal, consisting of invited talks, contributed talks on work in progress, and open-ended discussion sessions. They are dedicated to John Reynolds, whose work is an inspiration to us all. The 11th ACM SIGPLAN Workshop on Higher-Order Programming with Effects will take place on Monday, September 4, 2023, that is, the day before ICFP 2023. Goals of the Workshop A recurring theme in many papers at ICF ...
who it's for
programming language researchers, language designers, programming language implementers, type system researchers, compiler engineers, formal methods engineers, verification tool developers, distributed systems researchers
topics
algebraic effects and handlers; dynamic effect instances; operational game semantics; closure conversion and predicative references; CPS weakest-precondition transformation; flow-sensitive effect typing; multiparty session actors; HORPO termination for effects; coexponentials for continuations; join-as-semilattice parallelism; potential-synthesis for amortised cost; free variables as effects and wasm/x86 backend
| title | author | length |
|---|---|---|
| One Weird Trick to Untie Landin's Knot | Paulette Koronkevich, William J. Bowman | 28m |
Claim: Landin’s Knot arises from impredicative quantification over a function’s closure environment, not merely from storing functions in refs. Method: perform… | ||
| Operational game semantics for generative algebraic effects and handlers | Hamza Jaâfar, Guilhem Jaber | 30m |
Claims a trace-based operational game semantics for a typed call-by-value λ-calculus with algebraic effects, handlers and dynamic effect instances (new creates… | ||
| Higher-Order Weakest Precondition Transformers via a CPS Transformation | Satoshi Kura | 29m |
Claims that generic weakest preconditions for a higher‑order language with effects and recursion are computable syntactically by a CPS transformation, using… | ||
| Event-Driven Multiparty Session Actors | Simon Fowler, Raymond Hu | 35m |
Claims a first statically-typed multiparty session system for actors that lets a single actor participate in multiple sessions by combining flow-sensitive… | ||
| Flattening Meets Effects: A Surprising Connection | Ezra e. k. Cooper | 35m |
Claims a concrete link between algebraic-effects metal language and term-rewriting termination techniques, showing HORPO-style ordering can be extended to… | ||
| Continuations and Coexponentials | Vikraman Choudhury | 30m |
Proposes that higher-order continuations are categorical coexponentials and shows how the continuation monad and a full-image factorization of negation produce… | ||
| Granite: Compositional Functional Logic Programming | Nick Rioux, Steve Zdancewic | 32m |
Granite puts a join as semilattice primitive at the language core, letting parallel executions merge by associative commutative idempotent joins; it encodes… | ||
| Semantic foundations of potential-synthesis for expected amortised-cost analysis | Ohad Kammar, Georg Moser | 20m |
Ongoing work builds a semantic stack that synthesises potential functions for randomized data structures and guarantees amortised-cost bounds correct by… | ||
| Free Variable as Effect, in Practice | Oleg Kiselyov | 32m |
Proposes that treating free variables as algebraic effects gives practical wins: a tagless-final compiler prototype emits runnable wasm module and x86 code… | ||
| nothing matches | ||