Dagstuhl Seminar Proceedings, Volume 5021,

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