License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/DagSemProc.05021.10
URN: urn:nbn:de:0030-drops-2894
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2006/289/
Go to the corresponding Portal

Rubio Garcia, Julio

Constructive Proofs or Constructive Statements?

pdf-format:
05021.RubioGarciaJulio.ExtAbstract.289.pdf (0.09 MB)

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.

BibTeX - Entry

@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/opus/volltexte/2006/289},
  URN =		{urn:nbn:de:0030-drops-2894},
  doi =		{10.4230/DagSemProc.05021.10},
  annote =	{Keywords: Program extraction, symbolic computation, constructive logic}
}

Keywords: Program extraction, symbolic computation, constructive logic
Collection: 05021 - Mathematics, Algorithms, Proofs
Issue Date: 2006
Date of publication: 16.01.2006

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI