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 Videos: carmin.tv Documents Indexed: 18 Publications since 2010 1 Further Contribution Software Indexed: 6 Packages Co-Authors: 36 Co-Authors with 17 Joint Publications 478 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 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 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 16 Publications have been cited 269 times in 233 Documents Cited by ▼ Year ▼ Homotopy type theory. Univalent foundations of mathematics. Zbl 1298.03002 The Univalent Foundations Program 261 2013 Cubical type theory: a constructive interpretation of the univalence axiom. Zbl 1434.03036 Cohen, Cyril; Coquand, Thierry; Huber, Simon; Mörtberg, Anders 87 2018 A machine-checked proof of the odd order theorem. Zbl 1317.68211 Gonthier, 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 70 2013 Refinements for free! Zbl 1426.68165 Cohen, Cyril; Dénès, Maxime; Mörtberg, Anders 21 2013 Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination. Zbl 1241.68096 Cohen, Cyril; Mahboubi, Assia 19 2012 Pragmatic quotient types in Coq. Zbl 1317.68207 Cohen, Cyril 13 2013 Construction of real algebraic numbers in Coq. Zbl 1360.68744 Cohen, Cyril 11 2012 Formalization techniques for asymptotic reasoning in classical analysis. Zbl 1451.68329 Affeldt, Reynald; Cohen, Cyril; Rouhling, Damien 10 2018 The MetaCoq project. Zbl 1468.68075 Sozeau, Matthieu; Anand, Abhishek; Boulier, Simon; Cohen, Cyril; Forster, Yannick; Kunze, Fabian; Malecha, Gregory; Tabareau, Nicolas; Winterhalter, Théo 10 2020 Formalized linear algebra over elementary divisor rings in Coq. Zbl 1448.68461 Cano, Guillaume; Cohen, Cyril; Dénès, Maxime; Mörtberg, Anders; Siles, Vincent 6 2016 Competing inheritance paths in dependent type theory: a case study in functional analysis. Zbl 07614659 Affeldt, Reynald; Cohen, Cyril; Kerjean, Marie; Mahboubi, Assia; Rouhling, Damien; Sakaguchi, Kazuhiko 6 2020 Towards certified meta-programming with typed Template-Coq. Zbl 1468.68071 Anand, Abhishek; Boulier, Simon; Cohen, Cyril; Sozeau, Matthieu; Tabareau, Nicolas 5 2018 A formal proof in Coq of Lasalle’s invariance principle. Zbl 1484.68315 Cohen, Cyril; Rouhling, Damien 4 2017 A formal quantifier elimination for algebraically closed fields. Zbl 1286.68394 Cohen, Cyril; Mahboubi, Assia 3 2010 Formal proofs of Tarjan’s strongly connected components algorithm in Why3, Coq and Isabelle. Zbl 07649962 Chen, Ran; Cohen, Cyril; Lévy, Jean-Jacques; Merz, Stephan; Théry, Laurent 3 2019 Unsolvability of the quintic formalized in dependent type theory. Zbl 07699425 Bernard, Sophie; Cohen, Cyril; Mahboubi, Assia; Strub, Pierre-Yves 1 2021 Unsolvability of the quintic formalized in dependent type theory. Zbl 07699425 Bernard, Sophie; Cohen, Cyril; Mahboubi, Assia; Strub, Pierre-Yves 1 2021 The MetaCoq project. Zbl 1468.68075 Sozeau, Matthieu; Anand, Abhishek; Boulier, Simon; Cohen, Cyril; Forster, Yannick; Kunze, Fabian; Malecha, Gregory; Tabareau, Nicolas; Winterhalter, Théo 10 2020 Competing inheritance paths in dependent type theory: a case study in functional analysis. Zbl 07614659 Affeldt, Reynald; Cohen, Cyril; Kerjean, Marie; Mahboubi, Assia; Rouhling, Damien; Sakaguchi, Kazuhiko 6 2020 Formal proofs of Tarjan’s strongly connected components algorithm in Why3, Coq and Isabelle. Zbl 07649962 Chen, Ran; Cohen, Cyril; Lévy, Jean-Jacques; Merz, Stephan; Théry, Laurent 3 2019 Cubical type theory: a constructive interpretation of the univalence axiom. Zbl 1434.03036 Cohen, Cyril; Coquand, Thierry; Huber, Simon; Mörtberg, Anders 87 2018 Formalization techniques for asymptotic reasoning in classical analysis. Zbl 1451.68329 Affeldt, Reynald; Cohen, Cyril; Rouhling, Damien 10 2018 Towards certified meta-programming with typed Template-Coq. Zbl 1468.68071 Anand, Abhishek; Boulier, Simon; Cohen, Cyril; Sozeau, Matthieu; Tabareau, Nicolas 5 2018 A formal proof in Coq of Lasalle’s invariance principle. Zbl 1484.68315 Cohen, Cyril; Rouhling, Damien 4 2017 Formalized linear algebra over elementary divisor rings in Coq. Zbl 1448.68461 Cano, Guillaume; Cohen, Cyril; Dénès, Maxime; Mörtberg, Anders; Siles, Vincent 6 2016 Homotopy type theory. Univalent foundations of mathematics. Zbl 1298.03002 The Univalent Foundations Program 261 2013 A machine-checked proof of the odd order theorem. Zbl 1317.68211 Gonthier, 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 70 2013 Refinements for free! Zbl 1426.68165 Cohen, Cyril; Dénès, Maxime; Mörtberg, Anders 21 2013 Pragmatic quotient types in Coq. Zbl 1317.68207 Cohen, Cyril 13 2013 Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination. Zbl 1241.68096 Cohen, Cyril; Mahboubi, Assia 19 2012 Construction of real algebraic numbers in Coq. Zbl 1360.68744 Cohen, Cyril 11 2012 A formal quantifier elimination for algebraically closed fields. Zbl 1286.68394 Cohen, Cyril; Mahboubi, Assia 3 2010 all cited Publications top 5 cited Publications all top 5 Cited by 389 Authors 8 Buchholtz, Ulrik 8 Coquand, Thierry 8 Paulson, Lawrence Charles 6 Affeldt, Reynald 6 Divasón, Jose 6 Møgelberg, Rasmus Ejlers 6 Pitts, Andrew M. 6 Sattler, Christian 5 Angiuli, Carlo 5 Cohen, Cyril 5 Harper, Robert 5 Huber, Simon 5 Kaliszyk, Cezary 5 Mörtberg, Anders 5 Orton, Ian 4 Ahrens, Benedikt 4 Allamigeon, Xavier 4 Altenkirch, Thorsten 4 Aransay, Jesús 4 Avigad, Jeremy 4 Gambino, Nicola 4 Kaposi, Ambrus 4 Kapulkin, Krzysztof 4 Katz, Ricardo David 4 Licata, Daniel R. 4 Spitters, Bas 4 Théry, Laurent 4 Thiemann, René 4 Vezzosi, Andrea 3 Awodey, Steve 3 Birkedal, Lars 3 Bizjak, Aleš 3 Boulier, Simon 3 Clouston, Ranald A. 3 Hou (Favonia), Kuen-Bang 3 Kirst, Dominik 3 Li, Wenda 3 Lochbihler, Andreas 3 Mannaa, Bassel 3 Martin-Dorel, Érik 3 Narboux, Julien 3 Rabe, Florian 3 Rouhling, Damien 3 Roux, Pierre 3 Tabareau, Nicolas 3 van der Weide, Niels 3 Veltri, Niccolò 3 Weinberger, Jonathan Maximilian Lajos 3 Yamada, Akihisa 2 Abel, Andreas M. 2 Asperti, Andrea 2 Barrett, Clark W. 2 Boutry, Pierre 2 Dagand, Pierre-Evariste 2 Davenport, James Harold 2 Devriese, Dominique 2 Doczkal, Christian 2 Dubois, Catherine 2 Dumbrava, Stefania 2 Farmer, William M. 2 Forster, Yannick 2 Fürer, Basil 2 Garrigue, Jacques 2 Grathwohl, Hans Bugge 2 Gunther, Emmanuel 2 Heras, Jónathan 2 Joosten, Sebastiaan J. C. 2 Kohlhase, Michael 2 Kovács, András 2 Kraus, Nicolai 2 Kremer, Gereon 2 Kunze, Fabian 2 Larchey-Wendling, Dominique 2 Mahboubi, Assia 2 Martín-Mateos, Francisco-Jesús 2 Muñoz, César A. 2 Narkawicz, Anthony Joseph 2 Nipkow, Tobias 2 Norrish, Michael 2 Nowak, David E. 2 Ozdemir, Alex 2 Pagano, Miguel 2 Platzer, André 2 Rijke, Egbert 2 Saikawa, Takafumi 2 Sakaguchi, Kazuhiko 2 Schneider, Joshua P. 2 Shulman, Michael A. 2 Sozeau, Matthieu 2 Steinberg, Florian 2 Stojanović Đurđević, Sana 2 Stratulat, Sorin 2 Strub, Pierre-Yves 2 Tan, Yong Kiam 2 Tassi, Enrico 2 Thies, Holger 2 Tinelli, Cesare 2 Traytel, Dmitry 2 Tsementzis, Dimitris 2 Uemura, Taichi ...and 289 more Authors all top 5 Cited in 45 Serials 39 Journal of Automated Reasoning 17 Logical Methods in Computer Science 14 Mathematical Structures in Computer Science 9 Journal of Functional Programming 4 Synthese 4 Annals of Pure and Applied Logic 3 Journal of Symbolic Computation 3 Annals of Mathematics and Artificial Intelligence 3 Journal of Formalized Reasoning 3 Journal of Logical and Algebraic Methods in Programming 3 Higher Structures 2 Formal Aspects of Computing 2 Indagationes Mathematicae. New Series 2 Experimental Mathematics 2 Mathematics in Computer Science 2 Philosophical Transactions of the Royal Society of London. A. Mathematical, Physical and Engineering Sciences 1 Artificial Intelligence 1 Communications in Mathematical Physics 1 The Mathematical Intelligencer 1 Journal of the London Mathematical Society. Second Series 1 Journal of Mathematical Economics 1 Journal of Pure and Applied Algebra 1 The Journal of Symbolic Logic 1 Mathematica Scandinavica 1 Proceedings of the American Mathematical Society 1 Theoretical Computer Science 1 European Journal of Combinatorics 1 Information and Computation 1 Bulletin of the American Mathematical Society. New Series 1 Applicable Algebra in Engineering, Communication and Computing 1 The New York Journal of Mathematics 1 Selecta Mathematica. New Series 1 Theory and Applications of Categories 1 La Gaceta de la Real Sociedad Matemática Española 1 Algebraic & Geometric Topology 1 Theory and Practice of Logic Programming 1 JP Journal of Algebra, Number Theory and Applications 1 ACM Transactions on Computational Logic 1 Journal of Homotopy and Related Structures 1 Journal of Topology 1 The Review of Symbolic Logic 1 Forum of Mathematics, Pi 1 Stochastic Systems 1 Proceedings of the Royal Society of London. A. Mathematical, Physical and Engineering Sciences 1 Journal of Membrane Computing all top 5 Cited in 28 Fields 164 Computer science (68-XX) 113 Mathematical logic and foundations (03-XX) 48 Algebraic topology (55-XX) 47 Category theory; homological algebra (18-XX) 9 Number theory (11-XX) 7 General and overarching topics; collections (00-XX) 7 Commutative algebra (13-XX) 6 Linear and multilinear algebra; matrix theory (15-XX) 6 Numerical analysis (65-XX) 5 Field theory and polynomials (12-XX) 5 Algebraic geometry (14-XX) 4 Geometry (51-XX) 3 Group theory and generalizations (20-XX) 3 Real functions (26-XX) 3 Convex and discrete geometry (52-XX) 3 Operations research, mathematical programming (90-XX) 2 History and biography (01-XX) 2 Combinatorics (05-XX) 2 Order, lattices, ordered algebraic structures (06-XX) 2 Associative rings and algebras (16-XX) 2 Ordinary differential equations (34-XX) 2 Systems theory; control (93-XX) 1 Functions of a complex variable (30-XX) 1 Probability theory and stochastic processes (60-XX) 1 Quantum theory (81-XX) 1 Game theory, economics, finance, and other social and behavioral sciences (91-XX) 1 Information and communication theory, circuits (94-XX) 1 Mathematics education (97-XX) Citations by Year