The following pages link to Nicolas Magaud (Q448974):
Displaying 16 items.
- A case study in formalizing projective geometry in Coq: Desargues theorem (Q448975) (← links)
- Designing and proving correct a convex hull algorithm with hypermaps in Coq (Q448980) (← links)
- A proof of GMP square root (Q1868507) (← links)
- Formalizing a discrete model of the continuum in Coq from a discrete geometry perspective (Q2354911) (← links)
- Two cryptomorphic formalizations of projective incidence geometry (Q2631964) (← links)
- Formal Proof in Coq and Derivation of an Imperative Program to Compute Convex Hulls (Q2849508) (← links)
- Formalizing Projective Plane Geometry in Coq (Q3003232) (← links)
- Changing Data Representation within the Coq System (Q3559761) (← links)
- (Q4736398) (← links)
- Some representations of real numbers using integer sequences (Q5877245) (← links)
- A Matroid-Based Automatic Prover and Coq Proof Generator for Projective Incidence Geometry (Q6493566) (← links)
- Proof pearl: formalizing spreads and packings of the smallest projective space PG(3,2) Using the coq proof assistant (Q6572563) (← links)
- Pragmatic isomorphism proofs between Coq representations: application to lambda-term families (Q6643041) (← links)
- Mechanization of incidence projective geometry in higher dimensions, a combinatorial approach (Q6653961) (← links)
- Spreads and packings of PG(3,2), formally! (Q6653965) (← links)
- Two new ways to formally prove Dandelin-Gallucci's theorem (Q6666520) (← links)
