A Constructive Formalization of
the Catch and Throw Mechanism
Hiroshi Nakano
Faculty of Science and Technology
Ryukoku University
Seta, Otsu, 520-21, Japannakano@rins.ryukoku.ac.jp

Abstract
The catch/throw mechanism is a programming construct for non-local exit. In the practical programming,
this mechanism plays an important role when programmers handle exceptional situations. In this paper wegive a constructive formalization which captures themechanism in the proofs-as-programs notion. We introduce a modi ed version of LJ equipped with inference rules corresponding to the operations of catch andthrow. Then we show that we can actually extract programs which make use of the catch/throw mechanism
from proofs under a certain realizability interpretation.
Although the catch/throw mechanism provides only a
restricted access to the current continuation, the formulation remains constructive in contrast to the works
due to Grin and Murthy on more powerful facilities such as call/cc (call-with-current-continuation) of
Scheme.
1 Introduction

The catch/throw mechanism provides a facility for
non-local exit. We can nd examples of the mechanism in some practical programming languages suchas C-language [4] and Common Lisp [9]. This mechanism plays an important role when programmers handle exceptional situations. Suppose, for example, wehave to construct a program P with a speci cation
represented by a sequent 0 ! C _ E of LJ combining three subprograms Q : 0 ! A _ E , R : 0 A !
B _ E and S : 0 B ! C _ E , where C is the normal
output for the input 0, and E is an error signal which
denotes that there is something wrong in the input.
The speci cations of Q, R and S say that such errors may be detected in the execution of these subprograms. Under this situation, the construction of P in

LJ would be as Figure 1, where applications of structural rules are omitted. The constructed program P
would work as follows. The program P rst calls the
subprogram Q and gets its return value, then checks
the value whether it denotes an error or not. If not,P calls the subprogram R with that value and gets
its return value. P again checks the value and calls S
if it does not denote an error. Eventually, P returns
the value returned by S . If P detects an error in thevalues returned by Q or S , it immediately returns avalue denoting an error. We can nd an ineciency
that whenever P gets values from the subprograms it
must check them whether they denote a error or not.
This is often found in the practical programming without the catch/throw mechanism. If the mechanism isavailable, programmers can concentrate on the mainstream of programming as if there must not happen
any exceptional situation since error signals are passed
through bypasses provided by the mechanism. Following the proofs-as-programs notion in the opposite direction, we can nd that the problem comes from therestriction of LJ that only one formula is admissible
to the right hand side of sequents. If the restriction is
dropped like LK, we can construct P of a speci cation 0 ! C E from subprograms Q : 0 ! AE , R : 0 A!BE and S : 0B !CE as follows:
.. R
.. S
.
.
.. Q
.
0 A ! BE 0 B ! CE (cut)
0 ! AE
0 A ! CE (cut);
0 ! CE
0

0

0

0

0

0

0

where structural rules are omitted again. The proof
is much simpler than the previous one and easy todevelop. The point is that exceptional conclusions
are admitted beside the main conclusion and we canproceed the proof construction as if they do not exist. It re ects the programmer's reasoning behind thecatch/throw mechanism. Of course, we must justify

.. S
.

)
E ! E (init(!_
0 B ! C _ E E ! C _ E (_!)))
0 B _ E ! C _ E (cut)
E ! E (init
0 A!B _E(!_
0A !C _E
E ! C _ E (_!))
0 A _ E ! C _ E (cut);
0! C _E
.. R
.

.. Q
.

0 !A_E

Figure 1: Exception handling without catch/throw.
A ! A ; (init)

01 ! A ;11 02 A ! C ;12 (cut)01 02 ! C ;11 12

0 ! A ;11 BC 12 (!x)
0 ! A ;11 CB 12

01 AB 02 ! C ;1
01 BA 02 ! C ;1 (x!)

01 ! A ;11 02 ! B ;12 (!^)
01 02 ! A ^ B ;11 12

0 ! A ;1 (!_ )1
0 ! A _ B ;1

0 ! E ;1
0 ! A ; E 1 (throw)

0 ! A ; EE 1 (!c)
0! A; E 1

01 AA 02 ! C ;1 (c!)
01 A 02 ! C ;1

0 A ! C ;1
0 A ^ B ! C ;1 (^1 !)0 ! B ;1 (!_ )2
0 ! A _ B ;1

0 A!B ;
0 ! A  B ; (!)

0 ! A ; A 1 (catch)
0 ! A ;1

0 ! A ;1 (!w)
0 !A; E 1

0 ! C ;1
0 A ! C ;1 (w!)

0 B ! C ;1
0 A ^ B ! C ;1 (^2!)

01 A ! C ;11 02 B ! C ;12 (_!)
01 02 A _ B ! C ;11 12

01 ! A ;11 02 B ! C ;12 (!)01 02 A  B ! C ;11 12

0! A; E 1
0 ! A/E ;1 (!/)

01 A ! B ;11 02 E ! C ;12 (/!)
01 02 A/E ! C ; B 11 12
Figure 2: Inference rules.

such a logic constructively so that correct programs
can be extracted from the proofs. In the following sections, we present such an attempt to extract a logicalstructure from the programmer's reasoning concerning
exception handling by the catch/throw mechanism.
2 The formal system

We introduce a sequent calculus to capture thecatch/throw mechanism. But it is not importantwhether the formalization is done by the sequent calculus style or not. We adopt such a style here justfor convenience of readers who are familiar with thecorrespondence between classical logic and control op-

erators such as call/cc, for it becomes clear when we
regard our formal system as an intermediate system
between LJ and LK. We are also able to consider anatural deduction style formalization, and it would be
more suitable for natural development of programs.
We restrict the logic to a minimal propositional
logic in this paper since the restricted system is enoughfor us to observe the essence how the mechanism
works. Note that it can be easily extended to thepredicate logic.
Formulas Formulas of our system consist of atomic
formulas, conjunctions (A ^ B ), disjunctions (A _ B ),implications (A  B ) and exceptions (A/ B ). The last
one is introduced to handle the catch/throw mechanism and represents another kind of disjunction. Wegive a precise meaning to the connective / by a realizability interpretation later.
Sequents Sequents of the system are of the form:

where the set of tag constants is a representation of
the set of natural numbers. We use n to denote thetag constant which represents a natural number n, and^t to denote the natural number represented by a tag
constant t.

where m and n can be 0. They look like the ones of LK
rather than LJ ignoring the semicolons \;" between C
and E1 : : : En . Actually, their purely logical meaning is the same as LK. In this sense, the semicolons
are negligible. But they play a certain role for theconstructive meaning of the sequents. The formula C
between the arrow and the semicolon represents themain conclusion and E1 : : : En represent exceptional
conclusions. The sequent A1 :::Am ! C ; E1 :::En represents a program such that when we execute the program supplying values that satis es the speci cation
A1 :::Am for the corresponding free variables of the
program, it normally returns a value which meets C ,otherwise the program exits with a value which meets
one of E1 :::En . Note that if n = 0, i.e. E1 :::En isempty, the meaning of the sequent is just the same as
the usual interpretation of the sequent of LJ.
Inference rules The inference rules of the formal
system are listed in Figure 2. If we ignore semicolons
in the sequents, they are almost the same as the ones of
LK except for the logical rules concerning the new connective /. The only essential di erence is that there
must be exactly one formula on the right hand side of
the sequent when we apply the right-implication rule(!). Roughly, our system can be regarded as the
propositional fragment of LK with this restriction on
the right-implication rule. But it should be also notedthat every right logical rule introduces a logical connective into the formula between the arrow and thesemicolon, i.e. the main conclusion.

Ce A set of individual constants c;d;:::.
Ve A countably in nite set of individual variables
x;y;z;:::.
Ct A set of tag constants 0; 1; 2;:::.
Vt A countably in nite set of tag variables u;v;w;:::.

A1 :::Am ! C ; E1 :::En;

3 A realizability interpretation

Before discussing the syntactical properties of theformal system, we give an example of realizability interpretation of the system to explain how thecatch/throw mechanism can be captured in it. Theinterpretation is de ned by an abstract machine
which manipulates expressions equipped with thecatch/throw mechanism. We start with the de nitionof the expression syntax.
Constants and variables We rst assume the following disjoint sets of individual constants, individual
variables, tag constants and tag variables are given,

Tags Tag constants and tag variables are called tags.
We denote the set of tags by T . That is,
T ::= Ct j Vt:

We use s;t;::: to denote tags.

Expressions Expressions E are de ned as follows.
E ::= Ce j Ve j let Ve = E:E j EE j Ve :E
j <E;E> j proj E j proj E
j inj1 E j inj2 E 1j caseE Ve2:E Ve:E
j throwT E j catchVt E j ET j Vt:E

The expressions  Vt :E and E T are used for tagabstraction and tag-instantiation, respectively. We
use e;f;::: to denote expressions. Free and bound occurrences of variables are de ned in the standard manner. We regard a tag variable u as bound in catch ue
and u:e. We use e[M=x] to denote the expression
obtained from an expression e by replacing each freeoccurrence of a variable x by an expression or a tag
M.

An abstract stack machine We now de ne an
abstract machine which evaluates expressions. The
machine is designed only to illustrate how thecatch/throw mechanism works. We leave other mechanisms required for the evaluation of expressions being
abstract (cf. [5, 8]). It has a stack of expressions anda special symbol denoted by 3 which may appear onlyat the top of the stack. The state of the machine is determined only by the state of this stack. We represent
a state of the stack as follows.
bottom! top[ e1 ; e2 ; e3; :::; en; M ];where e1 :::en are expressions and M is an expression
or the special symbol 3.

Transition rules The abstract machine changes its
state as follows:~ x:e2 ; e1 ; 3] ) [f;~ e2[e1 =x]][f;~~[f; let x = e1:e2] ) [f; x:e2 ; e1][f1;:::; fn;:::; throw n e] ) [f1 ;:::; fn ; e][f1 ;:::; fn ; catch ue] ) [f1 ;:::; fn ; e[n=u]]~ <e1 ;e2 >] ) [f;~ <e1 ;e2 >; 3][f;~[f; proj1 <e1 ;e2 >] ) [f;~ e1][f;~ proj2 <e1 ;e2 >] ) [f;~ e2]~ inj1 e] ) [f;~ inj1 e; 3][f;~~[f; inj2 e] ) [f; inj2 e; 3]~ case (inj1 e) x:e1 y:e2] ) [f;~ e1[e=x]][f;~ case (inj2 e) x:e1 y:e2] ) [f;~ e2[e=y ]][f;~[f; x:e] ) [f;~ x:e; 3]~[f; (x:e1 ) e2] ) [f;~ e1[e2 =x]]~ u:e] ) [f;~ u:e; 3][f;~~[f; (u:e) t] ) [f; e[t=u]]~ c] ) [f;~ c; 3];[f;where f~ denotes a sequence of expressions. The rule
applicable for a state is uniquely determined by theobject at the top of the stack. Let ) be the transitive
re exive closure of the relation ). If [e1 ] ) [e2; 3],
the expression e2 is unique modulo alpha-conversion.
This represents that e2 is the head normal form of
e1 . We denote it by Eval(e1 ) = e2 . It should be
noted that the machine has no evaluation strategy
for the expressions except for let-expressions. For example, there is no rules to apply when an expression ((x:x)(x:x)) c is the top object of the stack.
To get c as the result of evaluation, the expression should be let y =(x:x)(x:x): yc. The machine
rst evaluates e1 of let x = e1:e2 to get its head normal form, then proceed to the evaluation of e2 with
it. Only let-expressions determine the evaluation order. We must specify the evaluation order of expressions by let-expressions explicitly. Note also that letexpressions are the only expressions that push something to the stack. The expressions f1 :::fn of thestack [f1; :::; fn;e] must be of the form of lambdaabstraction, and the composition of f1 :::fn represents
the continuation after the evaluation of the expressione (cf. [2]). The catch/throw mechanism of the machine provides a restricted access to the continuation
through tags. Although it does not provide a way totreat it as a rst class citizen as in Scheme, it does not
require any explicit copying of the control context.
Realizability interpretation of formulas We
now de ne a realizability for formulas using the abstract machine. Let A be a mapping which assigns a3

3

subset of Ce to each atomic formula. Let e and A be
an expression and a formula, respectively. We de ne
the realizability relation denoted by e r A between
expressions and formulas as follows.
1. e r A i e 2 A(A), if A is an atomic formula.
2. e r A1 ^ A2 i e = <e1; e2 > for some e1 and e2
such that e1 r A1 and e2 r A2 .
3. e r A1 _ A2 i e = inj e for some i (i = 1; 2) ande r Ai .
4. e r A1  A2 i e = x:e and Eval(e [f=x]) r A2
for any expression f such that f r A1.
5. e r A1 /A2 i e = u:e and one of the following
holds.
(a) Eval(e [n=u]) r A1 for any natural numbern.
)(b) [f1 ; ::: ; fn ; ::: ; fn+m ; e [n=u]][f1 ;:::;fn;e ; 3] and e r A2 for any natural
numbers n and m.
If the relation holds between an expression and aformula, we say that the expression realizes the formula, and the expression is a realizer of the formula.
Realizability interpretation of sequents We
now consider a triple which consists of a sequence ofindividual variables of length m, an expression and asequence of tag variables of length n for each sequent
A1 :::Am ! C ; B1 :::Bn. We assume the free individual and tag variables of the expression are included in
the two sequences. We de ne a realizability relationr between such triples and sequents as follows. The
relation< x1 :::xm ; e; u1 :::un > r A1 :::Am ! C ; B1 :::Bnholds if and only if one of the following two holds forany natural number l, expressions f1 ;:::;fl ;g1 ;:::;gm
such that g1 r A1, ::: , gm r Am, and tag constants
t1;:::;tn such that t^0  l, ::: , t^n  l.
i

0

0

0

0

0

0

3

0

00

00

1. [f1;:::;fl ;e[~g=~x;~t=~u] ) [f1 ;:::;fl ;e ; 3] and e r C .
2. [f1;:::;fl ;e[~g=~x;~t=~u] ) [f1 ;:::;ft^ ;e ; 3] and e r Bi
for some i (0  i  n),
where the expression e[~g=~x; ~t=~u] stands fore[g1 =x1;:::;gm=xm; t1 =u1 ;:::;tn=un]. If the relation
holds between a triple and a sequent, we say that the
triple realizes the sequent, and the triple is a realizerof the sequent. Note that this de nition of realizability is essentially the same as the standard realizability
3

0

3

0

0

i

0

de nition of LJ in the case that the formula C does
not include any occurrence of / and B1 :::Bm is empty.
It should also be noted that the logical connective /corresponds to the semicolon of a sequent as so does
 to the arrow.
Soundness of the formal system The following
soundness theorem assures us that we can regard theproofs of the formal system as programs which satisfy
the speci cation de ned by the realizability interpretation of the conclusion.
Theorem 1 If a sequent is derivable in the formal
system, we can construct a realizer of the sequent.

Realizer construction The theorem is proved byinduction on the structure of the derivation. For example, if (catch) is the last inference rule of the derivation of a sequent 0 ! A ;1, we have a realizer of 0 !
A; A 1 by the induction hypothesis. Let < ~x;e;u~v >be the realizer. We can take < ~x; catchue;~v > as therealizer for the conclusion. We only summarize how
to construct the realizer according to the derivation to
Figure 3 here, and omit the details of the proof. Notethat the let-expressions included in the constructed realizers direct the evaluation of the expressions in callby-value fashion.
4 The formal system as a logic

In this section we discuss the basic property of theformal system considering it as a logic. First we consider the new logical connective /.
De nition 2 We use A~ to denote the formula obtained from a formula A by replacing every occurrenceof the logical connective / by _. If A~ = B~ , then wedenote it by A ' B . If 0 = A0 :::An , 1 = B0 :::Bnand Ai ' Bi for any i (0  i  n), then we denote itby 0 ' 1.
Lemma 3 If A ' A , then A ! A ; is a drivable sequent of the system.
Proof. Straightforward induction on the structure of
the formula A. The basic idea comes from the following two derivations.
.. ind. hyp.
.. ind. hyp.
.
.
A !A ;B !B ;(!_1 ) B ! A _ B ; (!_2)
A!A _B ;(/!)
A/B ! A _ B ; A _ B(catch)A/B ! A _ B ;
0

0

0

0

0

0

0

0

0

0

0

0

0

0

.. ind. hyp.
.. ind. hyp. B !. B ;.
(throw)
A! A ;B !A ; B(_!)
A_B !A ; B(!/)
A _ B ! A /B ;Theorem 4 If 0 ! A ;1 is a derivable sequent of thesystem, and if 0 ' 0 , A ' A and 1 ' 1 , then 0!A ;1 is also derivable.
Proof. Induction on the structure of the derivation of
the sequent 0 ! A ;1. Apply Lemma 3 in the case thatthe last rule is (init).
The theorem says that the logical meaning of A/B isessentially the same as A _ B . The di erence between
them consists only in their implementation.
If we identify A/B with A _ B , the formal system
can be regarded as a variant of the propositional fragment of LJ.
Theorem 5 A sequent A1 :::Am ! C ; is derivable inthe system if and only if A~1 ::: A~m ! C~ is derivable in(the propositional fragment of) LJ.
Proof. The if part is trivial because the propositional
fragment of LJ can be regarded as a subsystem of ours.
For the only if part, prove the following conjecture
by induction on the structure of the derivation: If
A1 :::Am ! C ; E1 :::En is derivable, then A~1 ::: A~m !
C~ _ E~1 _ ::: _ E~n is derivable in (the propositional fragment of ) LJ. The theorem is a corollary of the conjecture.
As a corollary of the theorem, we get the disjunction property of the system.
Corollary 6 If ! A _ B ; is a derivable sequent, thenwe can derive ! A ; or ! B ; .
There must be no formulas on the right hand sideof the semicolon when we apply the right-implication
rule (!). This restriction is the most signi cantdi erence from LK, and it keeps the system constructive. LK with this kind of restrictions is known asa variant of LJ, which is essentially equivalent to LJ(cf.[6, 10, 11]). The same restriction is also requiredfor (!8)-rule in the case of predicate calculus. If wedropped the restriction, the system would become aclassical one.
The cut-elimination theorem holds for the formal
system.
Theorem 7 If a sequent is derivable, then we can derive it without (cut)-rule.
0

0

0

0

0

0

0

0

0

0

0

0

0

0

A! A ;
< x;x;>(init)< ~x;e1 ;~u > < ~y z;e2 ;~v >< ~x;e;~v >01 ! A ;11 02 A ! C ;12 (cut)
0 ! E ;1
01 02 ! C ;11 12
0 ! A ; E 1 (throw)< ~x~y; let z = e1:e2;~u~v >< ~x; let y = e: throw uy;u~v >< ~x;e;u~v >0 ! A ; A 1 (catch)
0 ! A ;1
< ~x; catch ue;~v >< ~x;e;~u v1 v2 w~ >0 ! A ;11 BC 12
0 ! A ;11 CB 12 (!x)
< ~x;e;~u v2 v1 w~ >< ~x;e;~v >0 ! A ;1
0 ! A ; E 1 (!w)
< ~x;e;u~v >< ~x;e;u1 u2 ~v >0 ! A ; EE 1 (!c)
0 !A; E 1
< ~x;e[u=u1 ;u=u2 ];u~v >< ~xy1 y2 ~z;e;~u >01 AB 02 ! C ;1
01 BA 02 ! C ;1 (x!)< ~xy2 y1 ~z;e;~u >< ~x;e;~u >0 ! C ;1
0 A ! C ;1 (w!)< ~x y;e;~u >< ~xy1 y2 ~z;e;~u >01 AA 02 ! C ;1 (c!)
01 A 02 ! C ;1
< ~x y~z;e[y=y1;y=y2 ];~u >< ~x;e1;~u > < ~y;e2;~v >01 ! A ;11 02 ! B ;12 (!^)
01 02 ! A ^ B ;11 12< ~x~y; let z1 = e1: let z2 = e2:<z1 ;z2 >;~u~v >< ~x;e;~u >0 ! A ;1
0 ! A _ B ;1 (!_1 )< ~x; let y = e: inj1 y;~u >< ~x;e;~u >0 ! B ;1
0 ! A _ B ;1 (!_2 )< ~x; let y = e: inj2 y;~u >< ~xy;e;>0A !B ;
0 ! A  B ; (!)
< ~x;y:e;>< ~x;e;u~v >0 ! A ; E 1 ( ! /)0 ! A/E ;1< ~x;u:e;~v >< ~xz;e;~u >0 A ! C ;1
0 A ^ B ! C ;1 (^1 !)< ~xy; let z = proj1 y:e;~u >< ~xz;e;~u >0 B ! C ;1
0 A ^ B ! C ;1 (^2 !)< ~xy; let z = proj2 y:e;~u >< ~x z1;e1;~u > < ~y z2;e2 ;~v >01 A ! C ;11 02 B ! C ;12 (_!)
01 02 A _ B ! C ;11 12< ~x~y z; case zz1:e1 z2:e2 ;~u~v >< ~x;e1 ;~u > < ~y z ;e2 ;~v >01 ! A ;11 02 B ! C ;12 (!)01 02 A  B ! C ;11 12< ~x~y z; let z = e1: let z = zz :e2;~u~v >
0

00

0

00

< ~x z1;e1 ;~v > < ~y z2;e2 ; w~ >01 A ! B ;11 02 E ! C ;12 (/!)
01 02 A/E ! C ; B 11 12< ~x~y z; let z2 =(catch w let z1 = zw : let z = e1: throw uz ):e2;u~v w~ >
0

0

0

0

Figure 3: Realizer construction.
We omit the proof for lack of space. The proof becomes more complicated than the case of LJ/LK because it required a special condition to apply (!)rule and the new connective / has been introduced.
Unfortunately, the computational behavior of thecatch/throw mechanism is not captured by the cutelimination process. Consider the following simple example.
A ! A ; (init)
A ! A ; A (throw)(catch)A !A;< x; catchu (let y = x: throw uy);>

It is a cut-free derivation, but the realizer includes acatch-throw pair. Another kind of proof translation
should be considered to explain the mechanism.
5 Some comments on the formalization

As mentioned above, sequents of our formal system can be regarded as the ones of LK ignoring semicolons. Let us compare the system with LK. First,
there must be at least one formula on the right handside of sequents. But this comes from that the system
is a minimal logic and is not an important di erence

for us.
The three right-structural rules of LK are divided
into ve rules, and there is no right-exchange rules
over the semicolon. The rules (catch) and (!c) correspond to the right-contraction rule of LK. The former introduces a catch-expression. The latter means asharing of one tag variable by two throw-expressions,i.e. multiple throw-expressions would be caught by
one catch-expression afterwards. The right-weakening
rule of LK is divided into (throw) and (!w). The
former corresponds to a throw-expression. The lattermeans an introduction of a redundant tag variable.
We note that the rule (!w) is a derived rule of otherrules.
< ~x;e;~v >0 ! A ;1)
0 ! E ; A 1 ((throw
throw)
0 ! A ; EA 1 (!x)
0 ! A ; AE 1 (catch)
0! A; E 1
< ~x; catchw(let y =(let z = e: throw wz ): throwuy);u~v >But we adopt (!w) as a primitive rule because therealizer given above introduces a redundant throwexpression, i.e. a throw-expression never visited.
We do not have a right-exchange rule over the semicolon, but it is also a derived rule as follows.
< ~x;e;u w~ >0 ! A ; E 1 throw)
0 ! E ; AE 1 ((!
x)
0 ! E ; EA 1 (catch)
0! E ; A1< ~x; catchu (let y = e: throw vy );v w~ >In contrast to (!w), we leave it as a derived rule because there is no primitive realizer construction corresponding to the rule.
We have a restriction on (!)-rule to keep the system constructive as mentioned before. If we dropped
the restriction, the following anomaly would occur.
Consider the following derivation of A _ (A  B ).
A ! A ; (init)(!_1)
A ! A _ (A  B );(throw)
A ! B ; A _ (A  B ))!A B ; A_(A B) (!(!_!A _(AB ); A _(A B) (catch2))!A_ (AB);
The realizer would be catch u (let y = x: (let z =(letx =x: inj1 x ): throw uz ): inj2 y). Removing redundant let-expressions, we get catch u inj2 (x: throw u00(inj1 x)). The evaluation process of the expression
would be as follows.
[x1:e1 ;:::;xn:en ; catchu inj2 (x: throw u (inj1 x))]) [x1:e1;:::;xn:en; inj2 (x:throw n (inj1 x)); 3]) [x1:e1;:::;xn 1:en 1;
en[inj2 (x: throw n (inj1 x))=xn]]
Note that the tag constant n in the last is meaningless because the the corresponding control context has
been lost. From a computational point of view, thisproblem can be solved by introducing more powerful
facilities for non-local exit such as call/cc of Scheme.
But it a ects the realizability interpretation of formulas. For example, although the realizers of disjunctions
still have a certain constructive meaning yet, they do
not always contain the information which formula of
A_B is realized by them (cf. [3, 7]). It should be notedthat the system without the restriction becomes a classical one, and we do not have the disjunction property
anymore.
The restriction on (!)-rule leads us to introduce
the new connective /. We can not construct any function that may throw something to the outside of thefunction without the new connective. Such a function
is represented by a formula of the form A(B/E ), andis called with a value for A and a tag for E . Normally,
the function returns a value of B , otherwise it throws
a value of E to the given tag. Concerning the left logical rule of /, there is another possibility of formulation
as follows:< ~xz;e;~v >0 A ! C ;1 (/!)
0 A/E ! C ; E 1< ~xy; let z = yu:e;u~v >From the viewpoint of realizer construction, it corresponds to a more primitive construction than theoriginal one listed in Figure 2, and is easy to understand for programmers. But it requires (cut)-rule tobe equivalent to the original. So the cut-elimination
theorem does not hold if we substitute it for the original. This is the only reason why we adopt the original
formulation.
00

6 Conclusion

We have presented a formal system which captures
the catch/throw mechanism in the proofs-as-programs
notion. Although the system is just a variant of LJ,
it admits extra conclusions beside the main one. So
we can construct proofs which handle the exceptionalsituations eciently. We showed that we can actuallyextract programs that make use of the catch/throwmechanism from such proofs. Our work can be regarded as a higher order extension of the work concerning goto statements in Hoare logic (cf. [1]), whose
main idea is also the existence of extra post-conditions.
Although, from a computational point of view, thecatch/throw mechanism provides only a restricted access to the current continuation, we can extract correct programs without any restriction required for thecase of more powerful facilities such as call/cc (cf.
[7]). And more important, there exists a characteristic
way of programmer's reasoning concerning exception
handling behind the mechanism. We wonder whether
there also exists such a reasoning corresponding to theuse of call/cc and its variants beyond the catch/throw.

Acknowledgements
The author wishes to thank Susumu Hayashi fora great number of helpful suggestions and invaluable
encouragement regarding this work. He pointed out
the connection between this work and the literature
concerning variants of LJ and the treatment of gotoin Hoare logic. Thanks are also due to the referees
for helpful comments on the detailed abstract of thispaper.
References[1] S. Alagic and M. A. Arbib, The Design ofWell-Structured and Correct Programs, SpringerVerlag, 1978.
[2] M. Felleisen, D. Friedman, E. Kohlbecker, and
B. Duba, A syntactic theory of sequential control, Theoretical Computer Science, Vol. 52(3),pp. 205-237, 1987.
[3] T. G. Grin, A formulae-as-types notion of control, Conf. Rec. ACM Symp. on Principles ofProgramming Languages, pp. 47-58, 1990.
[4] B. W. Kernighan and D. M. Ritchie, The C
programming language (2nd ed.), Prentice Hall,
1989.
[5] P. J. Landin, The mechanical evaluation of expressions, Computer Journal, Vol. 6(4), 1964.
[6] S. Maehara, Eine Darstellung intuitionistic Logik
und der Klassishen, Nagoya Math. Journal, Vol.
7, pp. 45-64, 1954.

[7] C. R. Murthy, An evaluation semantics for classical proofs, Proc. IEEE Symp. on Logic in Computer Science, pp. 96-107, 1991.
[8] G. D. Plotkin, Call-by-name, call-by-value andthe -calculus, Theoretical Computer Science,Vol. 1, pp. 125-159, 1975.
[9] G. L. Steele, Common Lisp: The Language, Digital Press, 1984.
[10] K. Schutte, Vollstandige Systeme Modaler und
Intuitionistischer Logik, Springer-Verlag, 1968.
[11] G. Takeuti, Proof theory (2nd ed.), North Holland, 1987.