HOPE 2024
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 12th ACM SIGPLAN Workshop on Higher-Order Programming with Effects will take place on Monday, September 2, 2024, that is, the day before ICFP 2024. Goals of the Workshop A recurring theme in many papers at ICF ...
who it's for
programming language researchers, functional programming researchers, type system designers, proof engineers and mechanizers, compiler and language implementers, systems security researchers
topics
Dijkstra monads for capabilities; capability enforcement in F*; mechanized monadic reasoning; ML references equational theory; arrows as applicatives; algebraic effects with parameters; delimited-effect handlers implementation; AsmFX assembly effect handlers; linear translation of Rust borrows; incremental borrow calculus; contextual distance amplification; clocked guarded domain theory
| title | author | length |
|---|---|---|
| Modularizing Reasoning about AI Capabilities via Abstract Dijkstra Monads | Cyrus Omar, Patrick Ferris, Anil Madhavapeddy | 36m |
Position proposes a Bastion OS design that uses Dijkstra monads and secIO in F to enforce capability-based, provable constraints on agent actions. Concrete… | ||
| Mechanized monadic equational reasoning for ML references | Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa | 29m |
Extends a Coq mechanization by adding a typed store monad and a bespoke equational theory for ML references, implemented on top of the Mona library and a… | ||
| Arrows as applicatives in a monad | Leo White | 29m |
Argues that arrows are essentially applicatives with sharing and gives a concrete API: a Node type with an applicative interface whose map returns inside a… | ||
| Paella: algebraic effects with parameters and their handlers | Jesse Sigal, Ohad Kammar, Cristina Matache, Conor McBride | 29m |
Library implements algebraic effects as computation trees indexed by worlds, claiming handlers that safely support dynamically allocated full ground reference… | ||
| Logical Relations for Effect Capabilities | Patrycja Balik, Piotr Polesiuk | 29m |
A calculus of effect capabilities appears with an operational translation that generates runtime labels and labeled effects and captures continuations up to… | ||
| Effectful Assembly Programming with AsmFX | Brian Campbell, Sam Lindley, Wilmer Ricciotti, Ian Stark | 31m |
AsmFX proposes a six‑instruction extension (enter, do, return, exit, resume, break) plus re-enter/final-re-enter and shallow variants to implement effect… | ||
| Towards a linear functional translation for borrowing | Sidney Congard | 31m |
Claims a mechanical translation from Rust mutable borrows to a pure linear functional program that preserves Rust’s linearity guarantees and relies on existing… | ||
| An Incremental Approach to the Semantics of Borrowing | Brianna Marshall, Andrew Wagner, John Li, Olek Gierczak, Amal Ahmed | 31m |
Presents a core, extensible borrow calculus built incrementally: start from a linear call-by-push-value core, add immutable borrows, lifetimes, mutable… | ||
| Amplifying Contextual Distance in Higher-Order Languages, using the Law of Large Numbers | Raphaëlle Crubillé, Houssein Mansour | 29m |
Claim: contextual distance in a probabilistic higher-order language where every program terminates with probability 1 collapses to 0 or 1. Proof builds… | ||
| An introduction to synthetic guarded domain theory with applications to probabilistic(…) | Rasmus Ejlers Møgelberg | 01h 07m |
Presents a clocked cubical type theory metalanguage that uses a guarded delay monad to define both big‑step operational and denotational semantics for FPC and… | ||
| nothing matches | ||