A constructive logic behind the catch and throw mechanism

https://doi.org/10.1016/0168-0072(94)90087-6Get rights and content
Under an Elsevier user license
open archive

Abstract

The catch/throw mechanism is a programming construct for non-local exit. In practical programming, this mechanism plays an important role when programmers handle exceptional situations. In this paper we give a typing system which captures the mechanism in the proofs-as-programs notion. The typing system can be regarded as a constructive logic with facilities for exception handling, which includes inference rules corresponding to the operations of catch and throw. We show that we can actually regard its proofs as programs which make use of the catch/throw mechanism by a natural interpretation. On one hand the catch/throw mechanism provides only a restricted access to the current continuation, on the other hand its logic is constructive, in contrast to the works due to Griffin and Murthy on more powerful facilities such as call/cc (call-with-current-continuation) of Scheme.

Cited by (0)