Follow
Maxime Dénès
Maxime Dénès
Inria Paris-Rocquencourt
Verified email at maximedenes.fr - Homepage
Title
Cited by
Cited by
Year
Refinements for free!
C Cohen, M Dénès, A Mörtberg
International Conference on Certified Programs and Proofs, 147-162, 2013
1042013
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
912015
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
792015
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
712012
Full reduction at full throttle
M Boespflug, M Dénès, B Grégoire
International Conference on Certified Programs and Proofs, 362-377, 2011
622011
QuickChick: Property-based testing for Coq
M Dénès, C Hritcu, L Lampropoulos, Z Paraskevopoulou, BC Pierce
The Coq Workshop 125, 126, 2014
322014
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
262016
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
262012
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
222016
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
132011
Matrices à blocs et en forme canonique
G Cano, M Dénès
JFLA-Journées francophones des langages applicatifs, 2013
122013
Coq-Club
M Dénès
Propositional extensionality is inconsistent in Coq, 2013-12, 2013
102013
Étude formelle d'algorithmes efficaces en algèbre linéaire
M Dénès
Université Nice Sophia Antipolis, 2013
62013
CoqEAL, the Coq Effective Algebra Library, 2012
M Dénes, A Mörtberg, V Siles
52013
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
32020
Coqonut: A verified JIT compiler for Coq
M Dénès, X Leroy
32015
Towards primitive data types for COQ 63-bits integers and persistent arrays
M Dénès
Coq-5, the Coq Workshop 2013, 2013
32013
A Coq framework for verified property-based testing
Z Paraskevopoulou, C Hritcu
Internship Report, Inria Paris-Rocquencourt, 2014
22014
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
22009
Experiments with computable matrices in the Coq system
M Dénes, Y Bertot
Coq Workshop, 2011
12011
The system can't perform the operation now. Try again later.
Articles 1–20