Dagstuhl Seminar Proceedings: Mathematics, Algorithms, Proofs 2005

• Marie-Françoise Roy:
  Subdiscriminant of symmetric matrices are sums of squares.
  Electronic Edition (link) BibTeX
• César Domínguez, Dominique Duval, Laureano Lambán, Julio Rubio Garcia:
  Towards Diagrammatic Specifications of Symbolic Computation Systems.
  Electronic Edition (link) BibTeX
• Dominique Duval, Jean-Claude Reynaud:
  Diagrammatic logic and exceptions: an introduction.
  Electronic Edition (link) BibTeX
• Harold M. Edwards:
  Introduction to My Book "Essays in Constructive Mathematics".
  Electronic Edition (link) BibTeX
• Harold M. Edwards:
  Abel and the Concept of the Genus of a Curve.
  Electronic Edition (link) BibTeX
• Assia Mahboubi:
  Programming and certifying a CAD algorithm in the Coq system.
  Electronic Edition (link) BibTeX
• Paulo Oliva:
  Unifying Functional Interpretations.
  Electronic Edition (link) BibTeX
• Virgile Prevosto:
  Certified mathematical hierarchies: the FoCal system.
  Electronic Edition (link) BibTeX
• Fred Richman:
  Enabling conditions for interpolated rings.
  Electronic Edition (link) BibTeX
• Julio Rubio Garcia:
  Constructive Proofs or Constructive Statements?.
  Electronic Edition (link) BibTeX
• Carsten Schneider:
  Some Notes On "When is 0.999... equal to 1?".
  Electronic Edition (link) BibTeX
• Thierry Coquand, Henri Lombardi, Peter Schuster:
  A Nilregular Element Property.
  Electronic Edition (link) BibTeX
• Bas Spitters:
  Constructive algebraic integration theory without choice.
  Electronic Edition (link) BibTeX
• Ihsen Yengui:
  A dynamical solution of Kronecker's problem.
  Electronic Edition (link) BibTeX
• Philipp Gerhardy, Ulrich Kohlenbach:
  Generalized metatheorems on the extractability of uniform bounds in functional analysis.
  Electronic Edition (link) BibTeX
• Thomas C. Hales:
  Introduction to the Flyspeck Project.
  Electronic Edition (link) BibTeX
• Ulrich Kohlenbach, Laurentiu Leustean:
  Approximate fixed points of nonexpansive functions in product spaces.
  Electronic Edition (link) BibTeX
• Tobias Nipkow, Gertrud Bauer:
  Towards a Verified Enumeration of All Tame Plane Graphs.
  Electronic Edition (link) BibTeX
• Steven Obua:
  Proving Bounds for Real Linear Programs in Isabelle/HOL.
  Electronic Edition (link) BibTeX
• Erik Palmgren:
  Coequalisers of formal topology.
  Electronic Edition (link) BibTeX
• Hervé Perdry, Mariemi Alonso, Henri Lombardi:
  Henselian Local Rings: Around a Work in Progress.
  Electronic Edition (link) BibTeX
• Thierry Coquand:
  05021 Executive Summary -- Mathematics, Algorithms, Proofs.
  Electronic Edition (link) BibTeX
• Thierry Coquand, Henri Lombardi, Marie-Françoise Roy:
  05021 Abstracts Collection -- Mathematics, Algorithms, Proofs.
  Electronic Edition (link) BibTeX