Adjunctions for exceptions
Logic in Computer Science
2012-10-30 v2 Category Theory
Abstract
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.
Cite
@article{arxiv.1207.1255,
title = {Adjunctions for exceptions},
author = {Jean-Guillaume Dumas and Dominique Duval and Laurent Fousse and Jean-Claude Reynaud},
journal= {arXiv preprint arXiv:1207.1255},
year = {2012}
}
Comments
In this Version 2, minor improvements are made to Version 1