2 citations · 3 across the 5 of their papers we have counts for
Showing 2022Show all
3 papers · 1 filter
cs.LO2022
Pragmatic isomorphism proofs between Coq representations: application to lambda-term families
Catherine Dubois, Nicolas Magaud, Alain Giorgetti
There are several ways to formally represent families of data, such as lambda terms, in a type theory such as the dependent type theory of Coq. Mathematical representations are ver…
cs.LO2022
Spreads and Packings of PG(3,2), Formally!
Nicolas Magaud
We study how to formalize in the Coq proof assistant the smallest projective space PG(3,2). We then describe formally the spreads and packings of PG(3,2), as well as some of their…
cs.CG2022★ 2 cited
Mechanization of Incidence Projective Geometry in Higher Dimensions, a Combinatorial Approach
Pascal Schreck, Nicolas Magaud, David Braun
Several tools have been developed to enhance automation of theorem proving in the 2D plane. However, in 3D, only a few approaches have been studied, and to our knowledge, nothing h…