9 citations · 31 across the 12 of their papers we have counts for
12 papers
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…
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…
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…