Catala est un langage de programmation adapté à la programmation littéraire socio-fiscale. Il permet de dériver des implémentations d'algorithmes complexes à partir de textes législatifs, en annotant chaque ligne du texte avec sa signification en termes de code. Ce dépôt contient la formalisation des séquences du langage Catala en Coq.