Nicolas Magaud - researchr alias

researchr

You are not signed in
Sign in
Sign up

Viewing Publication 1 - 19 from 19

2024

A Matroid-Based Automatic Prover and Coq Proof Generator for Projective Incidence GeometryDavid Braun, Nicolas Magaud, Pascal Schreck. JAR, 68(1):3, March 2024. [doi]

2022

Pragmatic Isomorphism Proofs Between Coq Representations: Application to Lambda-Term FamiliesCatherine Dubois, Nicolas Magaud, Alain Giorgetti. TYPES 2023: [doi]

Proof Pearl: Formalizing Spreads and Packings of the Smallest Projective Space PG(3, 2) Using the Coq Proof AssistantNicolas Magaud. itp 2022: [doi]

Some representations of real numbers using integer sequencesLoïc Mazo, Marie-Andrée Jacob-Da Col, Laurent Fuchs, Nicolas Magaud, Gaëlle Skapin. mscs, 32(5):648-681, May 2022. [doi]

2021

Two New Ways to Formally Prove Dandelin-Gallucci's TheoremDavid Braun, Nicolas Magaud, Pascal Schreck. issac 2021: 59-66 [doi]

2020

Contributions au développement des méthodes formelles de preuves et applications à la géométrieNicolas Magaud. 2020. [doi]

2019

Two cryptomorphic formalizations of projective incidence geometryDavid Braun, Nicolas Magaud, Pascal Schreck. AMAI, 85(2-4):193-212, 2019. [doi]

2018

Formalizing Some "Small" Finite Models of Projective Geometry in CoqDavid Braun, Nicolas Magaud, Pascal Schreck. AISC 2018: 54-69 [doi]

2015

Formalizing a discrete model of the continuum in Coq from a discrete geometry perspectiveNicolas Magaud, Agathe Chollet, Laurent Fuchs. AMAI, 74(3-4):309-332, 2015. [doi]

2012

Designing and proving correct a convex hull algorithm with hypermaps in CoqChristophe Brun, Jean-François Dufourd, Nicolas Magaud. comgeo, 45(8):436-457, 2012. [doi]

Formal Proof in Coq and Derivation of an Imperative Program to Compute Convex HullsChristophe Brun, Jean-François Dufourd, Nicolas Magaud. adg 2013: 71-88 [doi]

A case study in formalizing projective geometry in Coq: Desargues theoremNicolas Magaud, Julien Narboux, Pascal Schreck. comgeo, 45(8):406-424, 2012. [doi]

2009

Formalizing Desargues theorem in Coq using ranksNicolas Magaud, Julien Narboux, Pascal Schreck. SAC 2009: 1110-1115 [doi]

2008

Formalizing Projective Plane Geometry in CoqNicolas Magaud, Julien Narboux, Pascal Schreck. adg 2011: 141-162 [doi]

2003

Changements de Représentation des Données dans le Calcul des Constructions. (Changing Data Representation in the Calculus of Constructions)Nicolas Magaud. PhD thesis, University of Nice Sophia Antipolis, France, 2003. [doi]

Changing Data Representation within the Coq SystemNicolas Magaud. tphol 2003: 87-102 [doi]

2002

A Proof of GMP Square RootYves Bertot, Nicolas Magaud, Paul Zimmermann. JAR, 29(3-4):225-252, 2002.

2001

Changement de représentation des structures de données en Coq: le cas des entiers naturelsNicolas Magaud, Yves Bertot. jfla 2001: 1-16

2000

Changing Data Structures in Type Theory: A Study of Natural NumbersNicolas Magaud, Yves Bertot. TYPES 2002: 181-196 [doi]

Sign in or sign up to see more results.

runs on WebDSL