Decorated proofs for computational effects: Exceptions

From MaRDI portal
Publication:6231626




Abstract: We define a proof system for exceptions which is close to the syntax for exceptions, in the sense that the exceptions do not appear explicitly in the type of any expression. This proof system is sound with respect to the intended denotational semantics of exceptions. With this inference system we prove several properties of exceptions.














This page was built for publication: Decorated proofs for computational effects: Exceptions

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6231626)