Edit Profile (opens in new tab) Cohen, Cyril Co-Author Distance Author ID: cohen.cyril Published as: Cohen, Cyril Homepage: https://perso.crans.org/cohen/ External Links: MGP · ORCID · ResearchGate · dblp Documents Indexed: 18 Publications since 2010 1 Further Contribution Co-Authors: 37 Co-Authors with 17 Joint Publications 453 Co-Co-Authors all top 5 Co-Authors 2 single-authored 6 Mahboubi, Assia 4 Mörtberg, Anders 3 Affeldt, Reynald 3 Coquand, Thierry 3 Rouhling, Damien 3 Sozeau, Matthieu 2 Anand, Abhishek 2 Avigad, Jeremy 2 Bertot, Yves 2 Boulier, Simon 2 Dénès, Maxime 2 Gonthier, Georges 2 Tabareau, Nicolas 2 Théry, Laurent 1 Aczel, Peter 1 Ahrens, Benedikt 1 Altenkirch, Thorsten 1 Angiuli, Carlo 1 Asperti, Andrea 1 Awodey, Steve 1 Barras, Bruno 1 Bauer, Andrej 1 Bernard, Sophie 1 Bezem, Marc 1 Bordg, Anthony 1 Brunerie, Guillaume 1 Cano, Guillaume 1 Chen, Ran 1 Constable, Robert Lee 1 Curien, Pierre-Louis 1 Dybjer, Peter 1 Finster, Eric 1 Forster, Yannick 1 Gambino, Nicola 1 Garillot, François 1 Garner, Richard 1 Grayson, Daniel Richard 1 Hales, Thomas Callister 1 Harper, Robert 1 Herbelin, Hugo 1 Hofmann, Martin 1 Hofstra, Pieter J. W. 1 Hötzel Escardó, Martín 1 Hou (Favonia), Kuen-Bang 1 Huber, Simon 1 Joyal, André 1 Kapulkin, Krzysztof 1 Kerjean, Marie 1 Kock, Joachim 1 Kraus, Nicolai 1 Kunze, Fabian 1 Leroux, Stéphane 1 Levy, Jean-Jacques 1 Li, Nuo 1 Licata, Dan 1 Lumsdaine, Peter LeFanu 1 Luo, Zhaohui 1 Malecha, Gregory 1 Martin-Löf, Per 1 Melikhov, Sergey Aleksandrovich 1 Merz, Stephan 1 Nahas, Michael 1 O’Connor, Russell 1 Ould Biha, Sidi 1 Palmgren, Erik 1 Paşca, Ioana 1 Pelayo, Alvaro 1 Polonsky, Andrew 1 Rideau, Laurence 1 Riehl, Emily 1 Rijke, Egbert 1 Sakaguchi, Kazuhiko 1 Scott, Dana Stewart 1 Scott, Philip J. 1 Shulman, Michael A. 1 Siles, Vincent 1 Sojakova, Kristina 1 Solov’ëv, Sergeĭ Vladimirovich 1 Solovyev, Alexey 1 Spitters, Bas 1 Strub, Pierre-Yves 1 Tassi, Enrico 1 1 Van den Berg, Benno 1 Voevodskiĭ, Vladimir Aleksandrovich 1 Warren, Michael Alton 1 Winterhalter, Théo 1 Zeilberger, Noam Serials 2 Journal of Automated Reasoning 2 Logical Methods in Computer Science 1 Journal of Algebra 1 Journal of Formalized Reasoning all top 5 Fields 16 Computer science (68-XX) 7 Mathematical logic and foundations (03-XX) 4 Field theory and polynomials (12-XX) 2 Category theory; homological algebra (18-XX) 2 Algebraic topology (55-XX) 1 Number theory (11-XX) 1 Algebraic geometry (14-XX) 1 Linear and multilinear algebra; matrix theory (15-XX) 1 Associative rings and algebras (16-XX) 1 Group theory and generalizations (20-XX) 1 Real functions (26-XX) 1 Ordinary differential equations (34-XX) Publications by Year all cited Publications top 5 cited Publications Citations contained in zbMATH Open 15 Publications have been cited 197 times in 170 Documents Cited by ▼ Year ▼ Homotopy type theory. Univalent foundations of mathematics. Zbl 1298.03002The Univalent Foundations Program 122 2013 A machine-checked proof of the odd order theorem. Zbl 1317.68211Gonthier, Georges; Asperti, Andrea; Avigad, Jeremy; Bertot, Yves; Cohen, Cyril; Garillot, François; Le Roux, Stéphane; Mahboubi, Assia; O’Connor, Russell; Ould Biha, Sidi; Pasca, Ioana; Rideau, Laurence; Solovyev, Alexey; Tassi, Enrico; Théry, Laurent 57 2013 Cubical type theory: a constructive interpretation of the univalence axiom. Zbl 1434.03036Cohen, Cyril; Coquand, Thierry; Huber, Simon; Mörtberg, Anders 52 2018 Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination. Zbl 1241.68096Cohen, Cyril; Mahboubi, Assia 15 2012 Refinements for free! Zbl 1426.68165Cohen, Cyril; Dénès, Maxime; Mörtberg, Anders 15 2013 Pragmatic quotient types in Coq. Zbl 1317.68207Cohen, Cyril 12 2013 Construction of real algebraic numbers in Coq. Zbl 1360.68744Cohen, Cyril 11 2012 Formalization techniques for asymptotic reasoning in classical analysis. Zbl 1451.68329Affeldt, Reynald; Cohen, Cyril; Rouhling, Damien 8 2018 Formalized linear algebra over elementary divisor rings in Coq. Zbl 1448.68461Cano, Guillaume; Cohen, Cyril; Dénès, Maxime; Mörtberg, Anders; Siles, Vincent 5 2016 The MetaCoq project. Zbl 1468.68075Sozeau, Matthieu; Anand, Abhishek; Boulier, Simon; Cohen, Cyril; Forster, Yannick; Kunze, Fabian; Malecha, Gregory; Tabareau, Nicolas; Winterhalter, Théo 5 2020 Towards certified meta-programming with typed Template-Coq. Zbl 1468.68071Anand, Abhishek; Boulier, Simon; Cohen, Cyril; Sozeau, Matthieu; Tabareau, Nicolas 5 2018 A formal proof in Coq of Lasalle’s invariance principle. Zbl 1484.68315Cohen, Cyril; Rouhling, Damien 4 2017 Competing inheritance paths in dependent type theory: a case study in functional analysis. Zbl 07614659Affeldt, Reynald; Cohen, Cyril; Kerjean, Marie; Mahboubi, Assia; Rouhling, Damien; Sakaguchi, Kazuhiko 4 2020 A formal quantifier elimination for algebraically closed fields. Zbl 1286.68394Cohen, Cyril; Mahboubi, Assia 2 2010 Formal proofs of Tarjan’s strongly connected components algorithm in Why3, Coq and Isabelle. Zbl 07649962Chen, Ran; Cohen, Cyril; Lévy, Jean-Jacques; Merz, Stephan; Théry, Laurent 2 2019 The MetaCoq project. Zbl 1468.68075Sozeau, Matthieu; Anand, Abhishek; Boulier, Simon; Cohen, Cyril; Forster, Yannick; Kunze, Fabian; Malecha, Gregory; Tabareau, Nicolas; Winterhalter, Théo 5 2020 Competing inheritance paths in dependent type theory: a case study in functional analysis. Zbl 07614659Affeldt, Reynald; Cohen, Cyril; Kerjean, Marie; Mahboubi, Assia; Rouhling, Damien; Sakaguchi, Kazuhiko 4 2020 Formal proofs of Tarjan’s strongly connected components algorithm in Why3, Coq and Isabelle. Zbl 07649962Chen, Ran; Cohen, Cyril; Lévy, Jean-Jacques; Merz, Stephan; Théry, Laurent 2 2019 Cubical type theory: a constructive interpretation of the univalence axiom. Zbl 1434.03036Cohen, Cyril; Coquand, Thierry; Huber, Simon; Mörtberg, Anders 52 2018 Formalization techniques for asymptotic reasoning in classical analysis. Zbl 1451.68329Affeldt, Reynald; Cohen, Cyril; Rouhling, Damien 8 2018 Towards certified meta-programming with typed Template-Coq. Zbl 1468.68071Anand, Abhishek; Boulier, Simon; Cohen, Cyril; Sozeau, Matthieu; Tabareau, Nicolas 5 2018 A formal proof in Coq of Lasalle’s invariance principle. Zbl 1484.68315Cohen, Cyril; Rouhling, Damien 4 2017 Formalized linear algebra over elementary divisor rings in Coq. Zbl 1448.68461Cano, Guillaume; Cohen, Cyril; Dénès, Maxime; Mörtberg, Anders; Siles, Vincent 5 2016 Homotopy type theory. Univalent foundations of mathematics. Zbl 1298.03002The Univalent Foundations Program 122 2013 A machine-checked proof of the odd order theorem. Zbl 1317.68211Gonthier, Georges; Asperti, Andrea; Avigad, Jeremy; Bertot, Yves; Cohen, Cyril; Garillot, François; Le Roux, Stéphane; Mahboubi, Assia; O’Connor, Russell; Ould Biha, Sidi; Pasca, Ioana; Rideau, Laurence; Solovyev, Alexey; Tassi, Enrico; Théry, Laurent 57 2013 Refinements for free! Zbl 1426.68165Cohen, Cyril; Dénès, Maxime; Mörtberg, Anders 15 2013 Pragmatic quotient types in Coq. Zbl 1317.68207Cohen, Cyril 12 2013 Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination. Zbl 1241.68096Cohen, Cyril; Mahboubi, Assia 15 2012 Construction of real algebraic numbers in Coq. Zbl 1360.68744Cohen, Cyril 11 2012 A formal quantifier elimination for algebraically closed fields. Zbl 1286.68394Cohen, Cyril; Mahboubi, Assia 2 2010 all cited Publications top 5 cited Publications all top 5 Cited by 325 Authors 6 Affeldt, Reynald 6 Coquand, Thierry 5 Buchholtz, Ulrik 5 Cohen, Cyril 5 Kaliszyk, Cezary 4 Ahrens, Benedikt 4 Allamigeon, Xavier 4 Avigad, Jeremy 4 Divasón, Jose 4 Huber, Simon 4 Katz, Ricardo David 4 Møgelberg, Rasmus Ejlers 4 Mörtberg, Anders 4 Paulson, Lawrence Charles 4 Pitts, Andrew M. 4 Sattler, Christian 4 Théry, Laurent 4 Thiemann, René 3 Angiuli, Carlo 3 Birkedal, Lars 3 Bizjak, Aleš 3 Boulier, Simon 3 Clouston, Ranald A. 3 Harper, Robert 3 Hou (Favonia), Kuen-Bang 3 Kaposi, Ambrus 3 Kapulkin, Krzysztof 3 Li, Wenda 3 Lochbihler, Andreas 3 Narboux, Julien 3 Orton, Ian 3 Rabe, Florian 3 Rouhling, Damien 3 Spitters, Bas 3 Yamada, Akihisa 2 Abel, Andreas M. 2 Altenkirch, Thorsten 2 Aransay, Jesús 2 Asperti, Andrea 2 Awodey, Steve 2 Boutry, Pierre 2 Doczkal, Christian 2 Dumbrava, Stefania 2 Farmer, William M. 2 Forster, Yannick 2 Fürer, Basil 2 Garrigue, Jacques 2 Grathwohl, Hans Bugge 2 Heras, Jónathan 2 Joosten, Sebastiaan J. C. 2 Kirst, Dominik 2 Kohlhase, Michael 2 Kunze, Fabian 2 Larchey-Wendling, Dominique 2 Mahboubi, Assia 2 Mannaa, Bassel 2 Martin-Dorel, Érik 2 Martín-Mateos, Francisco-Jesús 2 Muñoz, César A. 2 Narkawicz, Anthony Joseph 2 Norrish, Michael 2 Roux, Pierre 2 Saikawa, Takafumi 2 Sakaguchi, Kazuhiko 2 Schneider, Joshua P. 2 Shulman, Michael A. 2 Steinberg, Florian 2 Stojanović Đurđević, Sana 2 Stratulat, Sorin 2 Strub, Pierre-Yves 2 Tabareau, Nicolas 2 Tan, Yong Kiam 2 Thies, Holger 2 Traytel, Dmitry 2 Tsementzis, Dimitris 2 Urban, Josef 2 van der Weide, Niels 2 Veltri, Niccolò 2 Vezzosi, Andrea 2 von Raumer, Jakob 1 Abrahamsson, Oskar 1 Adams, Mark 1 Anand, Abhishek 1 Annenkov, Danil 1 Avelar, Andréia Borges 1 Ayala-Rincón, Mauricio 1 Baanen, Anne 1 Bancerek, Grzegorz 1 Barbosa, Haniel 1 Barrett, Clark W. 1 Bauer, Gertrud 1 Bentzen, Bruno 1 Benzaken, Véronique 1 Bernard, Sophie 1 Bertholon, Guillaume 1 Bertot, Yves 1 Bezem, Marc 1 Blot, Arthur 1 Bonifati, Angela 1 Bordg, Anthony ...and 225 more Authors all top 5 Cited in 33 Serials 33 Journal of Automated Reasoning 17 Logical Methods in Computer Science 11 MSCS. Mathematical Structures in Computer Science 6 Journal of Functional Programming 3 Synthese 3 Journal of Symbolic Computation 3 Annals of Mathematics and Artificial Intelligence 3 Journal of Formalized Reasoning 2 Annals of Pure and Applied Logic 2 Formal Aspects of Computing 2 Experimental Mathematics 2 Mathematics in Computer Science 2 Philosophical Transactions of the Royal Society of London. A. Mathematical, Physical and Engineering Sciences 2 Higher Structures 1 Artificial Intelligence 1 The Mathematical Intelligencer 1 Journal of Mathematical Economics 1 Mathematica Scandinavica 1 Proceedings of the American Mathematical Society 1 Theoretical Computer Science 1 Information and Computation 1 Bulletin of the American Mathematical Society. New Series 1 Indagationes Mathematicae. New Series 1 Applicable Algebra in Engineering, Communication and Computing 1 The New York Journal of Mathematics 1 Theory and Practice of Logic Programming 1 JP Journal of Algebra, Number Theory and Applications 1 ACM Transactions on Computational Logic 1 The Review of Symbolic Logic 1 Forum of Mathematics, Pi 1 Stochastic Systems 1 Journal of Logical and Algebraic Methods in Programming 1 Journal of Membrane Computing all top 5 Cited in 26 Fields 132 Computer science (68-XX) 79 Mathematical logic and foundations (03-XX) 23 Category theory; homological algebra (18-XX) 22 Algebraic topology (55-XX) 9 Number theory (11-XX) 6 General and overarching topics; collections (00-XX) 6 Commutative algebra (13-XX) 5 Algebraic geometry (14-XX) 5 Numerical analysis (65-XX) 4 Field theory and polynomials (12-XX) 4 Linear and multilinear algebra; matrix theory (15-XX) 3 Real functions (26-XX) 3 Geometry (51-XX) 3 Convex and discrete geometry (52-XX) 3 Operations research, mathematical programming (90-XX) 2 Ordinary differential equations (34-XX) 2 Systems theory; control (93-XX) 1 History and biography (01-XX) 1 Combinatorics (05-XX) 1 Associative rings and algebras (16-XX) 1 Nonassociative rings and algebras (17-XX) 1 Group theory and generalizations (20-XX) 1 Functions of a complex variable (30-XX) 1 Probability theory and stochastic processes (60-XX) 1 Game theory, economics, finance, and other social and behavioral sciences (91-XX) 1 Information and communication theory, circuits (94-XX) Citations by Year