Published in: Dagstuhl Seminar Proceedings, Volume 5021, Mathematics, Algorithms, Proofs (2006)
Thierry Coquand, Henri Lombardi, and Marie-Françoise Roy. 05021 Abstracts Collection – Mathematics, Algorithms, Proofs. In Mathematics, Algorithms, Proofs. Dagstuhl Seminar Proceedings, Volume 5021, pp. 1-15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)
@InProceedings{coquand_et_al:DagSemProc.05021.1, author = {Coquand, Thierry and Lombardi, Henri and Roy, Marie-Fran\c{c}oise}, title = {{05021 Abstracts Collection – Mathematics, Algorithms, Proofs}}, booktitle = {Mathematics, Algorithms, Proofs}, pages = {1--15}, series = {Dagstuhl Seminar Proceedings (DagSemProc)}, ISSN = {1862-4405}, year = {2006}, volume = {5021}, editor = {Thierry Coquand and Henri Lombardi and Marie-Fran\c{c}oise Roy}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.05021.1}, URN = {urn:nbn:de:0030-drops-3038}, doi = {10.4230/DagSemProc.05021.1}, annote = {Keywords: Constructive mathematics, computer algebra, proof systems} }
Published in: Dagstuhl Seminar Proceedings, Volume 5021, Mathematics, Algorithms, Proofs (2006)
Thierry Coquand. 05021 Executive Summary – Mathematics, Algorithms, Proofs. In Mathematics, Algorithms, Proofs. Dagstuhl Seminar Proceedings, Volume 5021, pp. 1-3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)
@InProceedings{coquand:DagSemProc.05021.2, author = {Coquand, Thierry}, title = {{05021 Executive Summary – Mathematics, Algorithms, Proofs}}, booktitle = {Mathematics, Algorithms, Proofs}, pages = {1--3}, series = {Dagstuhl Seminar Proceedings (DagSemProc)}, ISSN = {1862-4405}, year = {2006}, volume = {5021}, editor = {Thierry Coquand and Henri Lombardi and Marie-Fran\c{c}oise Roy}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.05021.2}, URN = {urn:nbn:de:0030-drops-4385}, doi = {10.4230/DagSemProc.05021.2}, annote = {Keywords: Constructive mathematics, computer algebra, proof systems} }
Published in: Dagstuhl Seminar Proceedings, Volume 5021, Mathematics, Algorithms, Proofs (2006)
Ulrich Kohlenbach and Laurentiu Leustean. Approximate fixed points of nonexpansive functions in product spaces. In Mathematics, Algorithms, Proofs. Dagstuhl Seminar Proceedings, Volume 5021, pp. 1-5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)
@InProceedings{kohlenbach_et_al:DagSemProc.05021.6, author = {Kohlenbach, Ulrich and Leustean, Laurentiu}, title = {{Approximate fixed points of nonexpansive functions in product spaces}}, booktitle = {Mathematics, Algorithms, Proofs}, pages = {1--5}, series = {Dagstuhl Seminar Proceedings (DagSemProc)}, ISSN = {1862-4405}, year = {2006}, volume = {5021}, editor = {Thierry Coquand and Henri Lombardi and Marie-Fran\c{c}oise Roy}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.05021.6}, URN = {urn:nbn:de:0030-drops-4330}, doi = {10.4230/DagSemProc.05021.6}, annote = {Keywords: Proof mining, fixed point theory, approximated fixed points, nonexpansive functions, product spaces} }
Published in: Dagstuhl Seminar Proceedings, Volume 5021, Mathematics, Algorithms, Proofs (2006)
Erik Palmgren. Coequalisers of formal topology. In Mathematics, Algorithms, Proofs. Dagstuhl Seminar Proceedings, Volume 5021, pp. 1-12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)
@InProceedings{palmgren:DagSemProc.05021.8, author = {Palmgren, Erik}, title = {{Coequalisers of formal topology}}, booktitle = {Mathematics, Algorithms, Proofs}, pages = {1--12}, series = {Dagstuhl Seminar Proceedings (DagSemProc)}, ISSN = {1862-4405}, year = {2006}, volume = {5021}, editor = {Thierry Coquand and Henri Lombardi and Marie-Fran\c{c}oise Roy}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.05021.8}, URN = {urn:nbn:de:0030-drops-4361}, doi = {10.4230/DagSemProc.05021.8}, annote = {Keywords: Formal topology, type theory} }
Published in: Dagstuhl Seminar Proceedings, Volume 5021, Mathematics, Algorithms, Proofs (2006)
Philipp Gerhardy and Ulrich Kohlenbach. Generalized metatheorems on the extractability of uniform bounds in functional analysis. In Mathematics, Algorithms, Proofs. Dagstuhl Seminar Proceedings, Volume 5021, pp. 1-5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)
@InProceedings{gerhardy_et_al:DagSemProc.05021.13, author = {Gerhardy, Philipp and Kohlenbach, Ulrich}, title = {{Generalized metatheorems on the extractability of uniform bounds in functional analysis}}, booktitle = {Mathematics, Algorithms, Proofs}, pages = {1--5}, series = {Dagstuhl Seminar Proceedings (DagSemProc)}, ISSN = {1862-4405}, year = {2006}, volume = {5021}, editor = {Thierry Coquand and Henri Lombardi and Marie-Fran\c{c}oise Roy}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.05021.13}, URN = {urn:nbn:de:0030-drops-4318}, doi = {10.4230/DagSemProc.05021.13}, annote = {Keywords: Proof mining, majorization} }
Published in: Dagstuhl Seminar Proceedings, Volume 5021, Mathematics, Algorithms, Proofs (2006)
Hervé Perdry, Mariemi Alonso, and Henri Lombardi. Henselian Local Rings: Around a Work in Progress. In Mathematics, Algorithms, Proofs. Dagstuhl Seminar Proceedings, Volume 5021, pp. 1-8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)
@InProceedings{perdry_et_al:DagSemProc.05021.14, author = {Perdry, Herv\'{e} and Alonso, Mariemi and Lombardi, Henri}, title = {{Henselian Local Rings: Around a Work in Progress}}, booktitle = {Mathematics, Algorithms, Proofs}, pages = {1--8}, series = {Dagstuhl Seminar Proceedings (DagSemProc)}, ISSN = {1862-4405}, year = {2006}, volume = {5021}, editor = {Thierry Coquand and Henri Lombardi and Marie-Fran\c{c}oise Roy}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.05021.14}, URN = {urn:nbn:de:0030-drops-4371}, doi = {10.4230/DagSemProc.05021.14}, annote = {Keywords: Local rings, henselian local rings} }
Published in: Dagstuhl Seminar Proceedings, Volume 5021, Mathematics, Algorithms, Proofs (2006)
Thomas C. Hales. Introduction to the Flyspeck Project. In Mathematics, Algorithms, Proofs. Dagstuhl Seminar Proceedings, Volume 5021, pp. 1-11, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)
@InProceedings{hales:DagSemProc.05021.16, author = {Hales, Thomas C.}, title = {{Introduction to the Flyspeck Project}}, booktitle = {Mathematics, Algorithms, Proofs}, pages = {1--11}, series = {Dagstuhl Seminar Proceedings (DagSemProc)}, ISSN = {1862-4405}, year = {2006}, volume = {5021}, editor = {Thierry Coquand and Henri Lombardi and Marie-Fran\c{c}oise Roy}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.05021.16}, URN = {urn:nbn:de:0030-drops-4329}, doi = {10.4230/DagSemProc.05021.16}, annote = {Keywords: Certified proofs, Kepler conjecture} }
Published in: Dagstuhl Seminar Proceedings, Volume 5021, Mathematics, Algorithms, Proofs (2006)
Steven Obua. Proving Bounds for Real Linear Programs in Isabelle/HOL. In Mathematics, Algorithms, Proofs. Dagstuhl Seminar Proceedings, Volume 5021, pp. 1-2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)
@InProceedings{obua:DagSemProc.05021.18, author = {Obua, Steven}, title = {{Proving Bounds for Real Linear Programs in Isabelle/HOL}}, booktitle = {Mathematics, Algorithms, Proofs}, pages = {1--2}, series = {Dagstuhl Seminar Proceedings (DagSemProc)}, ISSN = {1862-4405}, year = {2006}, volume = {5021}, editor = {Thierry Coquand and Henri Lombardi and Marie-Fran\c{c}oise Roy}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.05021.18}, URN = {urn:nbn:de:0030-drops-4351}, doi = {10.4230/DagSemProc.05021.18}, annote = {Keywords: Certified proofs, Kepler conjecture} }
Published in: Dagstuhl Seminar Proceedings, Volume 5021, Mathematics, Algorithms, Proofs (2006)
Tobias Nipkow and Gertrud Bauer. Towards a Verified Enumeration of All Tame Plane Graphs. In Mathematics, Algorithms, Proofs. Dagstuhl Seminar Proceedings, Volume 5021, pp. 1-25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)
@InProceedings{nipkow_et_al:DagSemProc.05021.21, author = {Nipkow, Tobias and Bauer, Gertrud}, title = {{Towards a Verified Enumeration of All Tame Plane Graphs}}, booktitle = {Mathematics, Algorithms, Proofs}, pages = {1--25}, series = {Dagstuhl Seminar Proceedings (DagSemProc)}, ISSN = {1862-4405}, year = {2006}, volume = {5021}, editor = {Thierry Coquand and Henri Lombardi and Marie-Fran\c{c}oise Roy}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.05021.21}, URN = {urn:nbn:de:0030-drops-4343}, doi = {10.4230/DagSemProc.05021.21}, annote = {Keywords: Kepler conjecture, certified proofs, flyspeck} }
Published in: Dagstuhl Seminar Proceedings, Volume 5021, Mathematics, Algorithms, Proofs (2006)
Ihsen Yengui. A dynamical solution of Kronecker's problem. In Mathematics, Algorithms, Proofs. Dagstuhl Seminar Proceedings, Volume 5021, pp. 1-9, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)
@InProceedings{yengui:DagSemProc.05021.3, author = {Yengui, Ihsen}, title = {{A dynamical solution of Kronecker's problem}}, booktitle = {Mathematics, Algorithms, Proofs}, pages = {1--9}, series = {Dagstuhl Seminar Proceedings (DagSemProc)}, ISSN = {1862-4405}, year = {2006}, volume = {5021}, editor = {Thierry Coquand and Henri Lombardi and Marie-Fran\c{c}oise Roy}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.05021.3}, URN = {urn:nbn:de:0030-drops-2889}, doi = {10.4230/DagSemProc.05021.3}, annote = {Keywords: Dynamical Gr\~{A}ƒ\^{A}¶bner basis, ideal membership problem, principal domains} }
Published in: Dagstuhl Seminar Proceedings, Volume 5021, Mathematics, Algorithms, Proofs (2006)
Thierry Coquand, Henri Lombardi, and Peter Schuster. A Nilregular Element Property. In Mathematics, Algorithms, Proofs. Dagstuhl Seminar Proceedings, Volume 5021, pp. 1-6, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)
@InProceedings{coquand_et_al:DagSemProc.05021.4, author = {Coquand, Thierry and Lombardi, Henri and Schuster, Peter}, title = {{A Nilregular Element Property}}, booktitle = {Mathematics, Algorithms, Proofs}, pages = {1--6}, series = {Dagstuhl Seminar Proceedings (DagSemProc)}, ISSN = {1862-4405}, year = {2006}, volume = {5021}, editor = {Thierry Coquand and Henri Lombardi and Marie-Fran\c{c}oise Roy}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.05021.4}, URN = {urn:nbn:de:0030-drops-2784}, doi = {10.4230/DagSemProc.05021.4}, annote = {Keywords: Lists of generators, polynomial ideals, Krull dimension, Zariski topology, commutative Noetherian rings, constructive algebra} }
Published in: Dagstuhl Seminar Proceedings, Volume 5021, Mathematics, Algorithms, Proofs (2006)
Harold M. Edwards. Abel and the Concept of the Genus of a Curve. In Mathematics, Algorithms, Proofs. Dagstuhl Seminar Proceedings, Volume 5021, pp. 1-2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)
@InProceedings{edwards:DagSemProc.05021.5, author = {Edwards, Harold M.}, title = {{Abel and the Concept of the Genus of a Curve}}, booktitle = {Mathematics, Algorithms, Proofs}, pages = {1--2}, series = {Dagstuhl Seminar Proceedings (DagSemProc)}, ISSN = {1862-4405}, year = {2006}, volume = {5021}, editor = {Thierry Coquand and Henri Lombardi and Marie-Fran\c{c}oise Roy}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.05021.5}, URN = {urn:nbn:de:0030-drops-2772}, doi = {10.4230/DagSemProc.05021.5}, annote = {Keywords: Constructive Mathematics} }
Published in: Dagstuhl Seminar Proceedings, Volume 5021, Mathematics, Algorithms, Proofs (2006)
Virgile Prevosto. Certified mathematical hierarchies: the FoCal system. In Mathematics, Algorithms, Proofs. Dagstuhl Seminar Proceedings, Volume 5021, pp. 1-12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)
@InProceedings{prevosto:DagSemProc.05021.7, author = {Prevosto, Virgile}, title = {{Certified mathematical hierarchies: the FoCal system}}, booktitle = {Mathematics, Algorithms, Proofs}, pages = {1--12}, series = {Dagstuhl Seminar Proceedings (DagSemProc)}, ISSN = {1862-4405}, year = {2006}, volume = {5021}, editor = {Thierry Coquand and Henri Lombardi and Marie-Fran\c{c}oise Roy}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.05021.7}, URN = {urn:nbn:de:0030-drops-2740}, doi = {10.4230/DagSemProc.05021.7}, annote = {Keywords: Specifications, proofs, inheritance, refinement, types, Focal, Coq, computer algebra, mathematics} }
Published in: Dagstuhl Seminar Proceedings, Volume 5021, Mathematics, Algorithms, Proofs (2006)
Bas Spitters. Constructive algebraic integration theory without choice. In Mathematics, Algorithms, Proofs. Dagstuhl Seminar Proceedings, Volume 5021, pp. 1-13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)
@InProceedings{spitters:DagSemProc.05021.9, author = {Spitters, Bas}, title = {{Constructive algebraic integration theory without choice}}, booktitle = {Mathematics, Algorithms, Proofs}, pages = {1--13}, series = {Dagstuhl Seminar Proceedings (DagSemProc)}, ISSN = {1862-4405}, year = {2006}, volume = {5021}, editor = {Thierry Coquand and Henri Lombardi and Marie-Fran\c{c}oise Roy}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.05021.9}, URN = {urn:nbn:de:0030-drops-2905}, doi = {10.4230/DagSemProc.05021.9}, annote = {Keywords: Algebraic integration theory, spectral theorem, choiceless constructive mathematics, pointfree topology} }
Published in: Dagstuhl Seminar Proceedings, Volume 5021, Mathematics, Algorithms, Proofs (2006)
Julio Rubio Garcia. Constructive Proofs or Constructive Statements?. In Mathematics, Algorithms, Proofs. Dagstuhl Seminar Proceedings, Volume 5021, pp. 1-4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)
@InProceedings{rubiogarcia:DagSemProc.05021.10, author = {Rubio Garcia, Julio}, title = {{Constructive Proofs or Constructive Statements?}}, booktitle = {Mathematics, Algorithms, Proofs}, pages = {1--4}, series = {Dagstuhl Seminar Proceedings (DagSemProc)}, ISSN = {1862-4405}, year = {2006}, volume = {5021}, editor = {Thierry Coquand and Henri Lombardi and Marie-Fran\c{c}oise Roy}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.05021.10}, URN = {urn:nbn:de:0030-drops-2894}, doi = {10.4230/DagSemProc.05021.10}, annote = {Keywords: Program extraction, symbolic computation, constructive logic} }
Feedback for Dagstuhl Publishing