Lean Formalization of Catala

Catala (paper) is a programming language adapted for socio-fiscal legislative literate programming. By annotating each line of the legislative text with its meaning in terms of code, one can derive an implementation of complex socio-fiscal mechanisms that enjoys a high level of assurance regarding the code-law faithfulness.

The original paper proves the correctness of its core compilation step using the F^* proof assistant. The aim of this project is to produce a proof of correctness for the same steps in Lean.

Resources:

https://book.catala-lang.org/en/

https://catala-lang.org/en/doc/formalisation

https://github.com/CatalaLang/catala

https://github.com/FStarLang/FStar