DROPS

Document

Diagrammatic logic and exceptions:an introduction

Authors: Dominique Duval and Jean-Claude Reynaud

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

Abstract

For dealing with computational effects in computer science, it may be helpful to use several logics: typically, a logic with implicit effects for the language, and a more classical logic for the user. Hence, the study of computational effects should take place in a framework where distinct logics can be related. In this paper, such a framework is presented: it is a category, called the category of propagators. Each propagator defines a kind of logic, called a diagrammatic logic, which is endowed with a deduction system and a sound notion of models. Morphisms of propagators provide the required relationships between diagrammatic logics. The category of propagators has been introduced by Duval and Lair in 2002, it is based on the notion of sketches, which is due to Ehresmann in the 1960's. Then, the paper outlines how Duval and Reynaud in 2004 used the category of propagators for dealing with the computational effect of raising and handling exceptions. Another application of diagrammatic logic is presented by Dominguez et al. in the same conference

Cite as

Dominique Duval and Jean-Claude Reynaud. Diagrammatic logic and exceptions:an introduction. In Mathematics, Algorithms, Proofs. Dagstuhl Seminar Proceedings, Volume 5021, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)

Copy BibTex To Clipboard

@InProceedings{duval_et_al:DagSemProc.05021.11,
  author =	{Duval, Dominique and Reynaud, Jean-Claude},
  title =	{{Diagrammatic logic and exceptions:an introduction}},
  booktitle =	{Mathematics, Algorithms, Proofs},
  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.11},
  URN =		{urn:nbn:de:0030-drops-2931},
  doi =		{10.4230/DagSemProc.05021.11},
  annote =	{Keywords: Specifications, Semantics, Exceptions, Sketches, Diagrammatic Logic, Extensive Categories, Monads.}
}

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 Duval, Dominique

Diagrammatic logic and exceptions:an introduction

Abstract

Cite as

Towards Diagrammatic Specifications of Symbolic Computation Systems

Abstract

Cite as

Thanks for your feedback!

Could not send message