Effect categories and COQ

Proving properties of programs involving computational effects.

[Recent Talks] [Papers] [Code] [Contacts]

[Recent Talks]

Jean-Guillaume Dumas   Program certification with computational effects. Burak Ekici.
JNCF 2014 : Journées Nationales de Calcul Formel, Marseille, France, 5 November 2014.
Jean-Guillaume Dumas   The art of lying, with the proof assistant Coq. Dominique Duval.
IFIP WG1.3 : Foundations of System Specification, Sinaia, Romania, 3 September 2014.
Jean-Guillaume Dumas   Certification of programs with computational effects. Burak Ekici.
CICM 2014 -- Doctoral Session : The eighth Eigth Conference on Intelligent Computer Mathematics, Coimbra, Portugal, 11 July 2014.
Jean-Guillaume Dumas   Certified proofs in programs involving exceptions. Jean-Guillaume Dumas.
CICM 2014 : The eighth Eigth Conference on Intelligent Computer Mathematics, Coimbra, Portugal, 9 July 2014.
Jean-Guillaume Dumas   Formal verification in Coq of program properties involving the global state effect. Burak Ekici.
JFLA 2014 : Journées Francophones des Langages Applicatifs, Fréjus, France, 9 January 2014.
Jean-Guillaume Dumas   Formal verification in Coq of program properties involving the global state effect. Burak Ekici.
Séminaires LJK-Modèles et Algorithmes Déterministes : BIPOP-CASYS, Grenoble, France, 5 December 2013.

[Papers]

Jean-Guillaume Dumas   Program certification with computational effects. Jean-Guillaume Dumas, Dominique Duval, Burak Ekici and Damien Pous.
JNCF 2014 : Journées Nationales de Calcul Formel, Marseille, France, 3--7 November 2014, arXiv : cs.LO/1411.7140.
Jean-Guillaume Dumas   Certification of programs with computational effects. Burak Ekici.
CICM 2014 -- Doctoral Session : The eighth Eigth Conference on Intelligent Computer Mathematics, Coimbra, Portugal, 7--11 July 2014, arXiv : cs.LO/1411.7139.
Jean-Guillaume Dumas   Certified proofs in programs involving exceptions. Jean-Guillaume Dumas, Dominique Duval, Burak Ekici and Jean-Clauede Reynaud.
CICM 2014 : The eighth Eigth Conference on Intelligent Computer Mathematics, Coimbra, Portugal, 7--11 July 2014,
CEUR Workshop Proceedings
, no 1186, paper 20.
Jean-Guillaume Dumas   Formal verification in Coq of program properties involving the global state effect. Jean-Guillaume Dumas, Dominique Duval, Burak Ekici and Damien Pous.
JFLA 2014 : Journées Francophones des Langages Applicatifs, pages 1--15, Fréjus, France, 8--11 January 2014. IMAG-hal-00869230, arXiv : cs.LO/1310.0794.
Associated Coq proof verification of decorated Hilbert-Post completeness of the global state effect.
Jean-Guillaume Dumas   Patterns for computational effects arising from a monad or a comonad. Jean-Guillaume Dumas, Dominique Duval et Jean-Claude Reynaud.
Rapport de Recherche IMAG-hal-00868831, arXiv : cs.LO/1310.0605. Octobre 2013. France.
Jean-Guillaume Dumas   A duality between exceptions and states. Jean-Guillaume Dumas, Dominique Duval, Laurent Fousse et Jean-Claude Reynaud.
Mathematical Structures in Computer Science, Volume 22, issue 4, p 719--722, août 2012.
Jean-Guillaume Dumas   Decorated proofs for computational effects: States. Jean-Guillaume Dumas, Dominique Duval, Laurent Fousse et Jean-Claude Reynaud.
ACCAT 2012 : 7th Applied and Computational Category Theory (part of ETAPS 2012), Tallinn, Estonie, 24 Mars -- 1 Avril 2012.
Electronic Proceedings in Theoretical Computer Science. Volume 93, p 45--59, août 2012.
Jean-Guillaume Dumas   Adjunctions for exceptions. Jean-Guillaume Dumas, Dominique Duval, Laurent Fousse et Jean-Claude Reynaud.
Rapport de Recherche IMAG-hal-00714710, arXiv: cs.LO/1207.1255. Juin 2012. France.
Jean-Guillaume Dumas   A parameterization process: from a functorial point of view. César Dominguez, Dominique Duval.
International Journal of Foundations of Computer Science (IJFCS) 23 p.225-242 (2012).
Jean-Guillaume Dumas   Cartesian effect categories are Freyd-categories. Jean-Guillaume Dumas, Dominique Duval et Jean-Claude Reynaud.
Journal of Symbolic Computations. Volume 46, issue 3, p 272--293, mars 2011.
Jean-Guillaume Dumas   Diagrammatic logic applied to a parameterization process. César Dominguez, Dominique Duval.
Mathematical Structures in Computer Science 20(04) p. 639-654 (2010). Cambridge University Press.
Jean-Guillaume Dumas   Towards a diagrammatic modeling of the LinBox C++ linear algebra library. Jean-Guillaume Dumas et Dominique Duval.
LMO'2006 : Langages et Modèles à Objets, 22-24 Mars 2006, Nîmes, France.

[Source Code]

Source codes are available on the forge: coqeffects (Last update: Monday, March 2nd 2015

[Contacts]

Jean-Guillaume Dumas
Université de Grenoble, Laboratoire Jean Kuntzmann
B.P. 53X -- 51, av. des Mathématiques, 38041 Grenoble, France.
http://ljk.imag.fr/membres/Jean-Guillaume.Dumas
Dominique Duval
Université de Grenoble, Laboratoire Jean Kuntzmann
B.P. 53X -- 51, av. des Mathématiques, 38041 Grenoble, France
http://ljk.imag.fr/membres/Dominique.Duval
Burak Ekici
Université de Grenoble, Laboratoire Jean Kuntzmann
B.P. 53X -- 51, av. des Mathématiques, 38041 Grenoble, France.
http://ljk.imag.fr/membres/Burak.Ekici
Laurent Fousse
Google
1600 Amphitheatre Parkway, Mountain View, CA 94043, USA
http://komite.net/laurent/pro
Damien Pous
CNRS, ENS Lyon
LIP, ENS Lyon, 46 allee d'Italie, 69364 Lyon, France
http://perso.ens-lyon.fr/damien.pous/
Jean-Claude Reynaud
Reynaud Consulting
38640 Claix, France.