DROPS

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.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}
}

Document

DOI: 10.4230/DagSemProc.05021.22

Towards Diagrammatic Specifications of Symbolic Computation Systems

Authors: César Dominguez, Dominique Duval, Laureano Lamban, and Julio Rubio Garcia

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

Abstract

The aim of this work is to present an ongoing project to formalize, in the framework of diagrammatic logic (due to Dominique Duval and Christian Lair) some data structures appearing in Sergeraert's symbolic computation systems Kenzo and EAT. More precisely, we intend to translate into the diagrammatic setting a previous work based on standard algebraic specification techniques. In particular, we give hints on the reason why an important construction (called imp construction) in the specification of the systems can be understood as a freely generating functor between suitable categories of diagrammatic realizations. Even if very partial, these positive results seem to indicate that this new kind of specification is promising in the field of symbolic computation.

Cite as

César Dominguez, Dominique Duval, Laureano Lamban, and Julio Rubio Garcia. Towards Diagrammatic Specifications of Symbolic Computation Systems. In Mathematics, Algorithms, Proofs. Dagstuhl Seminar Proceedings, Volume 5021, pp. 1-23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)

Copy BibTex To Clipboard

@InProceedings{dominguez_et_al:DagSemProc.05021.22,
  author =	{Dominguez, C\'{e}sar and Duval, Dominique and Lamban, Laureano and Rubio Garcia, Julio},
  title =	{{Towards Diagrammatic Specifications of Symbolic Computation Systems}},
  booktitle =	{Mathematics, Algorithms, Proofs},
  pages =	{1--23},
  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/entities/document/10.4230/DagSemProc.05021.22},
  URN =		{urn:nbn:de:0030-drops-2927},
  doi =		{10.4230/DagSemProc.05021.22},
  annote =	{Keywords: Specification, symbolic computation, sketches, diagrammatic logic}
}

Search Results

Documents authored by Rubio Garcia, Julio

Constructive Proofs or Constructive Statements?

Abstract

Cite as

Towards Diagrammatic Specifications of Symbolic Computation Systems

Abstract

Cite as

Thanks for your feedback!

Could not send message