| Refinements for free! C Cohen, M Dénès, A Mörtberg Certified Programs and Proofs: Third International Conference, CPP 2013 …, 2013 | 96 | 2013 |
| Foundational property-based testing Z Paraskevopoulou, C Hriţcu, M Dénès, L Lampropoulos, BC Pierce Interactive Theorem Proving: 6th International Conference, ITP 2015, Nanjing …, 2015 | 80 | 2015 |
| Micro-policies: Formally verified, tag-based security monitors AA De Amorim, M Dénès, N Giannarakis, C Hritcu, BC Pierce, ... 2015 IEEE Symposium on Security and Privacy, 813-830, 2015 | 73 | 2015 |
| A Refinement-Based Approach to Computational Algebra in Coq M Dénès, A Mörtberg, V Siles Interactive Theorem Proving: Third International Conference, ITP 2012 …, 2012 | 66 | 2012 |
| Full reduction at full throttle M Boespflug, M Dénès, B Grégoire Certified Programs and Proofs: First International Conference, CPP 2011 …, 2011 | 55 | 2011 |
| QuickChick: Property-based testing for Coq M Dénès, C Hritcu, L Lampropoulos, Z Paraskevopoulou, BC Pierce The Coq Workshop 125, 126, 2014 | 27 | 2014 |
| Towards a Certified Computation of Homology Groups for Digital Images. J Heras, M Dénès, G Mata, A Mörtberg, M Poza, V Siles CTIC 12, 49-57, 2012 | 24 | 2012 |
| Testing noninterference, quickly C Hriţcu, L Lampropoulos, A Spector-Zabusky, AA De Amorim, M Dénès, ... Journal of Functional Programming 26, e4, 2016 | 22 | 2016 |
| Formalized linear algebra over elementary divisor rings in Coq G Cano, C Cohen, M Dénès, A Mörtberg, V Siles Logical Methods in Computer Science 12, 2016 | 15 | 2016 |
| Incidence simplicial matrices formalized in Coq/SSReflect J Heras, M Poza, M Dénès, L Rideau Intelligent Computer Mathematics: 18th Symposium, Calculemus 2011, and 10th …, 2011 | 14 | 2011 |
| Coq-Club M Dénès Propositional extensionality is inconsistent in Coq, 2013-12, 2013 | 9 | 2013 |
| Matrices à blocs et en forme canonique G Cano, M Dénès JFLA-Journées francophones des langages applicatifs, 2013 | 7 | 2013 |
| Étude formelle d'algorithmes efficaces en algèbre linéaire M Dénès Université Nice Sophia Antipolis, 2013 | 6 | 2013 |
| CoqEAL, the Coq Effective Algebra Library, 2012 M Dénes, A Mörtberg, V Siles | 5 | 2013 |
| ICUBAM: ICU Bed Availability Monitoring and analysis in the Grand Est région of France during the COVID-19 epidemic Consortium ICUBAM, L Bonnasse-Gahot, M Dénès, G Dulac-Arnold, ... medRxiv, 2020.05. 18.20091264, 2020 | 3 | 2020 |
| Coqonut: A verified JIT compiler for Coq M Dénès, X Leroy | 3 | 2015 |
| A Coq framework for verified property-based testing Z Paraskevopoulou, C Hritcu Internship Report, Inria Paris-Rocquencourt, 2014 | 2 | 2014 |
| Towards primitive data types for COQ 63-bits integers and persistent arrays M Dénès Coq-5, the Coq Workshop 2013, 2013 | 2 | 2013 |
| Formal proof of theorems on genetic regulatory networks M Dénès, B Lesage, Y Bertot, A Richard 2009 11th International Symposium on Symbolic and Numeric Algorithms for …, 2009 | 2 | 2009 |
| Experiments with computable matrices in the Coq system M Dénes, Y Bertot Coq Workshop, 2011 | 1 | 2011 |
Benjamin C. PierceProfessor of Computer and Information Science, University of PennsylvaniaVerified email at cis.upenn.edu
