Effect categories and COQ

[Talks]

	Program certification with computational effects. Burak Ekici. JNCF 2014 : Journées Nationales de Calcul Formel, Marseille, France, 5 November 2014.
	The art of lying, with the proof assistant Coq. Dominique Duval. IFIP WG1.3 : Foundations of System Specification, Sinaia, Romania, 3 September 2014.
	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.
	Certified proofs in programs involving exceptions. Jean-Guillaume Dumas. CICM 2014 : The eighth Eigth Conference on Intelligent Computer Mathematics, Coimbra, Portugal, 9 July 2014.
	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.
	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]

	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.
	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.
	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.
	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.
	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.
	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.
	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.
	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.
	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).
	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.
	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.
	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]

[Contacts]