Formally Verified Cryptographic Web Applications in WebAssembly. - Jonathan Protzenko; Benjamin Beurdouche; Denis Merigoux; Karthikeyan Bhargavan (IACR Cryptol. ePrint Arch., 2019)

SteelCore: an extensible concurrent separation logic for effectful dependently typed programs. - Nikhil Swamy; Aseem Rastogi; Aymeric Fromherz; Denis Merigoux; Danel Ahman; Guido Martínez (Proc. ACM Program. Lang., 2020)

A modern compiler for the French tax code. - Denis Merigoux; Raphaël Monat; Jonathan Protzenko (CC, 2021)

Steel: proof-oriented programming in a dependently typed concurrent separation logic. - Aymeric Fromherz; Aseem Rastogi; Nikhil Swamy; Sydney Gibson; Guido Martínez; Denis Merigoux; Tahina Ramananandro (Proc. ACM Program. Lang., 2021)

Catala: a programming language for the law. - Denis Merigoux; Nicolas Chataing; Jonathan Protzenko (Proc. ACM Program. Lang., 2021)

Proof-oriented domain-specific language design for high-assurance software. (Design de langage dédié orienté vers la preuve pour le logiciel critique). - Denis Merigoux (2021)

Formalizing Date Arithmetic and Statically Detecting Ambiguities for the Law. - Raphaël Monat; Aymeric Fromherz; Denis Merigoux (ESOP (2), 2024)