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.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} }
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.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} }
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.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} }
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.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} }
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.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} }
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.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} }
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.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} }
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.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} }
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.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} }
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.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} }
Dominique Duval and Jean-Claude Reynaud. Diagrammatic logic and exceptions:an introduction. In Mathematics, Algorithms, Proofs. Dagstuhl Seminar Proceedings, Volume 5021, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)
@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.} }
Fred Richman. Enabling conditions for interpolated rings. In Mathematics, Algorithms, Proofs. Dagstuhl Seminar Proceedings, Volume 5021, pp. 1-7, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)
@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} }
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.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} }
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.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} }
Harold M. Edwards. Introduction to My Book "Essays in Constructive Mathematics". In Mathematics, Algorithms, Proofs. Dagstuhl Seminar Proceedings, Volume 5021, pp. 1-2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)
@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.} }
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.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} }
Assia Mahboubi. Programming and certifying a CAD algorithm in the Coq system. In Mathematics, Algorithms, Proofs. Dagstuhl Seminar Proceedings, Volume 5021, pp. 1-18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)
@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.} }
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.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} }
Carsten Schneider. Some Notes On ``When is 0.999... equal to 1?. In Mathematics, Algorithms, Proofs. Dagstuhl Seminar Proceedings, Volume 5021, pp. 1-3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)
@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} }
Marie-Françoise Roy. Subdiscriminant of symmetric matrices are sums of squares. In Mathematics, Algorithms, Proofs. Dagstuhl Seminar Proceedings, Volume 5021, pp. 1-4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)
@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} }
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.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} }
César Dominguez, Dominique Duval, Laureano Lamban, and Julio Rubio Garcia. Towards Diagrammatic Specifications of Symbolic Computation Systems. In Mathematics, Algorithms, Proofs. Dagstuhl Seminar Proceedings, Volume 5021, pp. 1-23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)
@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} }
Paulo Oliva. Unifying Functional Interpretations. In Mathematics, Algorithms, Proofs. Dagstuhl Seminar Proceedings, Volume 5021, pp. 1-20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)
@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} }