Diagrammatic logic and effects : the example of exceptions
Résumé
This paper presents a unified framework for dealing with exceptions in axiomatic specifications and in programming languages. Our framework includes a deduction system and a denotational semantics with respect to a diagrammatic logic \cite{DL,Du}. This approach can be seen as an alternative to the monads approach for introducing effects in specifications and in programs \cite{Mo}; for instance, our denotational semantics is related to the monadic semantics of exceptions by an adjunction result between two different logics. Moreover, in order to build upon a realistic computational model, we use extensive categories as a minimal requirement to express our various logical theories.