@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}
}