default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDNicolas Magaud
Person information
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
Books and Theses
- 2020
[b2]Nicolas Magaud:
Contributions au développement des méthodes formelles de preuves et applications à la géométrie. University of Strasbourg, France, 2020- 2003
- [b1]Nicolas Magaud:
Changements de Représentation des Données dans le Calcul des Constructions. (Changing Data Representation in the Calculus of Constructions). University of Nice Sophia Antipolis, France, 2003
Journal Articles
- 2024
- [j7]David Braun, Nicolas Magaud
, Pascal Schreck:
A Matroid-Based Automatic Prover and Coq Proof Generator for Projective Incidence Geometry. J. Autom. Reason. 68(1): 3 (2024) - 2022
- [j6]Loïc Mazo, Marie-Andrée Jacob-Da Col, Laurent Fuchs, Nicolas Magaud, Gaëlle Skapin:
Some representations of real numbers using integer sequences. Math. Struct. Comput. Sci. 32(5): 648-681 (2022) - 2019
- [j5]David Braun, Nicolas Magaud, Pascal Schreck:
Two cryptomorphic formalizations of projective incidence geometry. Ann. Math. Artif. Intell. 85(2-4): 193-212 (2019) - 2015
- [j4]Nicolas Magaud, Agathe Chollet, Laurent Fuchs:
Formalizing a discrete model of the continuum in Coq from a discrete geometry perspective. Ann. Math. Artif. Intell. 74(3-4): 309-332 (2015) - 2012
- [j3]Nicolas Magaud, Julien Narboux, Pascal Schreck:
A case study in formalizing projective geometry in Coq: Desargues theorem. Comput. Geom. 45(8): 406-424 (2012) - [j2]Christophe Brun, Jean-François Dufourd, Nicolas Magaud:
Designing and proving correct a convex hull algorithm with hypermaps in Coq. Comput. Geom. 45(8): 436-457 (2012) - 2002
- [j1]Yves Bertot, Nicolas Magaud, Paul Zimmermann:
A Proof of GMP Square Root. J. Autom. Reason. 29(3-4): 225-252 (2002)
Conference and Workshop Papers
- 2023
- [c14]Nicolas Magaud:
Towards Automatic Transformations of Coq Proof Scripts. ADG 2023: 4-10 - 2022
- [c13]Nicolas Magaud:
Proof Pearl: Formalizing Spreads and Packings of the Smallest Projective Space PG(3, 2) Using the Coq Proof Assistant. ITP 2022: 25:1-25:17 - [c12]Catherine Dubois, Nicolas Magaud, Alain Giorgetti:
Pragmatic Isomorphism Proofs Between Coq Representations: Application to Lambda-Term Families. TYPES 2022: 11:1-11:19 - 2021
- [c11]David Braun, Nicolas Magaud, Pascal Schreck:
Two New Ways to Formally Prove Dandelin-Gallucci's Theorem. ISSAC 2021: 59-66 - [c10]Nicolas Magaud:
Integrating an Automated Prover for Projective Geometry as a New Tactic in the Coq Proof Assistant. PxTP 2021: 40-47 - [c9]Pascal Schreck, Nicolas Magaud, David Braun:
Mechanization of Incidence Projective Geometry in Higher Dimensions, a Combinatorial Approach. ADG 2021: 77-90 - [c8]Nicolas Magaud:
Spreads and Packings of PG(3, 2), Formally! ADG 2021: 107-115 - 2018
- [c7]David Braun, Nicolas Magaud, Pascal Schreck:
Formalizing Some "Small" Finite Models of Projective Geometry in Coq. AISC 2018: 54-69 - 2012
- [c6]Christophe Brun, Jean-François Dufourd, Nicolas Magaud:
Formal Proof in Coq and Derivation of an Imperative Program to Compute Convex Hulls. Automated Deduction in Geometry 2012: 71-88 - 2009
- [c5]Nicolas Magaud, Julien Narboux, Pascal Schreck:
Formalizing Desargues' theorem in Coq using ranks. SAC 2009: 1110-1115 - 2008
- [c4]Nicolas Magaud, Julien Narboux, Pascal Schreck:
Formalizing Projective Plane Geometry in Coq. Automated Deduction in Geometry 2008: 141-162 - 2003
- [c3]Nicolas Magaud:
Changing Data Representation within the Coq System. TPHOLs 2003: 87-102 - 2001
- [c2]Nicolas Magaud, Yves Bertot:
Changement de représentation des structures de données en Coq: le cas des entiers naturels. JFLA 2001: 1-16 - 2000
- [c1]Nicolas Magaud, Yves Bertot:
Changing Data Structures in Type Theory: A Study of Natural Numbers. TYPES 2000: 181-196
Informal and Other Publications
- 2022
- [i1]Catherine Dubois, Nicolas Magaud, Alain Giorgetti:
Pragmatic isomorphism proofs between Coq representations: application to lambda-term families. CoRR abs/2212.10453 (2022)
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from 
to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the 
of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from 
, 
, and 
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from 
.
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-06-13 21:50 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
