HOPE 2022
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 10th ACM SIGPLAN Workshop on Higher-Order Programming with Effects will take place on Sunday, September 11, 2022, that is, the day before ICFP 2022. Goals of the Workshop A recurring theme in many papers at IC ...
who it's for
programming language researchers, semantics researchers, language designers, compiler engineers, formal verification engineers, effect systems researchers, functional programmers
topics
Call-By-Push-Value with fixpoint; temporal refinements and modalities; comonadic box modality; later modality for liveness; relative monads in CBPV; stack-based effects encoding; F* IO for nonterminating programs; specification monad with infinite traces; stochastic memoization model; commutative semicartesian probability monad; lift inference for lexical effect handlers; flexibly graded monads and graded algebras
| title | author | length |
|---|---|---|
| Temporal refinements for Call-By-Push-Value with fixpoint | Guilhem Jaber, Kenji Maillard, Colin Riba | 26m |
Proposes temporal refinements for a Call-By-Push-Value calculus with arbitrary fixpoints and shows how a comonadic modality (a box) plus a later modality… | ||
| Relative Monads in CBPV for Stack-based Effects | Max S. New | 25m |
Claim: modeling stack-based implementations of effects uses relative monad structure inside Call-by-push-value (CBPV), not ordinary endo-monads. Uses CBPV’s… | ||
| Verifying non-terminating programs with IO in F* | Cezar-Constantin Andrici, Théo Winterhalter, Cătălin Hriţcu, Exequiel Rivas | 19m |
Defines an F effect that specifies IO for both terminating and potentially non-terminating programs, implements an example echo server and most of a simple web… | ||
| Higher order programming with probabilistic effects: A model of stochastic memo... | Younesse Kaddar, Sam Staton | 24m |
Claims a concrete categorical model that makes stochastic memoization respect the crucial dataflow property while keeping higher-order functions by building a… | ||
| Lift Inference for Lexical Effect Handlers with Second-Class Functions | Marius Müller, Philipp Schuster, Jonathan Immanuel Brachthäuser, Klaus Ostermann | 21m |
Presents an algorithm that infers lifting information for lexical effect handlers by translating System Xi (with second-class functions) into Lambda_cap with… | ||
| Flexibly graded monads and graded algebras | Dylan McDermott, Tarmo Uustalu | 21m |
Defines flexibly graded monad as a monad on graded sets (results may carry grades), proves no ordinary graded monad can have algebras exactly equal to graded… | ||
| Lift Inference for Lexical Effect Handlers with Second-Class Functions | Marius Müller, Philipp Schuster, Jonathan Immanuel Brachthäuser, Klaus Ostermann | 21m |
Claims a concrete compiler pass that infers lifting information for a core language with second‑class functions and emits explicit region evidence so lexical… | ||
| nothing matches | ||