AVoCat

Catala est un nouveau langage de programmation, conçu pour être compréhensible par les juristes et suivre la structure des textes législatifs afin de transformer la loi en code. Nous proposons d’explorer la vérification automatique de programmes Catala, afin d’obtenir des outils prouvant formellement que les lois fiscales et sociales satisfont des propriétés de sûreté et de correction, générant des contre-exemples concrets le cas échéant. Ces outils ont vocations à être utilisés par les juristes et informaticiens qui, au sein des administrations, traduisent le droit en code informatique afin de l'appliquer automatiquement à des échelles massives ou à des fins de modélisation économique.