| CARVIEW |
À propos
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 rejoint 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.
Contact
denis [point] merigoux [arobase] inria [point] fr
Blog
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.
Offres d'emploi
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.
Anciens projets
Mlang
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
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.
Signal*
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.
Le compilateur Rust
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.
Cranelift
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.
Spinfer
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
Étudiant·e·s encadré·e·s
- Justine Banuls (stage en janvier-juin 2023), maintenant avocate ;
- Alain Delaët-Tixeuil (doctorant depuis fin 2022), co-encadré avec Sandrine Blazy ;
- Émile Rolley (stage en mars-août 2022), maintenant développeur logiciel ;
- Lilya Slimani (stage en mars-juin 2022), maintenant avocate ;
- Nicolas Chataing (stage en mars-août 2020), maintenant ingénieur logiciel.
Publications
Documents administratifs
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.
About me
I am a project manager for software infrastructures in support of public policies at Inria. More specifically, as part of the “Apollo” program of Inria's digital programs agency, I'm in charge of the Catala project, which aims to modernize and make more reliable software for calculating taxes, social benefits, etc., based on legal specifications. Beyond the Catala project, I'm always on the lookout for other opportunities to bring my help and that of Inria to other public sector IT projects that could benefit from the expertise and methodologies of scientific research in computer science.
Indeed, I joined my current position after an early career as a researcher, specializing in the study of programming languages and formal verification. My field of research is at the intersection of computer science and law: my aim is to improve the way in which the law translated into code is automatically applied by the computer systems of administrations and companies. Along with other Computer Science and Law colleagues, I've created of the Catala language, which I am now responsible for industrializing.
Contact
denis [dot] merigoux [at] inria [dot] fr
Blog
I occasionally keep a blog to explain programming languages and verification-related topics to people that use computers but always wondered how it worked under the hood.
Offers
For now, I don't have any job posting to share. However, please contact me if you are a computer scientist (better, a functional programmer) or a lawyer (better, specialized in tax or social benefits law), and are interested in working around the Catala project.
Old projects
Mlang
Mlang is a compiler for the M language used at the French Directorate for Public Finances (DGFiP). The goal of Mlanfg is to replicate the computation of the French income tax in order to distribute it in other programming languages, and to analyse it formally. See my blog post for more details.
Steel
Steel is F*'s separation logic framework. After a period of intense contribution in the Summer of 2019, collaborating with Microsoft Research people, I specialized in the memory model architecture and the future extraction to C.
Signal*
From February 2018 to the end of 2018, I contributed to an F* implementation of the Signal cryptographic protocol en F*. Additionaly, I worked on the extraction of Signal* to WebAssembly and its interoperability with the Javascript calling context, in order to pass the whole Signal test suite.
The Rust compiler
During a second internship at Mozilla in 2018, I contributed to the Rust compiler. With the objective of using Cranelift inside the Rust compiler, I refactored the code generation part of the compiler so that it could target multiple backends, instead of the hardcoded dependency to LLVM.
Cranelift
During Summer 2017, I contributed to Cranelift, a machine code generator written in Rust and based on an intermediate representation close to WebAssembly. More specifically, I wrote the translation from WebAssembly to Cranelift IR.
Spinfer
Coccinelle is a tool for semantic refactoring of C code, used by the Linux kernel community. During Spring 2016, I designed a new tool, Spinfer, that analyses code commits and infers semantic transformation rules written in SmPL de transformation. The details are explained in a technical report.
Students
- Justine Banuls (internship in January-June 2023), now a laywer ;
- Alain Delaët-Tixeuil (PhD candidate since the end of 2022), co-advised with Sandrine Blazy ;
- Émile Rolley (intership en March-August 2022), now a software developer ;
- Lilya Slimani (internship in March-June 2022), now a lawyer ;
- Nicolas Chataing (internship in March-August 2020), now a software engineer.