Researcher - Cyril Cohen - Microsoft Research Inria Joint Centre

2013

Conference papers

titre: Refinements for Free!
auteur: Cyril Cohen, Maxime Dénès, Anders Mörtberg
article: Certified Programs and Proofs, Dec 2013, Melbourne, Australia. pp.147 - 162, 2013, <10.1007/978-3-319-03545-1_10>
Accès au texte intégral et bibtex

titre: A Machine-Checked Proof of the Odd Order Theorem
auteur: Georges Gonthier, Andrea Asperti, Jeremy Avigad, Yves Bertot, Cyril Cohen, François Garillot, Stéphane Le Roux, Assia Mahboubi, Russell O’Connor, Sidi Ould Biha, Ioana Pasca, Laurence Rideau, Alexey Solovyev, Enrico Tassi, Laurent Théry
article: Sandrine Blazy and Christine Paulin and David Pichardie. ITP 2013, 4th Conference on Interactive Theorem Proving, Jul 2013, Rennes, France. Springer, 7998, pp.163-179, 2013, LNCS. <10.1007/978-3-642-39634-2_14>
Accès au texte intégral et bibtex

Books

titre: Homotopy Type Theory: Univalent Foundations of Mathematics
auteur: Peter Aczel, Benedikt Ahrens, Thorsten Altenkirch, Steve Awodey, Bruno Barras, Andrej Bauer, Yves Bertot, Marc Bezem, Thierry Coquand, Eric Finster, Daniel Grayson, Hugo Herbelin, André Joyal, Dan Licata, Peter Lumsdaine, Assia Mahboubi, Per Martin-Löf, Sergey Melikhov, Alvaro Pelayo, Andrew Polonsky, Michael Shulman, Matthieu Sozeau, Bas Spitters, Benno Van den Berg, Vladimir Voevodsky, Michael Warren, Carlo Angiuli, Anthony Bordg, Guillaume Brunerie, Chris Kapulkin, Egbert Rijke, Kristina Sojakova, Jeremy Avigad, Cyril Cohen, Robert Constable, Pierre-Louis Curien, Peter Dybjer, Martín Escardó, Kuen-Bang Hou, Nicola Gambino, Richard Garner, Georges Gonthier, Thomas Hales, Robert Harper, Martin Hofmann, Pieter Hofstra, Joachim Koch, Nicolai Kraus, Nuo Li, Zhaohui Luo, Michael Nahas, Erik Palmgren, Emily Riehl, Dana Scott, Philip Scott, Sergei Soloviev
article: Aucun, pp.448, 2013
Accès au bibtex

2012

Journal articles

titre: Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination
auteur: Cyril Cohen, Assia Mahboubi
article: Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2012, 8 (1:02), pp.1-40. <10.2168/LMCS-8 (1:02) 2012>
Accès au texte intégral et bibtex

Conference papers

titre: Construction of real algebraic numbers in Coq
auteur: Cyril Cohen
article: Lennart Beringer and Amy Felty. ITP - 3rd International Conference on Interactive Theorem Proving - 2012, Aug 2012, Princeton, United States. Springer, 2012
Accès au texte intégral et bibtex

titre: Construction des nombres algébriques réels en Coq
auteur: Cyril Cohen
article: JFLA - Journées Francophones des Langages Applicatifs - 2012, Feb 2012, Carnac, France. 2012
Accès au texte intégral et bibtex

Theses

titre: Formalized algebraic numbers: construction and first-order theory.
auteur: Cyril Cohen
article: Logic in Computer Science [cs.LO]. Ecole Polytechnique X, 2012. English
Accès au texte intégral et bibtex

2010

Conference papers

titre: A formal quantifier elimination for algebraically closed fields
auteur: Cyril Cohen, Assia Mahboubi
article: Symposium on the Integration of Symbolic Computation and Mechanised Reasoning, Calculemus, Jul 2010, Paris, France. Springer, 6167, pp.189-203, 2010, Computer Science; Intelligent Computer Mathematics. <10.1007/978-3-642-14128-7_17>
Accès au texte intégral et bibtex

Preprints, Working Papers, …

Researchers