Decorated proofs for computational effects: Exceptions

TL;DR

This paper introduces a proof system for exceptions that aligns closely with their syntax, enabling formal reasoning about exceptions without explicitly including them in expression types, and proves its soundness and properties.

Contribution

The paper presents a novel proof system for exceptions that is syntactically close to exception syntax and is sound with respect to their denotational semantics.

Findings

Proof system for exceptions is sound.

Properties of exceptions are formally proven.

Exceptions do not appear explicitly in expression types.

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.