Search Results

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