142 citations · 367 across the 12 of their papers we have counts for
13 papers
Simplifying explicit subtyping coercions in a polymorphic calculus with effects
Filip Koprivec, Matija Pretnar
Algebraic effect handlers are becoming an increasingly popular way of structuring effectful computations, and their performance is often a concern. One of the proposed approaches t…
Wasm SpecTec: Engineering a Formal Language Standard
Joachim Breitner, Philippa Gardner, Jaehyun Lee +8
WebAssembly (Wasm) is a low-level bytecode language and virtual machine, intended as a compilation target for a wide range of programming languages, which is seeing increasing adop…
Higher-Order Asynchronous Effects
Danel Ahman, Matija Pretnar
We explore asynchronous programming with algebraic effects. We complement their conventional synchronous treatment by showing how to naturally also accommodate asynchrony within th…
Explicit Effect Subtyping
Georgios Karachalias, Matija Pretnar, Amr Hany Saleh +2
As popularity of algebraic effects and handlers increases, so does a demand for their efficient execution. Eff, an ML-like language with native support for handlers, has a subtypin…
Local Algebraic Effect Theories
Žiga Lukšič, Matija Pretnar
Algebraic effects are computational effects that can be described with a set of basic operations and equations between them. As many interesting effect handlers do not respect thes…
Asynchronous Effects
Danel Ahman, Matija Pretnar
We explore asynchronous programming with algebraic effects. We complement their conventional synchronous treatment by showing how to naturally also accommodate asynchrony within th…
Design and Implementation of the Andromeda Proof Assistant
Andrej Bauer, Gaëtan Gilbert, Philipp G. Haselwarter +2
Andromeda is an LCF-style proof assistant where the user builds derivable judgments by writing code in a meta-level programming language AML. The only trusted component of Andromed…
On the Expressive Power of User-Defined Effects: Effect Handlers, Monadic Reflection, Delimited Control
Yannick Forster, Ohad Kammar, Sam Lindley +1
We compare the expressive power of three programming abstractions for user-defined computational effects: Bauer and Pretnar's effect handlers, Filinski's monadic reflection, and de…
No value restriction is needed for algebraic effects and handlers
Ohad Kammar, Matija Pretnar
We present a straightforward, sound Hindley-Milner polymorphic type system for algebraic effects and handlers in a call-by-value calculus, which allows type variable generalisation…
Handling Algebraic Effects
Gordon D Plotkin, Matija Pretnar
Algebraic effects are computational effects that can be represented by an equational theory whose operations produce the effects at hand. The free model of this theory induces the…
Inferring Algebraic Effects
Matija Pretnar
We present a complete polymorphic effect inference algorithm for an ML-style language with handlers of not only exceptions, but of any other algebraic effect such as input & output…
An Effect System for Algebraic Effects and Handlers
Andrej Bauer, Matija Pretnar
We present an effect system for core Eff, a simplified variant of Eff, which is an ML-style programming language with first-class algebraic effects and handlers. We define an expre…
Programming with Algebraic Effects and Handlers
Andrej Bauer, Matija Pretnar
Eff is a programming language based on the algebraic approach to computational effects, in which effects are viewed as algebraic operations and effect handlers as homomorphisms fro…