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

Dominguez, CÚsar ; Duval, Dominique ; Lamban, Laureano ; Rubio Garcia, Julio

Towards Diagrammatic Specifications of Symbolic Computation Systems

Document 1.pdf (514 KB)


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.

BibTeX - Entry

  author =	{C{\'e}sar Dominguez and Dominique Duval and Laureano Lamban and Julio Rubio Garcia},
  title =	{Towards Diagrammatic Specifications of Symbolic Computation Systems},
  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: Specification, symbolic computation, sketches, diagrammatic logic}

Keywords: Specification, symbolic computation, sketches, diagrammatic logic
Seminar: 05021 - Mathematics, Algorithms, Proofs
Issue Date: 2006
Date of publication: 16.01.2006

DROPS-Home | Fulltext Search | Imprint Published by LZI