A constructive logic behind the catch and throw mechanism (Q1337695)

The paper presents a typing system which captures the catch/throw mechanism (a programming construct for non-local exit) in the proofs-as- programs notion. The typing system is regarded as a constructive logic with facilities for exception handling. The catch/throw mechanism is handled in a natural deduction style formation in which a direct correspondence between proofs and programs can be seen. A simple programming language is defined and its operational semantics is given by a set of reduction rules. The author also introduces an abstract machine which can imitate the standard implementation of the catch/throw mechanism. To give a realizability interpretation to each typing judgement, only the fixed evaluation (call-by-value) strategy is considered. Problems of treating the catch/throw mechanism in a more general context remain unsolved. The investigation of the relationship between this mechanism and proof transformations would be an interesting problem as well.