Je suis chef de projet infrastructures logicielles en appui aux politiques publiques à Inria. Plus précisément, au sein du programme « Apollo » de l'agence de programmes dans le numérique portée par Inria, je suis responsable du projet Catala qui vise fiabiliser et moderniser les logiciels de calcul des impôts, prestations sociales, etc. basés sur des spécifications juridiques. Au delà du projet Catala, je suis toujours attentif à d'autres opportunités d'apporter mon aide et celle d'Inria à d'autres projets informatiques du secteur public qui pourraient bénéficier de l'expertise et des méthodologies de la recherche scientifique en informatique.
En effet, j'ai rejoins mon poste actuel après un début de carrière de chercheur, 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. Je suis à l'origine, avec d'autres collègues informaticiens et juristes, du langage Catala dont j'assure maintenant l'industrialisation.
denis [point] merigoux [arobase] inria [point] fr
Je tiens de manière occassionnelle 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.
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
Pour accéder à l'intégralité des compte-rendu des conseils d'administration de l'École polytechnique entre août 2013 et juin 2021, de l'Institut Polytechnique de Paris entre août 2019 et décembre 2020, et de l'ENSTA entre septembre 2017 et septembre 2019, cliquez ici.