Skip to Main content Skip to Navigation
Conference papers

Étude formelle de l'implémentation du code des impôts

Abstract : The tax code, as a legislative text, defines a mathematical function that computes the income tax of a fiscal household. In order to collect taxes, this function is implemented as an algorithm by the Direction Générale des Finances Publiques (DGFiP), using a domain specific language called M (standing for "Macro-language"). We propose a formal semantics of the M language, tested thanks to data published by the DGFiP. This formalization, coupled with the public release by the DGFiP of the codebase used to compute the income tax, allowed us to produce a fully formalized artifact encoding the fragment of the tax code describing the income tax computation. We demonstrate the usefulness of such a formalization thanks to a prototype that uses an SMT solver to infer meta-properties on the income tax computation. These meta-properties could complete and refine the existing economical analysis of the redistributive effects of the income tax, as well as various social benefits. More generally, a systematic formalization of the algorithmic fragments of the law would raise the assurance level on the coherence of the French socio-fiscal system. This work has led to the development of three software artifacts: a mechanized semantics for M, an interpreter and compiler for M based on this semantics (written in OCaml), and a Python prototype of encoding the income tax computation into the Z3 SMT solver.
Document type :
Conference papers
Complete list of metadata

Cited literature [17 references]  Display  Hide  Download
Contributor : Denis Merigoux Connect in order to contact the contributor
Submitted on : Saturday, December 28, 2019 - 6:26:40 PM
Last modification on : Tuesday, January 11, 2022 - 11:16:05 AM
Long-term archiving on: : Sunday, March 29, 2020 - 12:35:31 PM


Files produced by the author(s)


  • HAL Id : hal-02320347, version 3


Denis Merigoux, Raphaël Monat, Christophe Gaie. Étude formelle de l'implémentation du code des impôts. JFLA 2020 - 31ème Journées Francophones des Langages Applicatifs, Jan 2020, Gruissan, France. ⟨hal-02320347v3⟩



Les métriques sont temporairement indisponibles