24 Search Results for "Lombardi, Henri"


Document
05021 Abstracts Collection – Mathematics, Algorithms, Proofs

Authors: Thierry Coquand, Henri Lombardi, and Marie-Françoise Roy

Published in: Dagstuhl Seminar Proceedings, Volume 5021, Mathematics, Algorithms, Proofs (2006)


Abstract
From 09.01.05 to 14.01.05, the Dagstuhl Seminar 05021 ``Mathematics, Algorithms, Proofs'' was held in the International Conference and Research Center (IBFI), Schloss Dagstuhl. During the seminar, several participants presented their current research, and ongoing work and open problems were discussed. Abstracts of the presentations given during the seminar as well as abstracts of seminar results and ideas are put together in this paper. The first section describes the seminar topics and goals in general. LinkstFo extended abstracts or full papers are provided, if available.

Cite as

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)


Copy BibTex To Clipboard

@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-dev.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}
}
Document
05021 Executive Summary – Mathematics, Algorithms, Proofs

Authors: Thierry Coquand

Published in: Dagstuhl Seminar Proceedings, Volume 5021, Mathematics, Algorithms, Proofs (2006)


Abstract
This workshop was the third MAP meeting, a continuation of the seminar "Verification and constructive algebra" held in Dagstuhl from 6 to 10 January 2003. The goal of these meetings is to bring together people from the communities of formal proofs, constructive mathematics and computer algebra (in a wide meaning). The special emphasis of the present meeting was on the constructive mathematics and efficient proofs in computer algebra.

Cite as

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)


Copy BibTex To Clipboard

@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-dev.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}
}
Document
Approximate fixed points of nonexpansive functions in product spaces

Authors: Ulrich Kohlenbach and Laurentiu Leustean

Published in: Dagstuhl Seminar Proceedings, Volume 5021, Mathematics, Algorithms, Proofs (2006)


Abstract
In this talk, we present another case study in the general program of proof mining in fixed point theory. Thus, we generalize results obtained by W. Kirk in the theory of approximated fixed points of nonexpansive mappings in product spaces

Cite as

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)


Copy BibTex To Clipboard

@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-dev.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}
}
Document
Coequalisers of formal topology

Authors: Erik Palmgren

Published in: Dagstuhl Seminar Proceedings, Volume 5021, Mathematics, Algorithms, Proofs (2006)


Abstract
We give a predicative construction of quotients of formal topologies. Along with earlier results on the match up between of continuous functions on real numbers (in the sense of Bishop's constructive mathematics) and approximable mappings on the formal space of reals, we argue that formal topology gives an adequate foundation for constructive algebraic topology, also in the predicative sense. Predicativity is of essence when formalising the subject in logical frameworks based on Martin-Löf type theories.

Cite as

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)


Copy BibTex To Clipboard

@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-dev.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}
}
Document
Generalized metatheorems on the extractability of uniform bounds in functional analysis

Authors: Philipp Gerhardy and Ulrich Kohlenbach

Published in: Dagstuhl Seminar Proceedings, Volume 5021, Mathematics, Algorithms, Proofs (2006)


Abstract
Recently U.Kohlenbach proved general metatheorems for the extraction of (uniform) bounds from classical proofs in functional analysis. The proof was based on a combination of Gödel's functional interpretation and Bezem's strong majorization relation. We present a generalization of the majorization relation which allows to generalize Kohlenbach's metatheorems significantly. Finally, we will discuss some examples which are now covered by the new metatheorems.

Cite as

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)


Copy BibTex To Clipboard

@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-dev.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}
}
Document
Henselian Local Rings: Around a Work in Progress

Authors: Hervé Perdry, Mariemi Alonso, and Henri Lombardi

Published in: Dagstuhl Seminar Proceedings, Volume 5021, Mathematics, Algorithms, Proofs (2006)


Abstract
I shall outline an elementary and effective construction of the Henselization of a local ring (which could be implemented in some computer algebra systems) and an effective proof of several classical results about Henselian local rings.

Cite as

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)


Copy BibTex To Clipboard

@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-dev.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}
}
Document
Introduction to the Flyspeck Project

Authors: Thomas C. Hales

Published in: Dagstuhl Seminar Proceedings, Volume 5021, Mathematics, Algorithms, Proofs (2006)


Abstract
This article gives an introduction to a long-term project called Flyspeck, whose purpose is to give a formal verification of the Kepler Conjecture. The Kepler Conjecture asserts that the density of a packing of equal radius balls in three dimensions cannot exceed $pi/sqrt{18}$. The original proof of the Kepler Conjecture, from 1998, relies extensively on computer calculations. Because the proof relies on relatively few external results, it is a natural choice for a formalization effort.

Cite as

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)


Copy BibTex To Clipboard

@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-dev.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}
}
Document
Proving Bounds for Real Linear Programs in Isabelle/HOL

Authors: Steven Obua

Published in: Dagstuhl Seminar Proceedings, Volume 5021, Mathematics, Algorithms, Proofs (2006)


Abstract
Linear programming is a basic mathematical technique for optimizing a linear function on a domain that is constrained by linear inequalities. We restrict ourselves to linear programs on bounded domains that involve only real variables. In the context of theorem proving, this restriction makes it possible for any given linear program to obtain certificates from external linear programming tools that help to prove arbitrarily precise bounds for the given linear program. To this end, an explicit formalization of matrices in Isabelle/HOL is presented, and how the concept of lattice-ordered rings allows for a smooth integration of matrices with the axiomatic type classes of Isabelle. As our work is a contribution to the Flyspeck project, we demonstrate that via reflection and with the above techniques it is now possible to prove bounds for the linear programs arising in the proof of the Kepler conjecture sufficiently fast.

Cite as

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)


Copy BibTex To Clipboard

@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-dev.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}
}
Document
Towards a Verified Enumeration of All Tame Plane Graphs

Authors: Tobias Nipkow and Gertrud Bauer

Published in: Dagstuhl Seminar Proceedings, Volume 5021, Mathematics, Algorithms, Proofs (2006)


Abstract
In his proof of the Kepler conjecture, Thomas Hales introduced the notion of tame graphs and provided a Java program for enumerating all tame plane graphs. We have translated his Java program into an executable function in HOL ("the generator"), have formalized the notions of tameness and planarity in HOL, and have partially proved that the generator returns all tame plane graphs. Running the generator in ML has shows that the list of plane tame graphs ("the archive") that Thomas Hales also provides is complete. Once we have finished the completeness proof for the generator. In addition we checked the redundancy of the archive by formalising an executable notion of isomorphism between plane graphs, and checking if the archive contains only graphs produced by the generator. It turned out that 2257 of the 5128 graphs in the archive are either not tame or isomorphic to another graph in the archive.

Cite as

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)


Copy BibTex To Clipboard

@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-dev.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}
}
Document
A dynamical solution of Kronecker's problem

Authors: Ihsen Yengui

Published in: Dagstuhl Seminar Proceedings, Volume 5021, Mathematics, Algorithms, Proofs (2006)


Abstract
In this paper, I present a new decision procedure for the ideal membership problem for polynomial rings over principal domains using discrete valuation domains. As a particular case, I solve a fundamental algorithmic question in the theory of multivariate polynomials over the integers called ``Kronecker's problem", that is the problem of finding a decision procedure for the ideal membership problem for $mathbb{Z}[X_1,ldots, X_n]$. The techniques utilized are easily generalizable to Dedekind domains. In order to avoid the expensive complete factorization in the basic principal ring, I introduce the notion of ``dynamical Gr"obner bases" of polynomial ideals over a principal domain. As application, I give an alternative dynamical solution to ``Kronecker's problem".

Cite as

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)


Copy BibTex To Clipboard

@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-dev.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}
}
Document
A Nilregular Element Property

Authors: Thierry Coquand, Henri Lombardi, and Peter Schuster

Published in: Dagstuhl Seminar Proceedings, Volume 5021, Mathematics, Algorithms, Proofs (2006)


Abstract
An element or an ideal of a commutative ring is nilregular if and only if it is regular modulo the nilradical. We prove that if the ring is Noetherian, then every nilregular ideal contains a nilregular element. In constructive mathematics, this proof can then be seen as an algorithm to produce nilregular elements of nilregular ideals whenever the ring is coherent, Noetherian, and discrete. As an application, we give a constructive proof of the Eisenbud--Evans--Storch theorem that every algebraic set in $n$--dimensional affine space is the intersection of $n$ hypersurfaces. The input of the algorithm is an arbitrary finite list of polynomials, which need not arrive in a special form such as a Gr"obner basis. We dispense with prime ideals when defining concepts or carrying out proofs.

Cite as

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)


Copy BibTex To Clipboard

@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-dev.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}
}
Document
Abel and the Concept of the Genus of a Curve

Authors: Harold M. Edwards

Published in: Dagstuhl Seminar Proceedings, Volume 5021, Mathematics, Algorithms, Proofs (2006)


Abstract
This talk is about the treatement of the Genus of a Curve by Abel, following the book "Essays in Constructive Mathematics".

Cite as

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)


Copy BibTex To Clipboard

@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-dev.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}
}
Document
Certified mathematical hierarchies: the FoCal system

Authors: Virgile Prevosto

Published in: Dagstuhl Seminar Proceedings, Volume 5021, Mathematics, Algorithms, Proofs (2006)


Abstract
The focal language (formerly Foc) allows a programmer to incrementally build mathematical structures and to formally prove their correctness. focal encourages a development process by refinement, deriving step-by-step implementations from specifications. This refinement process is realized using an inheritance mechanism on structures which can mix primitive operations, axioms, algorithms and proofs. Inheritance from existing structures allows to reuse their components under some conditions, which are statically checked by the compiler. In this talk, we first present the main constructions of the language. Then we show a shallow embedding of these constructions in the Coq proof assistant, which is used to check the proofs made in Focal. Such a proof can be either an hand-written Coq script, made in an environment set up by the Focal compiler, or a Coq term given the zenon theorem prover, which is partly developped within Focal. Last, we present a formalization of focal structures and show that the Coq embedding is conform to this model.

Cite as

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)


Copy BibTex To Clipboard

@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-dev.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}
}
Document
Constructive algebraic integration theory without choice

Authors: Bas Spitters

Published in: Dagstuhl Seminar Proceedings, Volume 5021, Mathematics, Algorithms, Proofs (2006)


Abstract
We present a constructive algebraic integration theory. The theory is constructive in the sense of Bishop, however we avoid the axiom of countable, or dependent, choice. Thus our results can be interpreted in any topos. Since we avoid impredicative methods the results may also be interpreted in Martin-Löf type theory or in a predicative topos in the sense of Moerdijk and Palmgren. We outline how to develop most of Bishop's theorems on integration theory that do not mention points explicitly. Coquand's constructive version of the Stone representation theorem is an important tool in this process. It is also used to give a new proof of Bishop's spectral theorem.

Cite as

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)


Copy BibTex To Clipboard

@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-dev.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}
}
Document
Constructive Proofs or Constructive Statements?

Authors: Julio Rubio Garcia

Published in: Dagstuhl Seminar Proceedings, Volume 5021, Mathematics, Algorithms, Proofs (2006)


Abstract
A question raised at previous MAP meetings is the following. Is Sergeraert's "Constructive Algebraic Topology" (CAT, in short) really constructive (in the strict logical sense of the word "constructive")? We have not an answer to that question, but we are interested in the following: could have a positive (or negative) answer to the previous question an influence in the problem of proving the correctness of CAT programs (as Kenzo)? Studying this problem, we have observed that, in fact, many CAT programs can be extracted from the statements (that is, from the specification of certain objects and constructions), without needing an extraction from proofs. This remark shows that the logic used in the proofs is uncoupled with respect to the correctness of programs. Thus, the first question posed could be quite irrelevant from the practical point of view. These rather speculative ideas will be illustrated by means of some elementary examples, where the Isabelle code extraction tool can be successfully applied.

Cite as

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)


Copy BibTex To Clipboard

@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-dev.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}
}
  • Refine by Author
  • 4 Coquand, Thierry
  • 4 Lombardi, Henri
  • 3 Roy, Marie-Françoise
  • 2 Duval, Dominique
  • 2 Edwards, Harold M.
  • Show More...

  • Refine by Classification

  • Refine by Keyword
  • 4 computer algebra
  • 3 Kepler conjecture
  • 2 Certified proofs
  • 2 Constructive Mathematics
  • 2 Constructive mathematics
  • Show More...

  • Refine by Type
  • 24 document

  • Refine by Publication Year
  • 23 2006
  • 1 2004

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail