3 papers
cs.PL2021
Catala: A Programming Language for the Law
Denis Merigoux, Nicolas Chataing, Jonathan Protzenko
Law at large underpins modern society, codifying and governing many aspects of citizens' daily lives. Oftentimes, law is subject to interpretation, debate and challenges throughout…
cs.PL2020
A Modern Compiler for the French Tax Code
Denis Merigoux, Raphaël Monat, Jonathan Protzenko
In France, income tax is computed from taxpayers' individual returns, using an algorithm that is authored, designed and maintained by the French Public Finances Directorate (DGFiP)…
cs.PL2018
Meta-F*: Proof Automation with SMT, Tactics, and Metaprograms
Guido Martínez, Danel Ahman, Victor Dumitrescu +10
We introduce Meta-F*, a tactics and metaprogramming framework for the F* program verifier. The main novelty of Meta-F* is allowing the use of tactics and metaprogramming to dischar…