| Refinements for free! C Cohen, M Dénès, A Mörtberg International Conference on Certified Programs and Proofs, 147-162, 2013 | 106 | 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 | 96 | 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 | 85 | 2015 |
| A Refinement-Based Approach to Computational Algebra in Coq M Dénès, A Mörtberg, V Siles International Conference on Interactive Theorem Proving, 83-98, 2012 | 74 | 2012 |
| Full reduction at full throttle M Boespflug, M Dénès, B Grégoire International Conference on Certified Programs and Proofs, 362-377, 2011 | 63 | 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 | 35 | 2014 |
| 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 | 26 | 2016 |
| 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 Computational Topology in Image Context: 4th International Workshop, CTIC …, 2012 | 26 | 2012 |
| 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 | 21 | 2016 |
| Incidence simplicial matrices formalized in Coq/SSReflect J Heras, M Poza, M Dénès, L Rideau International Conference on Intelligent Computer Mathematics, 30-44, 2011 | 17 | 2011 |
| Matrices à blocs et en forme canonique G Cano, M Dénès JFLA-Journées francophones des langages applicatifs, 2013 | 11 | 2013 |
| Coq-Club M Dénès Propositional extensionality is inconsistent in Coq, 2013-12, 2013 | 10 | 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 |
| Towards primitive data types for COQ 63-bits integers and persistent arrays M Dénès Coq-5, the Coq Workshop 2013, 2013 | 4 | 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 |
| Formal proof of theorems on genetic regulatory networks M Dénes, 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
