Formalization of the Sequent Calculus' meta-theory

Début: 01-07-2018

Convention: Autres LJm Formalization

This project concerns the formalization in Coq of the meta-theory of several variants sequent calculus, generalized as the typed lambda-calculus LJm, studied since 2003.