When quoting this document, please refer to the following
URN: urn:nbn:de:0030-drops-2894
Go to the corresponding Portal

Rubio Garcia, Julio

Constructive Proofs or Constructive Statements?

05021.RubioGarciaJulio.ExtAbstract.289.pdf (0.09 MB)


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

  author =	{Julio Rubio Garcia},
  title =	{Constructive Proofs or Constructive Statements?},
  booktitle =	{Mathematics, Algorithms, Proofs},
  year =	{2006},
  editor =	{Thierry Coquand and Henri Lombardi and Marie-Fran{\c{c}}oise Roy},
  number =	{05021},
  series =	{Dagstuhl Seminar Proceedings},
  ISSN =	{1862-4405},
  publisher =	{Internationales Begegnungs- und Forschungszentrum f{\"u}r Informatik (IBFI), Schloss Dagstuhl, Germany},
  address =	{Dagstuhl, Germany},
  URL =		{},
  annote =	{Keywords: Program extraction, symbolic computation, constructive logic}

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

DROPS-Home | Fulltext Search | Imprint Published by LZI