978 citations
- Centre National de la Recherche ScientifiqueFR196 papers
- Université Grenoble AlpesFR195 papers
- Institut national de recherche en sciences et technologies du numériqueFR115 papers
- Institut polytechnique de GrenobleFR93 papers
- Centre Inria de l'Université Grenoble AlpesFR78 papers
- Université Joseph FourierFR33 papers
- Pôle de recherche et d'enseignement supérieur Université de GrenobleFR22 papers
- Georgia Institute of TechnologyUS18 papers
- Laboratoire d'Informatique de GrenobleFR16 papers
- GIPSA-LabFR15 papers
- THOTH: Apprentissage de modèles visuels à partir de données massivesFR11 papers
- École PolytechniqueFR9 papers
15 papers · 1 filter
A Rule-based Operational Semantics of Graph Query Languages
Dominique Duval, Rachid Echahed, Frederic Prost
We consider a core language of graph queries. These queries are seen as formulas to be solved with respect to graph-oriented databases. For this purpose, we first define a graph qu…
Logical rules as fractions and logics as sketches
Dominique Duval
In this short paper, using category theory, we argue that logical rules can be seen as fractions and logics as limit sketches.
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…
Certification of programs with computational effects
Burak Ekici
In purely functional programming languages imperative features, more generally computational effects are prohibited. However, non-functional lan- guages do involve effects. The the…
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…