Formal Proof of Theorems on Genetic Regulatory Networks. - Maxime Dénès; Benjamin Lesage; Yves Bertot; Adrien Richard (SYNASC, 2009)

Full Reduction at Full Throttle. - Mathieu Boespflug; Maxime Dénès; Benjamin Grégoire (CPP, 2011)

Incidence Simplicial Matrices Formalized in Coq/SSReflect. - Jónathan Heras; María Poza; Maxime Dénès; Laurence Rideau (Calculemus/MKM, 2011)

Towards a Certified Computation of Homology Groups for Digital Images. - Jónathan Heras; Maxime Dénès; Gadea Mata; Anders Mörtberg; María Poza; Vincent Siles (CTIC, 2012)

A Refinement-Based Approach to Computational Algebra in Coq. - Maxime Dénès; Anders Mörtberg; Vincent Siles (ITP, 2012)

Refinements for Free! - Cyril Cohen; Maxime Dénès; Anders Mörtberg (CPP, 2013)

Étude formelle d'algorithmes efficaces en algèbre linéaire. (Formal study of efficient algorithms in linear algebra). - Maxime Dénès (2013)

Foundational Property-Based Testing. - Zoe Paraskevopoulou; Catalin Hritcu; Maxime Dénès; Leonidas Lampropoulos; Benjamin C. Pierce (ITP, 2015)

Micro-Policies: Formally Verified, Tag-Based Security Monitors. - Arthur Azevedo de Amorim; Maxime Dénès; Nick Giannarakis; Catalin Hritcu; Benjamin C. Pierce; Antal Spector-Zabusky; Andrew Tolmach (IEEE Symposium on Security and Privacy, 2015)

Formalized linear algebra over Elementary Divisor Rings in Coq. - Guillaume Cano; Cyril Cohen; Maxime Dénès; Anders Mörtberg; Vincent Siles (Log. Methods Comput. Sci., 2016)

Testing noninterference, quickly. - Catalin Hritcu; Leonidas Lampropoulos; Antal Spector-Zabusky; Arthur Azevedo de Amorim; Maxime Dénès; John Hughes 001; Benjamin C. Pierce; Dimitrios Vytiniotis (J. Funct. Program., 2016)