Related papers: A Recipe for State-and-Effect Triangles
This paper describes how to verify a parser for regular expressions in a functional programming language using predicate transformer semantics for a variety of effects. Where our previous work in this area focused on the semantics for a…
Type-and-effect systems incorporate information about the computational effects, e.g., state mutation, probabilistic choice, or I/O, a program phrase may invoke alongside its return value. A semantics for type-and-effect systems involves a…
Free monads (and their variants) have become a popular general-purpose tool for representing the semantics of effectful programs in proof assistants. These data structures support the compositional definition of semantics parameterized by…
This paper gives a systematic account of various metrics on probability distributions (states) and on predicates. These metrics are described in a uniform manner using the validity relation between states and predicates. The standard…
We introduce an extension of first-order logic that comes equipped with additional predicates for reasoning about an abstract state. Sequents in the logic comprise a main formula together with pre- and postconditions in the style of Hoare…
We show how to smoothly incorporate in the object-oriented paradigm constructs to raise, compose, and handle effects in an arbitrary monad. The underlying pure calculus is meant to be a representative of the last generation of OO languages,…
Monads govern computational side-effects in programming semantics. They can be combined in a ''bottom-up'' way to handle several instances of such effects. Indexed monads and graded monads do this in a modular way. Here, instead, we equip…
In functional programming, monads are supposed to encapsulate computations, effectfully producing the final result, but keeping to themselves the means of acquiring it. For various reasons, we sometimes want to reveal the internals of a…
One can perform equational reasoning about computational effects with a purely functional programming language thanks to monads. Even though equational reasoning for effectful programs is desirable, it is not yet mainstream. This is partly…
Type systems designed for information-flow control commonly use a program-counter label to track the sensitivity of the context and rule out data leakage arising from effectful computation in a sensitive context. Currently, type-system…
We show that state, reader, writer, and error monad transformers are instances of one general categorical construction: translation of a monad along an adjunction.
Sequential effect systems are a class of effect system that exploits information about program order, rather than discarding it as traditional commutative effect systems do. This extra expressive power allows effect systems to reason about…
We introduce the abstract notions of "monadic operational semantics", a small-step semantics where computational effects are modularly modeled by a monad, and "type-and-effect system", including "effect types" whose interpretation lifts…
Monads are a popular tool for the working functional programmer to structure effectful computations. This paper presents polymonads, a generalization of monads. Polymonads give the familiar monadic bind the more general type forall a,b. L a…
A new categorical framework is provided for dealing with multiple arguments in a programming language with effects, for example in a language with imperative features. Like related frameworks (Monads, Arrows, Freyd categories), we…
This paper presents equational-based logics for proving first order properties of programming languages involving effects. We propose two dual inference system patterns that can be instanciated with monads or comonads in order to be used…
We present the syntax and rules of deduction of QPEL (Quantum Program and Effect Language), a language for describing both quantum programs, and properties of quantum programs - effects on the appropriate Hilbert space. We show how…
Recent advances in programming languages study and design have established a standard way of grounding computational systems representation in category theory. These formal results led to a better understanding of issues of control and…
Wadler and Thiemann unified type-and-effect systems with monadic semantics via a syntactic correspondence and soundness results with respect to an operational semantics. They conjecture that a general, "coherent" denotational semantics can…
In these lecture notes, we give a brief introduction to some elements of category theory. The choice of topics is guided by applications to functional programming. Firstly, we study initial algebras, which provide a mathematical…