  An algebraic method is used to study the semantics of exceptions in computer
languages. The exceptions form a computational effect, in the sense that there
is an apparent mismatch between the syntax of exceptions and their intended
semantics. We solve this apparent contradiction by efining a logic for
exceptions with a proof system which is close to their syntax and where their
intended semantics can be seen as a model. This requires a robust framework for
logics and their morphisms, which is provided by categorical tools relying on
adjunctions, fractions and limit sketches.
