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.
Complete list of metadatas

Cited literature [17 references]  Display  Hide  Download

https://hal.inria.fr/hal-02320347
Contributor : Denis Merigoux <>
Submitted on : Saturday, December 28, 2019 - 6:26:40 PM
Last modification on : Thursday, January 30, 2020 - 6:39:49 PM
Document(s) archivé(s) le : Sunday, March 29, 2020 - 12:35:31 PM

File

main.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-02320347, version 3

Citation

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

Share

Metrics

Record views

466

Files downloads

1107