Je suis chercheur junior à l'Inria au sein de l'équipe Prosecco. Je suis spécialisé dans l'étude des langages de programmations et de la vérification formelle. Mon domaine de recherche est à l'intersection de l'informatique et du droit: mon but est d'améliorer la manière dont la loi traduite en code est appliquée automatiquement par les systèmes informatiques des administrations et entreprises. Dans ce cadre, je collabore avec la DGFiP sur le projet Mlang et je suis à l'origine du langage Catala (voir plus bas).
Vous pouvez me contacter sur
denis [point] merigoux [arobase] inria [point] fr
Je tiens de manière plus ou moins régulière un blog pédagogique autour des langages de programmation et de leur implémentation, à destination de tous ceux qui programment sans savoir comment les choses marchent sous le capot.
Pour l'instant, je n'ai pas d'offre de recrutement particulière à partager. Cependant, n'hésitez pas à me contacter si vous êtes informaticien·ne (voire programm·eur·euse fonctionnel·le) ou juriste (voire spécialiste en fiscalité ou droit des prestations sociales), et intéressé·e pour travailler autour du projet Catala (voir ci-dessous).
À partir de début 2020, j'ai lancé le projet Catala afin de répondre à l'absence d'outils reposant sur une base formelle afin de transformer la loi en code. Fruit d'une collaboration internationale et interdisciplinaire (avec des juristes), Catala se veut être un langage dédié de qualité industrielle pour la production de code garanti fidèle à une spécification législative ou réglementaire.
Mlang est un compilateur pour le langage M de la Direction Générale des Finances Publiques (DGFiP). Créé au printemps 2019, j'en suis l'auteur principal. Le but du projet est de répliquer le calcul de l'impôt sur le revenu afin de le distribuer dans d'autres langages de programmation et de l'analyser formellement. Voir mon billet de blog à ce sujet.
Steel est le framework de logique de séparation pour F*. Après avoir contribué intensivement pendant l'été 2019 en collaboration avec des chercheurs de Microsoft Research, je me suis spécialisé sur le modèle mémoire ainsi que la future extraction vers C.
De février 2018 à la fin de l'année 2018, j'ai contribué à l'écriture d'une implémentation du protocole cryptographique Signal en F*. J'ai plus particulièrement travaillé sur l'extraction de Signal* vers WebAssembly et son interopérabilité avec le code Javascript, afin de passer la suite de tests complète de l'implémentation officielle de Signal.
Lors d'un deuxième stage à Mozilla en 2018, j'ai contribué à l'architecture du compilateur Rust. En lien avec mon précédent stage sur Cranelift, j'ai refactorisé le bout de la chaîne de compilation afin de pouvoir cibler plusieurs backends de génération de code machine, enlevant ainsi la dépendance dure du compilateur Rust à LLVM.
J'ai contribué pendant l'été 2017 à Cranelift, générateur de code machine écrit en Rust basé sur une représentation intermédiaire proche de WebAssembly. Plus particulièrement, j'ai écrit la traduction de WebAssembly vers Cranelift IR.
Coccinelle est un outil de refactoring sémantique de code C utilisé par la communauté du noyau Linux. Au printemps 2016, j'ai conçu un nouvel outil, Spinfer, analysant des commits de code et inférant des règles SmPL de transformation. Le fonctionnement de Spinfer est détaillé dans mon rapport de stage
Recueil de fiches de cours de Terminale S et de MPSI (ancien programme), pour les mathématiques et la physique.
Pour accéder à l'intégralité des compte-rendu des conseils d'administration de l'École polytechnique entre août 2013 et juin 2021, cliquez ici.
Pour accéder à l'intégralité des compte-rendu des conseils d'administration de l'Institut Polytechnique de Paris août 2019 et décembre 2020, cliquez ici.
Pour accéder à l'intégralité des compte-rendu des conseils d'administration de l'ENSTA entre septembre 2017 et septembre 2019, cliquez ici.