@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.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}
}
@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.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}
}
@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.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}
}
@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.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}
}
@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.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}
}
@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.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}
}
@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.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}
}
@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.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}
}
@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.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}
}
@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.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}
}
@InProceedings{duval_et_al:DagSemProc.05021.11,
author = {Duval, Dominique and Reynaud, Jean-Claude},
title = {{Diagrammatic logic and exceptions:an introduction}},
booktitle = {Mathematics, Algorithms, Proofs},
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.dagstuhl.de/entities/document/10.4230/DagSemProc.05021.11},
URN = {urn:nbn:de:0030-drops-2931},
doi = {10.4230/DagSemProc.05021.11},
annote = {Keywords: Specifications, Semantics, Exceptions, Sketches, Diagrammatic Logic, Extensive Categories, Monads.}
}
@InProceedings{richman:DagSemProc.05021.12,
author = {Richman, Fred},
title = {{Enabling conditions for interpolated rings}},
booktitle = {Mathematics, Algorithms, Proofs},
pages = {1--7},
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.dagstuhl.de/entities/document/10.4230/DagSemProc.05021.12},
URN = {urn:nbn:de:0030-drops-2792},
doi = {10.4230/DagSemProc.05021.12},
annote = {Keywords: Brouwerian example, interpolated ring, intuitionistic algebra}
}
@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.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}
}
@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.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}
}
@InProceedings{edwards:DagSemProc.05021.15,
author = {Edwards, Harold M.},
title = {{Introduction to My Book "Essays in Constructive Mathematics"}},
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.dagstuhl.de/entities/document/10.4230/DagSemProc.05021.15},
URN = {urn:nbn:de:0030-drops-2801},
doi = {10.4230/DagSemProc.05021.15},
annote = {Keywords: Constructive Mathematics, Galois Theory, Genus of a Curve.}
}
@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.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}
}
@InProceedings{mahboubi:DagSemProc.05021.17,
author = {Mahboubi, Assia},
title = {{Programming and certifying a CAD algorithm in the Coq system}},
booktitle = {Mathematics, Algorithms, Proofs},
pages = {1--18},
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.dagstuhl.de/entities/document/10.4230/DagSemProc.05021.17},
URN = {urn:nbn:de:0030-drops-2763},
doi = {10.4230/DagSemProc.05021.17},
annote = {Keywords: Computer algebra, Bernstein polynomials, subresultants, CAD, Coq, certification.}
}
@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.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}
}
@InProceedings{schneider:DagSemProc.05021.19,
author = {Schneider, Carsten},
title = {{Some Notes On ``When is 0.999... equal to 1?}},
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.dagstuhl.de/entities/document/10.4230/DagSemProc.05021.19},
URN = {urn:nbn:de:0030-drops-2755},
doi = {10.4230/DagSemProc.05021.19},
annote = {Keywords: Symbolic summation, computer algebra, proofs, harmonic numbers, zeta-relations}
}
@InProceedings{roy:DagSemProc.05021.20,
author = {Roy, Marie-Fran\c{c}oise},
title = {{Subdiscriminant of symmetric matrices are sums of squares}},
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.dagstuhl.de/entities/document/10.4230/DagSemProc.05021.20},
URN = {urn:nbn:de:0030-drops-3471},
doi = {10.4230/DagSemProc.05021.20},
annote = {Keywords: Real algebra, sums of squares, subdiscriminants}
}
@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.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}
}
@InProceedings{dominguez_et_al:DagSemProc.05021.22,
author = {Dominguez, C\'{e}sar and Duval, Dominique and Lamban, Laureano and Rubio Garcia, Julio},
title = {{Towards Diagrammatic Specifications of Symbolic Computation Systems}},
booktitle = {Mathematics, Algorithms, Proofs},
pages = {1--23},
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.dagstuhl.de/entities/document/10.4230/DagSemProc.05021.22},
URN = {urn:nbn:de:0030-drops-2927},
doi = {10.4230/DagSemProc.05021.22},
annote = {Keywords: Specification, symbolic computation, sketches, diagrammatic logic}
}
@InProceedings{oliva:DagSemProc.05021.23,
author = {Oliva, Paulo},
title = {{Unifying Functional Interpretations}},
booktitle = {Mathematics, Algorithms, Proofs},
pages = {1--20},
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.dagstuhl.de/entities/document/10.4230/DagSemProc.05021.23},
URN = {urn:nbn:de:0030-drops-2919},
doi = {10.4230/DagSemProc.05021.23},
annote = {Keywords: Functional interpretation, modified realizability, Dialectica interpretation, intuitionistic logic}
}
The metadata provided by Dagstuhl Publishing on its webpages, as well as their export formats (such as XML or BibTeX) available at our website, is released under the CC0 1.0 Public Domain Dedication license. That is, you are free to copy, distribute, use, modify, transform, build upon, and produce derived works from our data, even for commercial purposes, all without asking permission. Of course, we are always happy if you provide a link to us as the source of the data.
Read the full CC0 1.0 legal code for the exact terms that apply: https://creativecommons.org/publicdomain/zero/1.0/legalcode
Feedback for Dagstuhl Publishing