research
∙
12/20/2022
Pragmatic isomorphism proofs between Coq representations: application to lambda-term families
There are several ways to formally represent families of data, such as l...
share
research
∙
01/03/2022
Spreads and Packings of PG(3,2), Formally!
We study how to formalize in the Coq proof assistant the smallest projec...
research
∙
01/03/2022
Mechanization of Incidence Projective Geometry in Higher Dimensions, a Combinatorial Approach
Several tools have been developed to enhance automation of theorem provi...
research
∙
07/06/2021