Periodic Reporting for period 1 - ForCUTT (Formalisation of Constructive Univalent Type Theory)

There has been in the past 15 years remarkable achievements in the field of interactive theorem proving, both for checking complex software and non trivial mathematical proofs.For software correctness, X. Leroy, (INRIA and College de France), has been leading since 2006 the...