Diagrammatic logic and exceptions:an introduction

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