Séminaire Cambium, Inria Paris, 2 rue Simone Iff
                          Salle Lions 1, bâtiment C
                           Vendredi 29 mars, 10h30

                      Aymeric Fromherz et Denis Merigoux
                                 Inria Paris

                         Formalizing Date Arithmetic
               and Statically Detecting Ambiguities for the Law

Legal expert systems routinely rely on date computations to determine
the eligibility of a citizen to social benefits or whether an
application has been filed on time. Unfortunately, date arithmetic
exhibits many corner cases, which are handled differently from one
library to the other, making faithfully transcribing the law into code
error-prone, and possibly leading to heavy financial and legal
consequences for users. In this work, we aim to provide a solid
foundation for date arithmetic working on days, months and years, and
to integrate it into Catala, a recent domain-specific language for
formalizing computational law.

After a presentation of the Catala langauge and recent news on the
project, we will present a novel, formal semantics for date
computations, and formally establish several semantic properties
through a mechanization in the F* proof assistant. Building upon this
semantics, we then propose a static analysis by abstract
interpretation to automatically detect ambiguities in date
computations. We finally implement our approach for Catala, and use it
to analyze the Catala implementation of the French housing benefits,
leading to the discovery of several date-related ambiguities.

            Vous pouvez vous abonner à nos annonces de séminaires:
                     http://cambium.inria.fr/seminar.html

             Nos séminaires sont accessibles en ligne en direct
                            via le lien ci-dessus.