ROPAS

Research On Program Analysis System

National Creative Research Initiative Center Korea Advanced Institute of Science and Technology

ROPAS MEMO 2000-8 October 4, 2000

Proving Exception Stackability and Linearity in an Ordered Logical Framework

Jeff Polakow

Department of Computer Science Carnegie Mellon University

              jpolakow@cs.cmu.edu

Kwangkeun Yi

Department of Computer Science KAIST

                                             kwang@cs.kaist.ac.kr

October 4, 2000

Abstract

We formally prove the stackability and linearity of exception handlers of ML-style semantics using a novel proof technique via an ordered logical framework (OLF). We first transform exceptions into continuation-passing-style (CPS) terms and formalize the exception properties as a judgement on the CPS terms. Then, rather than directly proving that the properties hold for terms, we prove our theorem for the representations of the CPS terms and transform in OLF. We rely upon the correctness of our representations to transfer the results back to the actual CPS terms and transform.

Our work can be seen as two-fold: we present a theoretical justification of using the stack mechanism to implement exceptions of ML-like semantics; and we demonstrate the value of an ordered logical framework as a conceptual tool in the theoretical study of programming languages.

1 Introduction

Exception handling facilities in modern languages like ML [MTHM97, LDG^{+}00] or Java allow the programmer to define, raise and handle exceptional conditions. Exceptional conditions are brought (by a raise expression) to the attention of another expression where the raised exceptions may be handled. Exceptions are not necessarily limited to dealing with errors. The programmer can use exceptions as a “control diverter” to escape from any control structure to a point where the corresponding exception is handled. Also, using exceptions, the programmer can tailor an operation’s results to particular purposes in a wider variety of contexts than would otherwise be the case.

In this article we formally prove a folklore property of exceptions: exception handlers are used at most once (linearity) in a stack-like-manner (stackability) (i.e., installing an exception handler and handling an exception respectively amounts to “push” and “pop.”). Furthermore we show that the ordering properties investigated in [DDP99, DP95] for results of the conventional continuation-passing-style (CPS) transformation [DF92, Plo75, Ste78]— stackability of both continuation identifiers and continuation parameters— also hold for results of an extended CPS transform which replaces exception-raise and -handle expressions by function (continuation) calls and constructions in higher-order programs[KYD98, App97].

We prove the two properties as follows:

0This work is supported by Creative Research Initiatives of the Korean Ministry of Science and Technology.

1. In order to expose the semantics of exceptions in the program text, we encode exceptions in source programs with continuations by using the extended CPS transformation.

2. We then formalize the properties of interest as a judgement on CPS terms.

3. We then prove that all terms resulting from the transformation satisfy our judgement.

We carry out the main portion of our proof (pt. 3 above) in a novel fashion— via an ordered logical framework (OLF) [PP00], a new formalism which is particularly well-suited for our purpose. Rather than directly proving that the properties hold for terms (which would require a rather tedious logical-relations style argument), we directly prove our theorem for representations of the CPS terms and transform in OLF. By working in OLF we can take advantage of known properties of OLF terms (e.g. substitution properties) which simplify our task. We then rely upon the correctness of our representations to transfer the results back to the actual CPS terms and transformation.

Our work can be seen as a theoretical justification of existing compilers that use the stack mechanism to implement exceptions. Our work also demonstrates the value of a (ordered) logical framework as a conceptual tool in the theoretical study of programming languages. We believe that working inside OLF greatly simplifies our proof. Of course such simplification comes at the cost of gaining familiarity with OLF. However, we feel the trade-off is advantageous. Logical frameworks have generally proven themselves to be useful tools for studying programming languages [Pfe96]; and we believe OLF, though still a new formalism, will likewise prove itself useful.

1.1 Overview

Section 2 introduces the ordered logical framework in which we will represent our terms and transform. In section 3.2 we define direct-style terms with exception raise and handle expressions, CPS terms, and the CPS transformation for encoding exception-raise and -handle expressions by continuations. We also define judgements on CPS terms for stackability (and linearity) of the exception handling mechanism. In section 4 we give OLF representations for direct-style terms and for CPS terms satisfying the stackability judgements. In section 5 we show the representation of the CPS transformation. This representation takes represented direct-style terms to represented CPS terms. The correctness of this representation completes our proof since represented CPS terms correspond to actual CPS terms satisfying the stackability judgements. Finally, we give a conclusion with some related and future work in section 7.

2 Ordered Logical Framework

OLF is a logical framework in the tradition of LF [HHP93] and its linear extension LLF [CP99]. Thus OLF is essentially a dependent type theory^{1} for which type checking is decidable and canonical forms exist. Since OLF has come under study quite recently, the remainder of this section provides the necessary background information to follow our proof.

OLF should be thought of as ordered linear types [PP99a] extended with dependent types. Thus, we will first review Ordered Linear Logic, the logic corresponding to ordered linear types.

1Types can depend upon terms.

2.1 Ordered Linear Logic

Ordered linear logic (OLL) is a conservative extension of intuitionistic linear logic with ordered hypotheses. We begin with a review of the fragment of OLL which we will use. For a description of the full system see [PP99b, PP99a].

Types A ::= a  atomic types
| A_{0} → A_{1}  intuitionistic implication
| A_{0} ↠ A_{1}  ordered right implication
| A_{0} & A_{1}  additive conjunction
| ⊤  additive truth

Objects M ::= c  constants
| x | z  variables
| λx:A. M | M_{0} M_{1}  intuitionistic functions (A → B)
| λ^{>}z:A. M | M_{0}^{>}M_{1}  right ordered functions (A ↠ B)
| ⟨M , N⟩ | π_{1} M | π_{2} M  additive pairs (A & B)
| ⟨⟩  additive unit (⊤)

We build typing rules for OLL objects from the following judgement

Γ; Ω ⊢ M : A

where Γ is a list of unrestricted hypotheses, Ω is a list of ordered hypotheses, and a signature containing constant declarations is left implicit. The inference rules will be structured to allow copying, discarding, and exchanging of unrestricted hypotheses. However, ordered hypotheses will not enjoy those structural properties— they must be used exactly once in their relative order.

Here are the rules for unrestricted functions.

\frac{ivar}{(Γ_{1}, x:A, Γ_{2}); · ⊢ x : A}  \begin{aligned}(Γ, x:A); Ω ⊢ M : B \\ & →I \\ Γ; Ω ⊢ λx:A. M : A → B \end{aligned}
Γ; Ω ⊢ M : A → B Γ; · ⊢ N : A

→E Γ; Ω ⊢ M N : B

Note that the ordered context in the minor premise of →_{E} must be empty. This ensures that unrestricted functions, which may use their argument arbitrarily, may not be applied to ordered arguments, which must be used exactly once.

The rules for ordered functions follow.

\frac{ovar}{Γ; z:A ⊢ z : A}  \begin{aligned}Γ; (Ω, z:A) ⊢ M : B \\ & ↠I \\ Γ; Ω ⊢ λ^{>}z:A. M : A ↠ B \end{aligned}
Γ; Ω_{1} ⊢ M : A ↠ B Γ; Ω_{2} ⊢ N : A
↠E
Γ; (Ω_{1}, Ω_{2}) ⊢ M^{>}N : B

Note that the argument to an ordered function may only depend upon ordered hypotheses to the right of those use by the body of the function—the order of the hypotheses constrains their use by ordered functions.

Finally we give the rules for pairs and unit.

\begin{matrix}Γ; Ω ⊢ M : A  Γ; Ω ⊢ N : B \\ & & I \\ Γ; Ω ⊢ ⟨M , N⟩ : A & B \end{matrix}  \frac{⊤_{I}}{Γ; Ω ⊢ ⟨⟩ : ⊤}

\begin{matrix}Γ; Ω ⊢ M : A & B \\ & & E1 \\ Γ; Ω ⊢ π_{1} M : A \end{matrix}  \begin{matrix}Γ; Ω ⊢ M : A & B \\ & & E2 \\ Γ; Ω ⊢ π_{2} M : B \end{matrix}

The reduction rules for OLL objects are simply β-reduction for both kinds of functions. The appropriate notion of equality of objects also includes η-conversion so that every welltyped object has an equivalent canonical form.

Our calculus enjoys subject reduction, as proved in [PP99a].

Theorem 1 (Subject Reduction) If M ⟹ M′ and Γ; Ω ⊢ M : A then Γ; Ω ⊢ M′ : A.

Proof: For each reduction, we apply inversion to the given typing derivation and then use a substitution lemma to obtain the typing derivation for the conclusion. □

Finally, we note that this calculus has canonical forms as shown in [PP99a]. Thus all terms of functional type may be converted to the form λx:A. M or λ^{>}z:A. M; all terms of conjunctive type may be converted to pairs ⟨M , N⟩; and all objects of atomic type may be reduced to a constant applied to zero or more canonical objects.

The existence of canonical forms for this simple implicational fragment of OLL provides a basis for an ordered logical framework. We conjecture that an ordered logical framework based on a full type theory can be constructed along the lines of the linear logical framework [CP99]. In this paper we only need a two-level fragment as explained in subsection 2.2.

2.2 Two-Level Framework

We extend the ordered λ-calculus from subsection 2.1 to a simple two-level logical framework. Level 2 type families p are indexed by level 1 objects M, and we can quantify only over level 1 objects.

Level 2 types F ::= p M_{1} … M_{n}
| F_{1} → F_{2}
| F_{1} ↠ F_{2}
| F_{1} & F_{2}
| ⊤
| Πx:A. F

Level 2 objects D ::= c | w | y
| λw:F. D | D_{1} D_{2}
| λ^{>}y:F. D | D_{1}^{>}D_{2}
| ⟨D_{1} , D_{2}⟩ | π_{1} D | π_{2} D
| ⟨⟩
| λx:A. D | D M

The extended typing judgement now has the form Γ; Ω ⊢ D : F, where Γ may contain declarations of the form x:A or w:F and Ω contains declarations y:F. We omit the typing rules which are very similar to the propositional case, except that we now need rules for the dependent types:

\frac{Γ, x:A; Ω ⊢ D : F}{Γ; Ω ⊢ λx:A. D : Πx:A. F}  \frac{Γ; Ω ⊢ D : Πx:A. F  Γ; · ⊢ M : A}{Γ; Ω ⊢ D M : F [M/x]}

and a rule for type conversion:

\frac{Γ; Ω ⊢ D : F F ≡_{βη} F′}{Γ; Ω ⊢ D : F′}

Since we stratify the type theory into two syntactically distinct levels, βη-equality for level-2 types immediately reduces to βη-equality for propositional objects. Since propositional objects possess canonical (= long βη-normal) forms, this equality is easy to decide, and type-checking in the fragment presented above can easily be seen to be decidable. Furthermore, canonical forms for level-2 objects likewise come as a consequence of level-1 objects having canonical forms. We will use the judgement

Γ; Ω ⊢ D ⇑ F

to denote that object D is canonical at well-formed type F.

3 Terms & Transforms

This section introduces the direct-style language with exception raise and handle expressions, its CPS counterpart, and the transformation between them. We use underlined constants (e.g. \underline{handle}) and lambdas (\underline{λ}) to distinguish these objects from their OLF representations which are given in section 4.

3.1 Direct Terms

We use the following syntax for direct-style (DS) terms:

DS Terms  r ::= e
DS Expressions  e ::= e_{0} e_{1} | \underline{handle} e_{0} (\underline{λ}x. e_{1}) | \underline{raise} e | t
DS Trivial Expressions  t ::= \underline{λ}x. r | x

Evaluating the expression \underline{raise} e first evaluates e. It then aborts the normal execution and locates a handler by going up the current evaluation chain. The e’s value is passed to handler. The handle expression \underline{handle} e_{0} (\underline{λ}x.e_{1}) evaluates e_{0}. If e_{0} raises an exception with value v and there are no other handle expressions between the current one and the raise expression, then the current handler function \underline{λ}x.e_{1} handles it: the v is bound to x in e_{1}. Otherwise, the value of the handle expression is the value of e_{0}.

We define the formal semantics of DS terms with a structural operational semantics [Plo81] using Felleisen’s evaluation contexts [Fel87]. In doing so, we need to extend the expressions to contain a set of raised values \overline{t} that are thrown from raise expressions: e ::= ⋯ | \overline{t}. An evaluation context C is defined by the following grammar:

C ::= [ ] | C e | t C | \underline{handle} C \underline{λ}x. e | \underline{raise} C

This context defines a left-to-right, call-by-value reduction. As usual, we write C[e] if the hole in context C is filled with e. We use this context to define the reduction rule for arbitrary expressions:

\frac{e ↦ e′}{C[e] ↦ C[e′]}

The single reduction step e ↦ e′ for a redex e consists of normal and exceptional reduction steps:

Normal reduction steps  Exceptional reduction steps ; \begin{matrix}(\underline{λ}x. e) t & ↦ & [t/x]e \\ \underline{handle} t (\underline{λ}x. e) & ↦ & t \end{matrix}  \underline{raise} t ↦ \overline{t} \underline{raise} \overline{t} ↦ \overline{t} \underline{handle} \overline{t} (\underline{λ}x. e) ↦ [t/x]e \overline{t} e ↦ \overline{t} (\underline{λ}x. e) \overline{t} ↦ \overline{t}

Normal reduction steps are not concerned with exceptions. Exceptional reduction steps specify the generation, propagation and handling of exceptions.

3.2 CPS Terms

Rather than working directly with DS terms, we transform them into CPS terms where the exception mechanism is captured by having a second (handler) continuation in addition to the regular (success) continuation. This transformation exposes the semantics of exceptions in the program text. We use the following grammar for CPS terms:

Root Terms  r ::= \underline{λ}k. e
Serious Terms  e ::= t_{0} t_{1} p | c t
Trivial Terms  t ::= \underline{λ}x. r | x | v
Continuation Pairs  p ::= \underline{pair}(c_{0} , c_{1}) | k
Continuation Terms  c ::= \underline{λ}x. e | \underline{λ}v. e | \underline{nrml} p | \underline{hnd_{0}} p | \underline{hnd_{1}} v p

Note that in the CPS syntax, we are distinguishing variables x which are parameters of functions or continuations from variables v which are only parameters to continuations. This distinction will be used to differentiate abstractions introduced by the transform from those already present in the DS term. \underline{nrml} and \underline{hnd_{0}} are essentially the projections for the continuation pairs; and \underline{hnd_{1}} is used to explicitly differentiate the case when a stacked intermediate value must be popped (aborted) to reach the handler.

The formal semantics are defined similarly to that for DS terms. However, rather than using special exception values (\overline{t}); exceptional flows (\underline{raise} and \underline{handle} expressions) are simulated by continuation functions. Let the set of result values, γ, consist of trivial terms and immediate functions:

γ ::= t | \underline{λ}x.e | \underline{λ}v.e | \underline{λ}k.e

An evaluation context C is extended for the cases of continuation pairs:

C ::= [ ] | C γ | γ C
| \underline{pair}(C , c) | \underline{pair}(γ , C)
| \underline{nrml} C | \underline{hnd_{0}} C | \underline{hnd_{1}} v C

The single reduction step e ↦ e′ for a redex e is:

Reduction steps

\begin{matrix}(\underline{λ}x. r)t & ↦ & [t/x]r \\ (\underline{λ}x. e)t & ↦ & [t/x]e \\ (\underline{λ}v. e)t & ↦ & [t/v]e \end{matrix} \underline{nrml} \underline{pair}(γ_{0} , γ_{1}) ↦ γ_{0}

\underline{hnd_{0}} \underline{pair}(γ_{0} , γ_{1}) ↦ γ_{1}
\underline{hnd_{1}} v \underline{pair}(γ_{0} , γ_{1}) ↦ γ_{1}

3.3 Continuation-passing-style (CPS) Transformation

We use an extension of the conventional continuation-passing-style (CPS) transformation [DF92, Plo75, Ste78] to get from a DS term to a CPS term. We remove the \underline{raise} and \underline{handle} expressions by passing two continuations to each expression: one for the normal course of execution, and a second one (the handler continuation) for exceptions.

Only \underline{raise} and \underline{handle} expressions use the handler continuation. A \underline{raise} expression is transformed to call the current handler continuation. A \underline{handle} expression is transformed to extend the handler function with the current handler continuation. For other expressions, the handler continuation is passively passed along, reflecting the dynamic scope of exceptions. Because [[−]]^{R} : DS Terms → Root Terms [[−]]^{E} : DS Expressions → Continuation Pairs → Serious Terms [[−]]^{T} : DS Trivial Expressions → Trivial Terms

In mnemonic CPS term syntax:

[[e]]^{R} = \underline{λ}⟨n, h⟩. T_{e} [[e]] ⟨n, h⟩
[[e_{0} e_{1}]]^{E} ⟨n, h⟩ = [[e_{0}]]^{E} ⟨\underline{λ}v_{0}. [[e_{1}]]^{E} ⟨\underline{λ}v_{1}. v_{0} v_{1} ⟨n, h⟩, h⟩ h⟩
[[\underline{handle} e_{0} (\underline{λ}x. e_{1})]]^{E} ⟨n, h⟩ = [[e_{0}]]^{E} ⟨n, \underline{λ}x. [[e_{1}]]^{E} ⟨n, h⟩⟩
[[\underline{raise} e]]^{E} ⟨n, h⟩ = [[e]]^{E} ⟨h, h⟩
[[t]]^{E} ⟨n, h⟩ = n [[t]]^{T}
[[x]]^{T} = x
[[\underline{λ}x. r]]^{T} = \underline{λ}x.[[r]]^{R}

In the exact CPS term syntax:

[[e]]^{R} = \underline{λ}k. [[e]]^{E} k
[[e_{0} e_{1}]]^{E} p = [[e_{0}]]^{E} \underline{pair}(\underline{λ}v_{0}. [[e_{1}]]^{E} \underline{pair}(\underline{λ}v_{1}. v_{0} v_{1} p , \underline{hnd_{1}} v_{0} p) , \underline{hnd_{0}} p)
[[\underline{handle} e_{0} (\underline{λ}x. e_{1})]]^{E} p = [[e_{0}]]^{E} \underline{pair}(\underline{nrml} p , \underline{λ}x. [[e_{1}]]^{E} p)
[[\underline{raise} e]]^{E} p = [[e]]^{E} \underline{pair}(\underline{hnd_{0}} p , \underline{hnd_{0}} p)
[[t]]^{E} p = (\underline{nrml} p) [[t]]^{T}
[[x]]^{T} = x
[[\underline{λ}x. r]]^{T} = \underline{λ}x.[[r]]^{R}

Figure 1: CPS transformation function [[−]]^{R}

the handler continuation encodes both how to handle a raised exception and how to proceed thereafter, we have to make the normal continuation ready to be captured by a handler continuation. Thus we keep passing two continuations (normal and handler continuations) to every expression.

Figure 1 shows the extended CPS transform in a conventional functional formulation: one in a mnemonic style and the other in our exact CPS term syntax. Notice the use of \underline{hnd_{1}} in the inner handler continuation of the application translation. That inner handler will only be invoked if the evaluation of e_{0} succeeds, pushing an intermediate value v_{0} onto the stack, and then the evaluation of e_{1} causes an exception. \underline{hnd_{1}} is necessary, rather than \underline{hnd_{0}}, because the stacked intermediate value v_{0} must be popped to reach the the inner handler sitting beneath v_{0} in the stack.

The correctness of this CPS transformation can be proven[KYD98] analogously to the proof of Plotkin’s simulation theorem [HD97, Plo75].

3.4 CPS Transformation as a Judgement

In order to represent the transform in OLF, we reformulate it as three mutually recursive judgements corresponding to [[−]]^{R}, [[−]]^{E}, and [[−]]^{T} in Figure 1. A direct-style term r is transformed into a CPS term r′ whenever the judgement

⊢ r ⟶^{DR} r′

is satisfied. Given a continuation pair p , a direct-style expression e is transformed into a CPS expression e′ whenever the judgement

⊢ e; p ⟶^{DE} e′

is satisfied. Finally, a direct-style trivial expression t is transformed into a CPS trivial expression t′ whenever the judgement

⊢ t ⟶^{DT} t′

is satisfied.

The derivation rules for the transform are as follows:

\frac{⊢ e; k ⟶^{DE} e′}{⊢ e ⟶^{DR} \underline{λ}k. e′}

\frac{⊢ t ⟶^{DT} t′}{⊢ t; p ⟶^{DE} (\underline{nrml} p) t′}  \frac{⊢ e; \underline{pair}(\underline{hnd_{0}} p , \underline{hnd_{0}} p) ⟶^{DE} e′}{⊢ \underline{raise} e; p ⟶^{DE} e′}

⊢ e_{1} ; \underline{pair}(\underline{λ}v_{1}. v_{0} v_{1} p , \underline{hnd_{1}} v_{0} p) ⟶^{DE} e′_{1} ⊢ e_{0} ; \underline{pair}(\underline{λ}v_{0}. e′_{1} , \underline{hnd_{0}} p) ⟶^{DE} e′ v_{0} not free

in conclusion

⊢ e_{0} e_{1} ; p ⟶^{DE} e′

\frac{⊢ e_{1} ; p ⟶^{DE} e′_{1} ⊢ e_{0} ; \underline{pair}(\underline{nrml} p , \underline{λ}x. e′_{1}) ⟶^{DE} e′}{⊢ \underline{handle} e_{0} (\underline{λ}x. e_{1}) ; p ⟶^{DE} e′}

\overline{⊢ x ⟶^{DT} x}  \frac{⊢ r ⟶^{DR} r′}{⊢ \underline{λ}x. r ⟶^{DT} \underline{λ}x. r′}

3.5 Invariants for Results of CPS Transform

Terms resulting from a left-to-right call-by-value CPS translation of direct-style terms satisfy an invariant on occurrences of continuation identifiers k and parameters v. We shall formalize this property with five mutually recursive judgements:

⊨^{Root} r  Φ ⊨^{Exp} e  Φ ⊨^{Triv} t; Φ′  Φ ⊨^{CPair} p  Φ ⊨^{Cont} c

where Φ is a stack of both continuation identifiers and parameters:

Φ ::= · | Φ, k | Φ, v

When Φ′ is a prefix of Φ, we define Φ − Φ′ as the remainder of Φ.

The derivation rules for these judgements are as follows:

\frac{k ⊨^{Exp} e}{⊨^{Root} \underline{λ}k. e}

\frac{Φ ⊨^{Triv} t; Φ′  Φ′ ⊨^{Cont} c}{Φ ⊨^{Exp} c t}  \frac{Φ ⊨^{Triv} t_{1}; Φ′ Φ′ ⊨^{Triv} t_{0}; Φ′′  Φ′′ ⊨^{CPair} p}{Φ ⊨^{Exp} t_{0} t_{1} p}

\overline{Φ ⊨^{Triv} x; Φ}  \frac{⊨^{Root} r}{Φ ⊨^{Triv} \underline{λ}x. r; Φ}  \overline{Φ, v ⊨^{Triv} v; Φ}

\overline{k ⊨^{CPair} k}  \frac{Φ ⊨^{Cont} c_{0}  Φ ⊨^{Cont} c_{1}}{Φ ⊨^{CPair} \underline{pair}(c_{0} , c_{1})}

\frac{Φ ⊨^{Exp} e}{Φ ⊨^{Cont} \underline{λ}x. e}  \frac{Φ, v ⊨^{Exp} e}{Φ ⊨^{Cont} \underline{λ}v. e}  \frac{Φ ⊨^{CPair} p}{Φ ⊨^{Cont} \underline{nrml} p}  \frac{Φ ⊨^{CPair} p}{Φ ⊨^{Cont} \underline{hnd_{0}} p}  \frac{Φ ⊨^{CPair} p}{Φ, v ⊨^{Cont} \underline{hnd_{1}} v p}

From the judgement rules, it is easy to see that continuation-pair identifiers, k, are used linearly in each root term, and that continuation parameters v (which were introduced by the CPS transform) form a stack in each serious term. In fact, the judgement actually implies the stronger property that continuation-pair identifiers and parameters are used together in a stack-like fashion. Each root term adds a new stack-frame, an identifier followed by parameters, which is fully consumed within that root term. This is apparent from the judgement on \underline{λ}x.r which requires that r not depend upon anything currently in the stack.

We now state one further property of our cps transform.

Lemma 2 ⊢ e; p ⟶^{DE} e′ and Φ ⊨^{CPair} p implies Φ ⊨^{Exp} e′.

Proof: By structural induction on ⊢ e; p ⟶^{DE} e′. For base case, ⊢ t; p ⟶^{DE} (\underline{nrml} p) t′, note that t′ ≠ v thus Φ ⊨^{Triv} t′; Φ for all Φ. □

We would like to prove that ⊢ r ⟶^{DR} r′ implies ⊨^{Root} r′. Proving this directly with the above definitions requires a logical relations style argument [DDP99, DP95]. However, by using an ordered logical framework, this may be proved directly.

4 Ordered Logical Framework Representation

In this section, we show how to represent the terms and transform of section 3 in OLF; and how these representations immediately give our desired proof. Following standard practice for LF-style logical frameworks, we shall represent judgements as types and derivations as terms [HHP93] ^{2}. Furthermore, we will take care that all of our representations are compositional bijections— 1) for every actual object represented there is a corresponding OLF object (and vice-versa); and 2) the representation function and its inverse both commute with substitution. These two properties allow us to transfer results for the representations back to the actual objects and vice-versa. Representations which are compositional bijections are sometimes referred to as adequate.

Our proof proceeds in the following manner.

2For representing abstract syntax (e.g. DS terms) we may view each syntactic category as a judgement and the constructors for terms of the category as derivation rules for the judgement.

1. We give a representation for DS terms which is in compositional bijection with all actual DS terms.

2. We give a representation for CPS terms which is in compositional bijection with only actual CPS terms satisfying the invariants; our representation does not capture all terms within the CPS grammar of section 3.2.

3. We give a representation for the CPS transform of section 3.4. This representation relates represented DS terms to represented CPS terms. Furthermore it is in compositional bijection with all possible CPS transformations.

4. By using the preceding compositional bijections, we conclude that ⊢ r ⟶^{DR} r′ implies ⊨^{Root} r′.

4.1 DS Terms

Our representation of DS terms will use three basic types corresponding to the three kinds of DS terms.

droot : type.  dexp : type.  dtriv : type.

We will then build our representations from term constructors corresponding to DS terms. Note that representation uses higher-order abstract syntax, so object-level functions are represented by meta-level functions and likewise object-level variables are represented (implicitly) by meta-level variables.

e2r : dexp → droot.
dapp : dexp → dexp → dexp.
handle : dexp → (dexp → dexp) → dexp.
raise : dexp → dexp.
t2e : dtriv → dexp.
dabort : dtriv.
dlam : (triv → droot) → dtriv.

Given the previous signature, there is an obvious compositional bijection between DS terms and canonical objects in the above signature. This bijection is established by the following mutually recursive representation functions, ⌜−⌝^{R},⌜−⌝^{E},⌜−⌝^{T}, and their inverses ⌞−⌟^{R},⌞−⌟^{E},⌞−⌟^{T}.

⌜e⌝^{R} = e2r ⌜e⌝^{E}  ⌞e2r E⌟_{R} = ⌞E⌟_{E}
⌜e_{0} e_{1}⌝^{E} = dapp ⌜e_{0}⌝^{E} ⌜e_{1}⌝^{E}  ⌞dapp E_{0} E_{1}⌟_{E} = ⌞E_{0}⌟_{E} ⌞E_{1}⌟_{E}
⌜\underline{handle} e_{0} (\underline{λ}x. e_{1})⌝^{E}  = handle ⌜e_{0}⌝^{E} (λx:dtriv. ⌜e_{1}⌝^{E})
⌞handle E_{0} (λx:dtriv. E_{1})⌟_{E} = \underline{handle} ⌞E_{0}⌟_{E} (\underline{λ}x. ⌞E_{1}⌟_{E})
⌜\underline{raise} e⌝^{E} = raise ⌜e⌝^{E}  ⌞raise E⌟_{E} = \underline{raise} ⌞E⌟_{E}
⌜t⌝^{E} = d2e ⌜t⌝^{T}  ⌞d2e T ⌟_{E} = ⌞T ⌟_{T}
⌜\underline{λ}x. r⌝^{T} = dlam (λx:dtriv. ⌜r⌝^{R})  ⌞dlam (λx:dtriv. R)⌟_{T} = \underline{λ}x. ⌞R⌟_{R}
⌜x⌝^{T} = x  ⌞x⌟_{T} = x

4.2 CPS Terms

Next, we give a representation of CPS terms satisfying the invariants of section 3.5. The key idea behind this representation is that ordered types implicitly capture the invariants. Thus, we can directly represent CPS terms which satisfy the invariants, without explicitly representing the invariants. Our representation will use five basic types corresponding to the five basic kinds of CPS terms.

root : type.  exp : type.  triv : type.  cont : type.  cpair : type.

We will then build our representations from term constructors corresponding to CPS terms. The use of ordered types forces the CPS term representations to satisfy the invariants.

klam : (cpair ↠ exp) → root.
app : cpair ↠ triv ↠ triv ↠ exp.
kapp : cont ↠ triv ↠ exp.
lam : (triv → root) → triv.
xlam : (triv → exp) ↠ cont.
vlam : (triv ↠ exp) ↠ cont.
nrml : cpair ↠ cont.
hnd_{0} : cpair ↠ cont.
hnd_{1} : cpair ↠ triv ↠ cont.
pair : (cont & cont) ↠ cpair.

Note that a positive occurrence of an unrestricted function → as in the type of klam imposes a restriction on the corresponding argument: it may not depend upon continuation-pairs k nor parameters v which are always ordered variables. On the other hand, a negative occurrence of → as in the type of lam licenses the unrestricted use of the corresponding bound variable x. The right ordered functions ↠ impose the stack-like discipline on parameters of continuations and the continuation-pairs themselves.

Given the previous signature, there is a compositional bijection between CPS terms satisfying the occurrence conditions and canonical objects in the above signature. This bijection is established by the following representation function, ⌜−⌝ and its inverse ⌞−⌟.

⌜\underline{λ}k. e⌝ = klam (λ^{>}k:cpair. ⌜e⌝)  ⌞klam (λ^{>}k:cpair. E)⌟ = \underline{λ}k. ⌞E⌟

⌜t_{0} t_{1} p⌝ = app^{>}⌜p⌝^{>}⌜t_{0}⌝^{>}⌜t_{1}⌝  ⌞app^{>}P^{>}T_{0}^{>}T_{1}⌟ = ⌞T_{0}⌟ ⌞T_{1}⌟ ⌞P ⌟
⌜c t⌝ = kapp^{>}⌜c⌝^{>}⌜t⌝  ⌞kapp^{>}C^{>}T ⌟ = ⌞C⌟ ⌞T ⌟
⌜\underline{λ}x. r⌝ = lam (λx:triv. ⌜r⌝)  ⌞lam (λx:triv. R)⌟ = \underline{λ}x. ⌞R⌟
⌜x⌝ = x  ⌞x⌟ = x
⌜v⌝ = v  ⌞v⌟ = v
⌜\underline{λ}x. e⌝ = xlam^{>}(\underline{λ}x:triv. ⌜e⌝)  ⌞xlam^{>}(\underline{λ}x:triv. E)⌟ = \underline{λ}x. ⌞E⌟
⌜\underline{λ}v. e⌝ = vlam^{>}(λ^{>}v:triv. ⌜e⌝)  ⌞vlam^{>}(λ^{>}v:triv. E)⌟ = \underline{λ}v. ⌞E⌟
⌜\underline{nrml} p⌝ = (nrml^{>}⌜p⌝)  ⌞nrml^{>}P ⌟ = \underline{nrml} ⌞P ⌟
⌜\underline{hnd_{0}} p⌝ = (hnd_{0}^{>}⌜p⌝)  ⌞hnd_{0}^{>}P ⌟ = \underline{hnd_{0}} ⌞P ⌟
⌜\underline{hnd_{1}} t p⌝ = (hnd_{1}^{>}⌜p⌝^{>}⌜t⌝)  ⌞hnd_{1}^{>}P^{>}T ⌟ = \underline{hnd_{1}} ⌞T ⌟ ⌞P ⌟
⌜k⌝ = k  ⌞k⌟ = k
⌜\underline{pair}(c_{0} , c_{1})⌝ = pair^{>}⟨⌜c_{0}⌝ , ⌜c_{1}⌝⟩  ⌞pair^{>}⟨C_{0} , C_{1}⟩⌟ = \underline{pair}(⌞C_{0}⌟ , ⌞C_{1}⌟)

Note that and ⌞⌜u⌝⌟ = u for any term u. Additionally, since variables are mapped to variables, the representation function and its inverse are compositional (i.e., commute with substitution).

We formally prove the correspondence in two parts.

Theorem 3 (Representations are Canonical Forms) Consider CPS terms r, e, t, c and p with free ordinary variables among x_{1}, …, x_{n}. Let Γ = x_{1}:triv … x_{n}:triv.

1. If ⊨^{Root} r then Γ; · ⊢ ⌜r⌝ ⇑ root.

2. If Φ ⊨^{Exp} e then Γ; ⌜Φ⌝ ⊢ ⌜e⌝ ⇑ exp.

3. If Φ ⊨^{Triv} t; Φ′ then Γ; ⌜Φ − Φ′⌝ ⊢ ⌜t⌝ ⇑ triv.

4. If Φ ⊨^{Cont} c then Γ; ⌜Φ⌝ ⊢ ⌜c⌝ ⇑ cont.

5. If Φ ⊨^{CPair} p then Γ; ⌜Φ⌝ ⊢ ⌜p⌝ ⇑ cpair.

Proof: By induction on the structure of the given derivations. □

Theorem 4 (Canonical Forms are Representations) Let Γ = x_{1}:triv, …, x_{n}:triv be given.

1. For any M such that Γ; · ⊢ M ⇑ root, ⌞M⌟ is defined and ⊨^{Root} ⌞M⌟.

2. For any Ω = v_{1}:triv, …, v_{m}:triv and M such that Γ; k:cpair, Ω ⊢ M ⇑ exp, ⌞M⌟ is defined and ⌞Ω⌟ ⊨^{Exp} ⌞M⌟.

3. For any Ω = v_{1}:triv, …, v_{m}:triv and M such that Γ; Ω ⊢ M ⇑ triv, ⌞M⌟ is defined and Φ, ⌞Ω⌟ ⊨^{Triv} ⌞M⌟; Φ for any Φ.

4. For any Ω = v_{1}:triv, …, v_{m}:triv and M such that Γ; k:cpair, Ω ⊢ M ⇑ cont, ⌞M⌟ is defined and ⌞Ω⌟ ⊨^{Cont} ⌞M⌟.

5. For any Ω = v_{1}:triv, …, v_{m}:triv and M such that Γ; k:cpair, Ω ⊢ M ⇑ cpair, ⌞M⌟ is defined and ⌞Ω⌟ ⊨^{CPair} ⌞M⌟.

Proof: By induction on the structure of the given canonical derivations. For the cases when M = lam (λx:triv. r), and M = klam (λ^{>}k:(triv → exp). e) note that the ordered context Ω must be empty since no ordered variables can occur in the argument to an intuitionistic application. □

5 CPS Transform

We represent CPS transform with three basic types corresponding to the three judgements of the transform.

cps r : droot → root → type.  cps e : dexp → cpair → exp → type.  cps t : dtriv → triv → type.

We then use the following terms to construct representations of the CPS transform.

cps root : ΠE:dexp. ΠE′:cpair ↠ exp.

(Πk:cpair. cps e E k (E′^{>}k)) → cps r (e2r E) (klam E′).

cps triv : ΠT:dtriv. ΠP:cpair. ΠT′:triv.

cps t T T′ → cps e (t2e T) P (kapp^{>}(nrml^{>}P)^{>}T′).

cps raise : ΠE:dexp. ΠE′:exp. ΠP:cpair.

cps e E (pair^{>}⟨hnd_{0}^{>}P , hnd_{0}^{>}P ⟩) E′→ cps e (raise E) P E′.

cps app : ΠE_{0}:dexp. ΠE_{1}:dexp. ΠP:cpair. ΠE′_{1}:triv ↠ exp. ΠE′:exp.

cps e E_{0} (pair^{>}⟨vlam^{>}E′_{1} , hnd_{0}^{>}P ⟩) E′→ (Πv_{0}:triv. cps e E_{1} (pair^{>}⟨vlam^{>}λ^{>}v_{1}:triv. app^{>}P^{>}v_{0}^{>}v_{1} , hnd_{1}^{>}P^{>}v_{0}⟩) (E′_{1}^{>}v_{0}))→ cps e (dapp E_{0} E_{1}) P E′.

cps handle : ΠE_{0}:dexp. ΠE_{1}:dtriv → droot. ΠE′_{1}:dtriv → droot. ΠP:cpair. ΠE′:exp.

cps e E_{0} (pair^{>}⟨nrml^{>}P , xlam^{>}E′_{1}⟩) E′→ (Πx:dtriv. Πx′:triv. cps t x x′ → cps e (E_{1} x) P (E′_{1} x′))→ cps e (handle E_{0} E_{1}) P E′.

cps lam : ΠR:dtriv → droot. ΠR′:triv → root.

(Πx:dtriv. Πx′:triv. cps t x x′ → cps r (R x) (R′ x′))→ cps t (dlam R) (lam R′).

We may now show the adequacy of above representation in two parts. In the actual transformation we map variables x to themselves; in the representation we

map each variable x from a DS term to a corresponding variable x′ in a CPS term^{3}. These variables and their relationship are captured in contexts

Γ = x_{1}:dtriv … x_{n}:dtriv
Γ′ = x′_{1}:triv … x′_{n}:triv
Γ_{m} = m_{1}:cps t x_{1} x′_{1} … m_{n}:cps t x_{n} x′_{n}

which always occur together in this manner. In addition we have contexts

Γ_{k} = k_{1}:cpair … k_{m}:cpair
Γ_{v} = v_{1}:triv … v_{l}:triv

which include all the continuation-pair identifiers k and temporary variables v which may occur in the continuation-pair p and CPS terms resulting from the translation. Note that ordering constraints are ignored during the translation, but will be nonetheless be satisfied by the resulting terms.

Theorem 5 (Representations are Canonical Forms) Let Γ^{∗} = Γ, Γ′, Γ_{m}, Γ_{k}, Γ_{v} be a context of the form explained above which contains all free variables occurring in the relevant judgement. Then

1. ⊢ r ⟶^{DR} r′ implies ∃M. Γ^{∗}; · ⊢ M ⇑ cps r ⌜r⌝^{R} ⌜r′⌝.

3This is accomplished by the cps lam rule.

2. ⊢ e; p ⟶^{DE} e′ and Φ ⊨^{CPair} p implies ∃M. Γ^{∗}, ⌜Φ⌝; · ⊢ M ⇑ cps e ⌜e⌝^{E} ⌜p⌝ ⌜e′⌝

3. ⊢ t ⟶^{DT} t′ implies ∃M. Γ^{∗}; · ⊢ M ⇑ cps t ⌜t⌝^{T} ⌜t′⌝

Proof: By structural induction on the given derivation making use of Lemma 2. □

Theorem 6 (Canonical Forms are Representations) Let Γ^{∗} = Γ, Γ′, Γ_{m}, Γ_{k}, Γ_{v} a context of the form explained above and assume the types below are canonical.

1. Γ^{∗}; · ⊢ M ⇑ cps r R R′ implies ⊢ ⌞R⌟_{R} ⟶^{DR} ⌞R′⌟.

2. Γ^{∗}; · ⊢ M ⇑ cps e E P E′ implies ⊢ ⌞E⌟_{E} ; ⌞P ⌟ ⟶^{DE} ⌞E′⌟.

3. Γ^{∗}; · ⊢ M ⇑ cps t T T′ implies ⊢ ⌞T ⌟_{T} ⟶^{DR} ⌞T′⌟.

Proof: By structural induction on the given canonical derivation. □

The adequacy of our representation gives us a simple proof that the terms resulting from a CPS transformation satisfy the occurrence conditions of section 3.2.

Theorem 7 ⊢ r ⟶^{DR} r′ implies ⊨^{Root} r′.

Proof: By theorem 5 we know ·; · ⊢ ⌜r′⌝ ⇑ root. Then by theorem 4 we know ⊨^{Root} ⌞⌜r′⌝⌟. Then we are done since ⌞⌜r′⌝⌟ = r′. □

The simplicity of the proof above may be surprising. It is so direct, because the work has been distributed to the proof of the adequacy theorems (which are clearly not trivial), combined with some deep properties of the logical framework such as the existence of canonical forms. This factoring of effort is typical in the use of logical frameworks.

6 Related Work

O’Hearn and Berdine have shown that the CPS transform with exceptions produces CPS terms which use their continuation-pair argument linearly [O’H00]. This work refines that analysis and shows that the immediate result of the transform actually uses the continuationpair argument in an ordered fashion. However, our results are brittle in the sense that the ordering property is not preserved by arbitrary β reduction— β reducing underneath a lambda could result in a term which doesn’t satisfy the ordering invariants.

In [PP00], Polakow and Pfenning show how OLF provides a convenient setting for reasoning about the CPS transform which doesn’t treat exceptions. This work shows how those representation techniques easily extend to treat the CPS transform which removes exceptions.

7 Conclusion & Future Work

We formally proved the stackability and linearity of exception handlers with ML-style semantics using the help of an ordered logical framework (OLF) [PP00]. We transformed exceptions into continuation-passing-style (CPS) terms and formalizeed the exception properties as a judgement on the CPS terms. Then, rather than directly proving that the properties hold for terms, we proved our theorem for OLF representations of the CPS terms and transform. We used the correctness of our representations to transfer the results back to the actual CPS terms and transform. We further showed that the results in [DP95, DDP99] carry-over to the extended CPS transform which removes exceptions. Working with OLF representations allowed for a relatively simple proof in which we could directly use known properties of OLF terms (e.g. substitution properties) rather than re-proving similar properties for actual CPS terms satisfying our invariants.

We can also extend our analysis to cover evaluation of CPS terms. The invariants satisfied by CPS-transformed terms clearly suggest a stack-like evaluation mechanism. In fact, we can show (though space doesn’t permit it in this paper) that a stack-like evaluation machine for CPS terms, which takes advantage of the ordering invariants, behaves the same as a regular evaluation machine which always uses substitution.

Our work can be seen as two-fold: it is a theoretical justification of existing compilers that use the stack mechanism to implement exceptions; and it demonstrates the value of a (ordered) logical framework as a conceptual tool in the theoretical study of programming languages. We conjecture that many systems with constrained resource access will have a natural representation in an ordered logical framework.

8 Acknowledgements

We would like to acknowledge insightful discussions with Peter O’Hearn and Frank Pfenning.

References

[App97] Andrew W. Appel. Modern Compiler Implementation in ML/C/Java: Basic Techniques. Cambridge University Press, 1997.

[CP99] Iliano Cervesato and Frank Pfenning. A linear logical framework. Information and Computation, 1999. To appear in the special issue with invited papers from LICS’96, E. Clarke, editor.

[DDP99] Olivier Danvy, Belmina Dzafic, and Frank Pfenning. On proving syntactic properties of cps programs. In Third International Workshop on Higher Order Operational Techniques in Semantics (HOOTS’99), Paris, France, September 1999.

[DF92] Olivier Danvy and Andrzej Filinski. Representing control: a study of the CPS transformation. Mathematical Structures in Computer Science, 2(4):361–391, December 1992.

[DP95] Olivier Danvy and Frank Pfenning. The occurrence of continuation parameters in CPS terms. Technical Report CMU-CS-95-121, Department of Computer Science, Carnegie Mellon University, February 1995.

[Fel87] Matthias Felleisen. The Calculi of λ-v-CS Conversion: A Syntactic Theory of Control and State in Imperative Higher-Order Programming Languages. PhD thesis, Department of Computer Science, Indiana University, Bloomington, Indiana, August 1987.

[HD97] John Hatcliff and Olivier Danvy. Thunks and the λ-calculus. Journal of Functional Programming, 7(3):303–320, 1997.

[HHP93] Robert Harper, Furio Honsell, and Gordon Plotkin. A framework for defining logics. Journal of the Association for Computing Machinery, 40(1):143–184, January [KYD98] Jungtaek Kim, Kwangkeun Yi, and Olivier Danvy. Assessing the overhead of

ml exceptions by selective cps transformation. In The Proceedings of the ACM SIGPLAN Workshop on ML, pages 103–114, September 1998.

[LDG^{+}00] Xavier Leroy, Damien Doligez, Jacques Garrigue, Didier Rémy, and Jérôme Vouillon. The objective caml system (relase 3.00), documentation and user’s manual. http://caml.inria.fr/ocaml/htmlman/index.html, 2000.

[MTHM97] Robin Milner, Mads Tofte, Robert Harper, and David MacQueen. The Definition of Standard ML (Revised). MIT Press, 1997.

[O’H00] P.W. O’Hearn. Personal communication with author. May 2000.

[Pfe96] Frank Pfenning. The practice of logical frameworks. In Hélène Kirchner, editor, Proceedings of the Colloquium on Trees in Algebra and Programming, pages 119– 134, Linköping, Sweden, April 1996. Springer-Verlag LNCS 1059. Invited talk.

[Plo75] Gordon D. Plotkin. Call-by-name, call-by-value and the λ-calculus. Theoretical Computer Science, 1:125–159, 1975.

[Plo81] Gordon D. Plotkin. A structural approach to operational semantics. Technical report, Aarhus University, September 1981.

[PP99a] Jeff Polakow and Frank Pfenning. Natural deduction for intuitionistic noncommutative linear logic. In J.-Y. Girard, editor, Proceedings of the Fourth International Conference on Typed Lambda Calculi and Applications (TLCA’99), pages 295–309, l’Aquila, Italy, April 1999. Springer-Verlag LNCS 1581.

[PP99b] Jeff Polakow and Frank Pfenning. Relating natural deduction and sequent calculus for intuitionistic non-commutative linear logic. In Andre Scedrov and Achim Jung, editors, Proceedings of the 15th Conference on Mathematical Foundations of Programming Semantics, pages 311–328, New Orleans, Louisiana, April 1999. Electronic Notes in Theoretical Computer Science, Volume 20.

[PP00] Jeff Polakow and Frank Pfenning. Properties of terms in continuation passing style in an ordered logical framework. In Workshop on Logical Frameworks and Meta-Languages (LFM 2000), Santa Barbara, California, June 2000.

[Ste78] Guy L. Steele Jr. Rabbit: A compiler for Scheme. Technical Report AI-TR-474, Artificial Intelligence Laboratory, Massachusetts Institute of Technology, Cambridge, Massachusetts, May 1978.