Programming with algebraic effects and handlers
From MaRDI portal
Publication:478396
DOI10.1016/j.jlamp.2014.02.001zbMath1304.68025arXiv1203.1539OpenAlexW3103594074WikidataQ115902568 ScholiaQ115902568MaRDI QIDQ478396
Publication date: 3 December 2014
Published in: Journal of Logical and Algebraic Methods in Programming (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1203.1539
Theory of programming languages (68N15) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Related Items
Continuity of Gödel's system T definable functionals via effectful forcing ⋮ Explicit effect subtyping ⋮ Runners in Action ⋮ Introducing \(\llparenthesis\lambda\rrparenthesis\), a \(\lambda \)-calculus for effectful computation ⋮ A Functional Abstraction of Typed Invocation Contexts ⋮ Factorisation systems for logical relations and monadic lifting in type-and-effect system semantics ⋮ Turing-Completeness Totally Free ⋮ When programs have to watch paint dry ⋮ Efficient algebraic effect handlers for Prolog ⋮ Sound and complete type inference for closed effect rows ⋮ Effect handlers via generalised continuations ⋮ Effekt: Capability-passing style for type- and effect-safe, extensible effect handlers in Scala ⋮ Doo bee doo bee doo ⋮ Structured handling of scoped effects ⋮ Automated temporal verification for algebraic effects ⋮ Verifying an Effect-Handler-Based Define-By-Run Reverse-Mode AD Library ⋮ Local algebraic effect theories ⋮ Interactive programming in Agda – Objects and graphical user interfaces ⋮ No value restriction is needed for algebraic effects and handlers ⋮ Mac Lane's comparison theorem for the Kleisli construction formalized in Coq ⋮ Unnamed Item ⋮ An introduction to algebraic effects and handlers (invited tutorial paper) ⋮ Validating Brouwer's continuity principle for numbers using named exceptions ⋮ Modular verification of programs with effects and effects handlers ⋮ Modular verification of programs with effects and effect handlers in Coq ⋮ Unnamed Item ⋮ Eff ⋮ Introducing a Calculus of Effects and Handlers for Natural Language Semantics ⋮ Continuation passing style for effect handlers ⋮ Not by equations alone: Reasoning with extensible effects
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- A new approach to abstract syntax with variable binding
- Combining algebraic effects with continuations
- A theory of type polymorphism in programming
- Modelling environments in call-by-value programming languages.
- Algebraic operations and generic effects
- Combining effects: sum and tensor
- Selection functions, bar recursion and backward induction
- Handlers of Algebraic Effects
- Representing Control: a Study of the CPS Transformation
- Tensors of Comodels and Models for Operational Semantics
- An introduction to algebraic effects and handlers (invited tutorial paper)