25 citations · 210 across the 59 of their papers we have counts for
11 papers · 1 filter
Hilbert-Post completeness for the state and the exception effects
Jean-Guillaume Dumas, Dominique Duval, Burak Ekici +2
In this paper, we present a novel framework for studying the syntactic completeness of computational effects and we apply it to the exception effect. When applied to the states eff…
Program certification with computational effects
Jean-Guillaume Dumas, Dominique Duval, Burak Ekici +1
Dynamic evaluation is a paradigm in computer algebra which was introduced for computing with algebraic numbers. In linear algebra, for instance, dynamic evaluation can be used to a…
Breaking a monad-comonad symmetry between computational effects
Jean-Guillaume Dumas, Dominique Duval, Jean-Claude Reynaud
Computational effects may often be interpreted in the Kleisli category of a monad or in the coKleisli category of a comonad. The duality between monads and comonads corresponds, in…
Formal verification in Coq of program properties involving the global state effect
Jean-Guillaume Dumas, Dominique Duval, Burak Ekici +1
The syntax of an imperative language does not mention explicitly the state, while its denotational semantics has to mention it. In this paper we present a framework for the verific…
Patterns for computational effects arising from a monad or a comonad
Jean-Guillaume Dumas, Dominique Duval, Jean-Claude Reynaud
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…
Certified proofs in programs involving exceptions
Jean-Guillaume Dumas, Dominique Duval, Burak Ekici +1
Exception handling is provided by most modern programming languages. It allows to deal with anomalous or exceptional events which require special processing. In computer algebra, e…
Adjunctions for exceptions
Jean-Guillaume Dumas, Dominique Duval, Laurent Fousse +1
An algebraic method is used to study the semantics of exceptions in computer languages. The exceptions form a computational effect, in the sense that there is an apparent mismatch…
Decorated proofs for computational effects: Exceptions
Jean-Guillaume Dumas, Dominique Duval, Laurent Fousse +1
We define a proof system for exceptions which is close to the syntax for exceptions, in the sense that the exceptions do not appear explicitly in the type of any expression. This p…
A duality between exceptions and states
Jean-Guillaume Dumas, Dominique Duval, Laurent Fousse +1
In this short note we study the semantics of two basic computational effects, exceptions and states, from a new point of view. In the handling of exceptions we dissociate the contr…
States and exceptions considered as dual effects
Jean-Guillaume Dumas, Dominique Duval, Laurent Fousse +1
In this paper we consider the two major computational effects of states and exceptions, from the point of view of diagrammatic logics. We get a surprising result: there exists a sy…
Cartesian effect categories are Freyd-categories
Jean-Guillaume Dumas, Dominique Duval, Jean-Claude Reynaud
Most often, in a categorical semantics for a programming language, the substitution of terms is expressed by composition and finite products. However this does not deal with the or…