ROPAS

Research On Program Analysis System

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

ROPAS MEMO 2000-6 July 13, 2000

Verification of Machine Codes Using An Effect Type System

Jaeyoun Chung, Sukyoung Ryu and Kwangkeun Yi

                      {jay,puppy,kwang}@ropas.kaist.ac.kr

July 13, 2000

Abstract We devise a mechanism to verify the safety of machine codes. We design a stack based machine etySECK whose code part is annotated with types and effects. And we propose an effect type system to verify properties of etySECK programs. Our system analyzes memory effects as a property of programs and we can extend our system to analyze other effects.

1 Effect-Typed Abstract Machine : etySECK

The etySECK machine is a variant of Landin’s SECD [1, 2, 3, 4] machine with type and effect annotations. The syntax and the semantics of the machine is described in Figure 1 and 2, respectively. Since the machine supports functional values, compilation from functional languages to this machine is not difficult. Throughout this paper, we use dot(.) as a list constructing operator and use a single value for a list of length one.

1.1 Syntax

A machine configuration consists of six components – a stack, a heap, an environment, a sequence of commands, a continuation and a set of effects of memory behaviors. The stack and the environment are just lists of values. Each command may consume several values from the stack and produce a result on the stack. The environment represents a lexically enclosing environment and the commands access the values in the environment. The continuation is a list of pairs of an environment and a code. Each pair of the continuation is a frozen state of the machine when the function application appears by the app command. The set of effects is a trace of memory behaviors which have occurred until the machine configuration reaches at the current state.

A memory region is a set of memory locations which are assumed to be allocated to the same block of the memory. Our system analyzes observable side-effects of memory behaviors – init, read, write – for regions.

The values are either primitive values, a location, or function values. A function value is a triple of its type, the function’s body, and an environment for static binding. A polymorphic value is either fn or rfn and it can be instantiated to a concrete monomorphic value.

The type is either an integer type, a boolean type, a unit type, a location type, a function type, a type variable, or a polymorphic type. A location type indicates that a value of this type is a location pointer to a value in the heap. A function type is annotated with a latent effect indicating a possible set of effects during the execution of the function’s body.

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

Machine Configuration: (S, H, E, C, K, φ)

S ∈ Stack = Value list  stack
H ∈ Heap = Loc → Value  heap
E ∈ Env = Value list  environment
K ∈ Cont = (Env × Cmds) list continuation

Region ∋ ρ  ::= r_{i}  region constant
| ρ_{i}  region variable
Effect ∋ φ ::= ϵ no effect
| {init(ρ)}  memory allocated
| {read(ρ)}  memory read
| {write(ρ)}  memory write
| φ ∪ φ′  effect composition
Type ∋ τ ::= i | b integer, boolean
| unit  unit type
| ref_{ρ}τ  location type
| τ→^{φ}τ  function type
| α  type variable
| ∀(α⃗, ρ⃗).τ  polymorphic type
Prim.Value ∋ p ::= n | true | false | ()
Value ∋ v  ::= p  primitive values
| l_{ρ}  location
| fn(τ, C, E)  function
| rfn(τ, C, E)  recursive function
| Λ(α⃗, ρ⃗).v  polymorphic value
Cmd ∋ C  ::= nil

| frame.C  | deframe.C

| fetch(n).C | quote(p).C
| add.C  | cond(C_{1}, C_{2}).C
| fn(∀α⃗, ρ⃗.C_{f} : τ_{1}→^{φ}τ_{2}).C
| rfn(∀α⃗, ρ⃗.C_{f} : τ_{1}→^{φ}τ_{2}).C

| app.C

| tapp(τ⃗, ρ⃗).C
| ref(ρ).C | get.C | set.C

Figure 1: Machine Configuration of etySECK (S, H, E, nil, (E′, C).K, φ)⇒(S, H, E′, C, K, φ)

(v.S, H, E, frame.C, K, φ)⇒(S, H, v.E, C, K, φ)

(S, H, v.E, deframe.C, K, φ)⇒(S, H, E, C, K, φ)

(S, H, v_{0}. · · · .v_{n}.E, fetch(n).C, K, φ)⇒(v_{n}.S, H, v_{0}. · · · .v_{n}.E, C, K, φ)

(S, H, E, quote(p).C, K, φ)⇒(p.S, H, E, C, K, φ)

(i_{2}.i_{1}.S, H, E, add.C, K, φ)⇒(i_{1} + i_{2}.S, H, E, C, K, φ)

(true.S, H, E, cond(C_{1}, C_{2}).C, K, φ)⇒(S, H, E, C_{1}.C, K, φ)

(false.S, H, E, cond(C_{1}, C_{2}).C, K, φ)⇒(S, H, E, C_{2}.C, K, φ)

(S, H, E, fn(∀α⃗, ρ⃗.C′ : τ_{1}→^{φ_{f}}τ_{2}).C, K, φ)⇒(Λ(α⃗, ρ⃗).fn(τ_{1}→^{φ_{f}}τ_{2}, C′, E).S, H, E, C, K, φ)

(S, H, E, rfn(∀α⃗, ρ⃗.C′ : τ_{1}→^{φ_{f}}τ_{2}).C, K, φ)⇒(Λ(α⃗, ρ⃗).rfn(τ_{1}→^{φ_{f}}τ_{2}, C′, E).S, H, E, C, K, φ)

(v.fn(τ_{1}→^{φ_{f}}τ_{2}, C_{f}, E_{f}).S, H, E, app.C, K, φ)⇒(S, H, v.E_{f}, C_{f}, (E, C).K, φ)

(v.rfn(τ_{1}→^{φ_{f}}τ_{2}, C_{f}, E_{f}).S, H, E, app.C, K, φ)⇒(S, H, v.rfn(τ_{1}→^{φ_{f}}τ_{2}, C_{f}, E_{f}).E_{f}, C_{f}, (E, C).K, φ)

(Λ(α⃗, ρ⃗).fn(τ_{1}→^{φ_{f}}τ_{2}, C_{f}, E_{f}).S, H, E, tapp(τ⃗, r⃗).C, K, φ)⇒

([τ_{i}/α_{i}, r_{i}/ρ_{i}]fn(τ_{1}→^{φ_{f}}τ_{2}, C_{f}, E_{f}).S, H, E, C, K, φ)

(Λ(α⃗, ρ⃗).rfn(τ_{1}→^{φ_{f}}τ_{2}, C_{f}, E_{f}).S, H, E, tapp(τ⃗, r⃗).C, K, φ)⇒

([τ_{i}/α_{i}, r_{i}/ρ_{i}]rfn(τ_{1}→^{φ_{f}}τ_{2}, C_{f}, E_{f}).S, H, E, C, K, φ)

(v.S, H, E, ref(ρ).C, K, φ)⇒(l_{ρ}.S, H[l_{ρ} → v], E, C, K, φ ∪ {init(ρ)}) l_{ρ} ∉ Dom(H)

(l_{ρ}.S, H, E, get.C, K, φ)⇒(H(l_{ρ}).S, H, E, C, K, φ ∪ {read(ρ)}) l_{ρ} ∈ Dom(H)

(v.l_{ρ}.S, H, E, set.C, K, φ)⇒(().S, H[l_{ρ} → v], E, C, K, φ ∪ {write(ρ)}) l_{ρ} ∈ Dom(H)

Figure 2: Machine Transition Rules of etySECK

1.2 Semantics

The semantics of our language is described by the transition relations (⇒) in Figure 2.

If the current sequence of commands is empty (nil), the first element of the continuation replaces the current environment and the commands:

(S, H, E, nil, (E′, C).K, φ)⇒(S, H, E′, C, K, φ).

Each instruction may take some values from the top of the stack and put a result value on the stack. The frame moves the stack top value into the environment and the deframe removes the value on the top of the environment:

(v.S, H, E, frame.C, K, φ) ⇒ (S, H, v.E, C, K, φ)
(S, H, v.E, deframe.C, K, φ) ⇒ (S, H, E, C, K, φ).

The fetch(n) gets the n-th value from the environment and puts the value on the stack. A new constant value p is put on the stack by the quote. The add gets two values from the stack and puts the sum on the stack. The cond(C_{1}, C_{2}) branches to either C_{1} or C_{2} according to the truth value of the stack top.

Function values are produced by the fn or the rfn. Let’s consider the fn rule:

(S, H, E, fn(∀α⃗, ρ⃗.C′ : τ_{1}→^{φ_{f}}τ_{2}).C, K, φ)⇒(Λ(α⃗, ρ⃗).fn(τ_{1}→^{φ_{f}}τ_{2}, C′, E).S, H, E, C, K, φ).

Note that produced values are polymorphic functions which cannot be directly used but should be instantiated to monomorphic ones by the tapp:

(Λ(α⃗, ρ⃗).fn(τ_{1}→^{φ_{f}}τ_{2}, C_{f}, E_{f}).S, H, E, tapp(τ⃗, r⃗).C, K, φ)⇒

([τ_{i}/α_{i}, r_{i}/ρ_{i}]fn(τ_{1}→^{φ_{f}}τ_{2}, C_{f}, E_{f}).S, H, E, C, K, φ).

When the app applies the argument on the stack top to the function on the second of the stack, the function value is already instantiated to a monomorphic one. The following rule is for applying non-recursive functions:

(v.fn(τ_{1}→^{φ_{f}}τ_{2}, C_{f}, E_{f}).S, H, E, app.C, K, φ)⇒(S, H, v.E_{f}, C_{f}, (E, C).K, φ).

In case of applying recursive functions, the recursive function value is also placed on the environment so that the function value is visible during the evaluation of the function’s body.

Operations on the heap are ref, get, and set. The ref allocates a memory cell, stores the stack top value to it, and places the location of the cell on the stack:

(v.S, H, E, ref(ρ).C, K, φ)⇒(l_{ρ}.S, H[l_{ρ} → v], E, C, K, φ ∪ {init(ρ)}) l_{ρ} ∉ Dom(H).

The get fetches a value from the heap and the set updates a value in the heap. Note that each operation on the heap produces a corresponding effect.

The etySECK machine starts from the initial configuration with all components except the commands are empty. The machine stops when both the commands and the continuation are empty or there is no transition rule to apply. The former case is when the machine terminates normally and the latter case is when the machine is in a stuck configuration. We define these cases as follows:

Definition 1 (Normal Termination) Program C terminates normally if

(nil, ϕ, nil, C, nil, ϕ) ⇒^{⋆} (S, H, E, nil, nil, φ).

Definition 2 (Stuck Configuration) The etySECK machine configuration (S, H, E, C, K, φ) (C ≠nil, K ≠ nil) is in a stuck configuration if there is no (S′, H′, E′, C′, K′, φ′) such that (S, H, E, C, K, φ)⇒(S′, H′, E′, C′, K′, φ′).

1.3 Type System

The type of a machine configuration is defined by the following judgement:

(S, H, E, C, K, φ) ⇝ (s_{o}, e_{o}, φ_{o}).

This judgement means that if a given machine configuration continues its execution to a final configuration then the stack, the environment, and the effects of the final configuration have the types s_{o}, e_{o}, and the effects φ_{o}, respectively. Figure 3 defines these typing rules.

In order to determine the type of a given machine configuration, we need to execute the configuration abstractly – that is, we need to execute it based on the type system. Typing

• (S, H, E, C, K, φ) ⇝ (s_{o}, e_{o}, φ_{o})

\begin{aligned}H ⊧ S : s_{1} & H ⊧ E : e_{1} & H ⊧ K : k_{1} & ⟨s_{1}, e_{1}, k_{1}, φ⟩ ⊢ C ⇝ ⟨s_{o}, e_{o}, φ_{o}⟩ \\ & (S, H, E, C, K, φ) ⇝ (s_{o}, e_{o}, φ_{o}) \end{aligned}

• H ⊧ S : s, H ⊧ E : e, H ⊧ K : k

H ⊧ nil : nil \begin{matrix}H ⊧ v : τ & H ⊧ S : s \\ H ⊧ v.S : τ.s \end{matrix}

\begin{matrix}H ⊧ v : τ & H ⊧ E : e \\ H ⊧ v.E : τ.e \end{matrix}  \begin{matrix}H ⊧ E : e & H ⊧ K : k \\ H ⊧ (E, C).K : (e, C).k \end{matrix}
• H ⊧ v : τ
H ⊧ p : type of(p)  \begin{matrix}l_{ρ} ∈ Dom(H) & H ⊧ H(l_{ρ}) : τ \\ H ⊧ l_{ρ} : ref_{ρ}τ \end{matrix}

\begin{aligned}H ⊧ E_{f} : e & ⟨ϵ, τ_{1}.e, ϵ, ϵ⟩ ⊢ C_{f} ⇝ ⟨τ_{2}, τ_{1}.e, φ′_{f}⟩ φ′_{f} ⊆ φ_{f} \\ & H ⊧ fn(τ_{1}→^{φ_{f}}τ_{2}, C_{f}, E_{f}) : τ_{1}→^{φ_{f}}τ_{2} \end{aligned}

\begin{aligned}H ⊧ E_{f} : e & ⟨ϵ, τ_{1}.τ_{1}→^{φ_{f}}τ_{2}.e, ϵ, ϵ⟩ ⊢ C_{f} ⇝ ⟨τ_{2}, τ_{1}.τ_{1}→^{φ_{f}}τ_{2}.e, φ′_{f}⟩ φ′_{f} ⊆ φ_{f} \\ & H ⊧ rfn(τ_{1}→^{φ_{f}}τ_{2}, C_{f}, E_{f}) : τ_{1}→^{φ_{f}}τ_{2} \end{aligned}

H ⊧ fn(τ_{1}→^{φ_{f}}τ_{2}, C_{f}, E_{f}) : τ_{1}→^{φ_{f}}τ_{2} H ⊧ E_{f} : e  α_{i}, ρ_{i} ∉ FTV(e)

H ⊧ Λ(α⃗, ρ⃗).fn(τ_{1}→^{φ_{f}}τ_{2}, C_{f}, E_{f}) : ∀(α⃗, ρ⃗).τ_{1}→^{φ_{f}}τ_{2}

H ⊧ rfn(τ_{1}→^{φ_{f}}τ_{2}, C_{f}, E_{f}) : τ_{1}→^{φ_{f}}τ_{2} H ⊧ E_{f} : e  α_{i}, ρ_{i} ∉ FTV(e)

H ⊧ Λ(α⃗, ρ⃗).rfn(τ_{1}→^{φ_{f}}τ_{2}, C_{f}, E_{f}) : ∀(α⃗, ρ⃗).τ_{1}→^{φ_{f}}τ_{2}

Figure 3: Typing Rules for etySECK (1) a machine configuration consists of typing a stack, an environment, a continuation, and a sequence of commands:

\begin{aligned}H ⊧ S : s_{1} & H ⊧ E : e_{1} & H ⊧ K : k_{1} & ⟨s_{1}, e_{1}, k_{1}, φ⟩ ⊢ C ⇝ ⟨s_{o}, e_{o}, φ_{o}⟩ \\ & (S, H, E, C, K, φ) ⇝ (s_{o}, e_{o}, φ_{o}) \end{aligned}.

The judgements H ⊧ S : s, H ⊧ E : e, and H ⊧ K : k mean that for a given heap H, a stack S, an environment E, and a continuation K have types s, e, and k, respectively. The type of a stack is a list of the types whose values are in the stack:

H ⊧ nil : nil  \begin{matrix}H ⊧ v : τ & H ⊧ S : s \\ H ⊧ v.S : τ.s \end{matrix}.

Types of an environment and a continuation are also lists of the types whose values are in those components.

The judgement H ⊧ v : τ means that for a given heap H a value v has a type τ. Since the type of a location l_{ρ} is determined by the value stored in the heap, we need H for the value typing:

\begin{matrix}l_{ρ} ∈ Dom(H) & H ⊧ H(l_{ρ}) : τ \\ H ⊧ l_{ρ} : ref_{ρ}τ \end{matrix}.

A location value l_{ρ} has a type ref_{ρ}τ if a value stored in the location has a type τ. We assume that there is a function type of which is a mapping from primitive values to their types. The type of a function value is determined by checking whether the annotated type is correct:

\begin{aligned}H ⊧ E_{f} : e & ⟨ϵ, τ_{1}.e, ϵ, ϵ⟩ ⊢ C_{f} ⇝ ⟨τ_{2}, τ_{1}.e, φ′_{f}⟩ φ′_{f} ⊆ φ_{f} \\ & H ⊧ fn(τ_{1}→^{φ_{f}}τ_{2}, C_{f}, E_{f}) : τ_{1}→^{φ_{f}}τ_{2} \end{aligned}.

Note that the actual effects of executing the function’s body may be less than the annotated effects.

We define the type of a sequence of commands as follows:

⟨s, e, k, φ⟩ ⊢ C ⇝ ⟨s_{o}, e_{o}, φ_{o}⟩.

This judgement means that if a given machine configuration which has a stack, an environment, a continuation of types s, e, k, respectively, effects φ, and a sequence of commands C continues its execution to a final configuration, then the types of the stack, the environment, and the effects of the final configuration are s_{o}, e_{o}, φ_{o}, respectively. Figure 4 defines the typing rules.

If the sequence of commands is empty, there are two possible typing rules. Rule nil describes that if both the commands and the continuation are empty, this configuration is a final state. Rule nilk states that if only the commands are empty but the continuation is not empty, the machine replaces the environment and the commands by the first element of the continuation and keeps going on:

\begin{matrix}⟨s, e′, k, φ⟩ ⊢ C′ ⇝ ⟨s_{o}, e_{o}, φ_{o}⟩ \\ ⟨s, e, (e′, C′).k, φ⟩ ⊢ nil ⇝ ⟨s_{o}, e_{o}, φ_{o}⟩ \end{matrix} nilk.

Each typing rule for commands is an abstraction of the corresponding machine transition rule. The frame moves the stack top type into the environment and the deframe removes the

July 13, 2000  ROPAS-2000-6  7
• ⟨s, e, k, φ⟩ ⊢ C ⇝ ⟨s_{o}, e_{o}, φ_{o}⟩
⟨s, e, ϵ, φ⟩ ⊢ nil ⇝ ⟨s, e, φ⟩ nil  \begin{matrix}⟨s, e′, k, φ⟩ ⊢ C′ ⇝ ⟨s_{o}, e_{o}, φ_{o}⟩ \\ ⟨s, e, (e′, C′).k, φ⟩ ⊢ nil ⇝ ⟨s_{o}, e_{o}, φ_{o}⟩ \end{matrix} nilk
\begin{matrix}⟨s, τ.e, k, φ⟩ ⊢ C ⇝ ⟨s_{o}, e_{o}, φ_{o}⟩ \\ ⟨τ.s, e, k, φ⟩ ⊢ frame.C ⇝ ⟨s_{o}, e_{o}, φ_{o}⟩ \end{matrix} frame
\begin{matrix}⟨s, e, k, φ⟩ ⊢ C ⇝ ⟨s_{o}, e_{o}, φ_{o}⟩ \\ ⟨s, τ.e, k, φ⟩ ⊢ deframe.C ⇝ ⟨s_{o}, e_{o}, φ_{o}⟩ \end{matrix} deframe
\begin{matrix}⟨τ_{n}.s, e, k, φ⟩ ⊢ C ⇝ ⟨s_{o}, e_{o}, φ_{o}⟩ \\ ⟨s, e as τ_{0}. · · · .τ_{n}.e′, k, φ⟩ ⊢ fetch(n).C ⇝ ⟨s_{o}, e_{o}, φ_{o}⟩ \end{matrix} fetch

τ = type of(p) ⟨τ.s, e, k, φ⟩ ⊢ C ⇝ ⟨s_{o}, e_{o}, φ_{o}⟩

⟨s, e, k, φ⟩ ⊢ quote(p).C ⇝ ⟨s_{o}, e_{o}, φ_{o}⟩ quote

\begin{matrix}⟨i.s, e, k, φ⟩ ⊢ C ⇝ ⟨s_{o}, e_{o}, φ_{o}⟩ \\ ⟨i.i.s, e, k, φ⟩ ⊢ add.C ⇝ ⟨s_{o}, e_{o}, φ_{o}⟩ \end{matrix} add
{⟨s, e, ϵ, ϵ⟩ ⊢ C_{i} ⇝ ⟨s_{b}, e_{b}, φ_{b_{i}}⟩ i = 1, 2 \atop ⟨s_{b}, e_{b}, k, φ_{b_{1}} ∪ φ_{b_{2}} ∪ φ⟩ ⊢ C ⇝ ⟨s_{o}, e_{o}, φ_{o}⟩} ; ⟨b.s, e, k, φ⟩ ⊢ cond(C_{1}, C_{2}).C ⇝ ⟨s_{o}, e_{o}, φ_{o}⟩ cond
{⟨ϵ, τ_{1}.e, ϵ, ϵ⟩ ⊢ C_{f} ⇝ ⟨τ_{2}, τ_{1}.e, φ′_{f}⟩ φ′_{f} ⊆ φ_{f}  α_{i}, ρ_{i} ∉ FTV(e) \atop ⟨(∀(α⃗, ρ⃗).τ_{1}→^{φ_{f}}τ_{2}).s, e, k, φ⟩ ⊢ C ⇝ ⟨s_{o}, e_{o}, φ_{o}⟩} ; ⟨s, e, k, φ⟩ ⊢ fn(∀α⃗, ρ⃗.C_{f} : τ_{1}→^{φ_{f}}τ_{2}).C ⇝ ⟨s_{o}, e_{o}, φ_{o}⟩ fn
{⟨ϵ, τ_{1}.τ_{1}→^{φ_{f}}τ_{2}.e, ϵ, ϵ⟩ ⊢ C_{f} ⇝ ⟨τ_{2}, τ_{1}.τ_{1}→^{φ_{f}}τ_{2}.e, φ′_{f}⟩ φ′_{f} ⊆ φ_{f} \atop ⟨(∀(α⃗, ρ⃗).τ_{1}→^{φ_{f}}τ_{2}).s, e, k, φ⟩ ⊢ C ⇝ ⟨s_{o}, e_{o}, φ_{o}⟩  α_{i}, ρ_{i} ∉ FTV(e)} ; ⟨s, e, k, φ⟩ ⊢ rfn(∀α⃗, ρ⃗.C_{f} : τ_{1}→^{φ_{f}}τ_{2}).C ⇝ ⟨s_{o}, e_{o}, φ_{o}⟩ rfn
\begin{matrix}⟨τ_{2}.s, e, k, φ ∪ φ_{f}⟩ ⊢ C ⇝ ⟨s_{o}, e_{o}, φ_{o}⟩ \\ ⟨τ_{1}.τ_{1}→^{φ_{f}}τ_{2}.s, e, k, φ⟩ ⊢ app.C ⇝ ⟨s_{o}, e_{o}, φ_{o}⟩ \end{matrix} app
\begin{matrix}⟨[τ_{i}/α_{i}, r_{i}/ρ_{i}]τ.s, e, k, φ⟩ ⊢ C ⇝ ⟨s_{o}, e_{o}, φ_{o}⟩ \\ ⟨(∀(α⃗, ρ⃗).τ).s, e, k, φ⟩ ⊢ tapp(τ⃗, r⃗).C ⇝ ⟨s_{o}, e_{o}, φ_{o}⟩ \end{matrix} tapp

⟨ref_{ρ}τ.s, e, k, φ ∪ {init(ρ)}⟩ ⊢ C ⇝ ⟨s_{o}, e_{o}, φ_{o}⟩

⟨τ.s, e, k, φ⟩ ⊢ ref(ρ).C ⇝ ⟨s_{o}, e_{o}, φ_{o}⟩ ref

⟨τ.s, e, k, φ ∪ {read(ρ)}⟩ ⊢ C ⇝ ⟨s_{o}, e_{o}, φ_{o}⟩

⟨ref_{ρ}τ.s, e, k, φ⟩ ⊢ get.C ⇝ ⟨s_{o}, e_{o}, φ_{o}⟩ get

⟨unit.s, e, k, φ ∪ {write(ρ)}⟩ ⊢ C ⇝ ⟨s_{o}, e_{o}, φ_{o}⟩

⟨τ.ref_{ρ}τ.s, e, k, φ⟩ ⊢ set.C ⇝ ⟨s_{o}, e_{o}, φ_{o}⟩ set

Figure 4: Typing Rules for etySECK (2) type on the top of the environment:

\begin{matrix}⟨s, τ.e, k, φ⟩ ⊢ C ⇝ ⟨s_{o}, e_{o}, φ_{o}⟩ \\ ⟨τ.s, e, k, φ⟩ ⊢ frame.C ⇝ ⟨s_{o}, e_{o}, φ_{o}⟩ \end{matrix} frame

\begin{matrix}⟨s, e, k, φ⟩ ⊢ C ⇝ ⟨s_{o}, e_{o}, φ_{o}⟩ \\ ⟨s, τ.e, k, φ⟩ ⊢ deframe.C ⇝ ⟨s_{o}, e_{o}, φ_{o}⟩ \end{matrix} deframe.

Typing rules for functions, fn and rfn, check if the annotated types are correct and put polymorphic types on the stack. The following rule describes the typing of non-recursive functions:

{⟨ϵ, τ_{1}.e, ϵ, ϵ⟩ ⊢ C_{f} ⇝ ⟨τ_{2}, τ_{1}.e, φ′_{f}⟩ φ′_{f} ⊆ φ_{f} α_{i}, ρ_{i} ∉ FTV(e) \atop ⟨(∀(α⃗, ρ⃗).τ_{1}→^{φ_{f}}τ_{2}).s, e, k, φ⟩ ⊢ C ⇝ ⟨s_{o}, e_{o}, φ_{o}⟩} ; ⟨s, e, k, φ⟩ ⊢ fn(∀α⃗, ρ⃗.C_{f} : τ_{1}→^{φ_{f}}τ_{2}).C ⇝ ⟨s_{o}, e_{o}, φ_{o}⟩ fn.

Rule app does not distinguish applications of non-recursive functions and recursive functions:

\begin{matrix}⟨τ_{2}.s, e, k, φ ∪ φ_{f}⟩ ⊢ C ⇝ ⟨s_{o}, e_{o}, φ_{o}⟩ \\ ⟨τ_{1}.τ_{1}→^{φ_{f}}τ_{2}.s, e, k, φ⟩ ⊢ app.C ⇝ ⟨s_{o}, e_{o}, φ_{o}⟩ \end{matrix} app.

Rule tapp also does not distinguish them and instantiates polymorphic types to monomorphic ones:

\begin{matrix}⟨[τ_{i}/α_{i}, r_{i}/ρ_{i}]τ.s, e, k, φ⟩ ⊢ C ⇝ ⟨s_{o}, e_{o}, φ_{o}⟩ \\ ⟨(∀(α⃗, ρ⃗).τ).s, e, k, φ⟩ ⊢ tapp(τ⃗, r⃗).C ⇝ ⟨s_{o}, e_{o}, φ_{o}⟩ \end{matrix} tapp.

Rules ref, get, and set introduce corresponding memory effects. For example, rule ref introduces a {init(ρ)} effect:

⟨ref_{ρ}τ.s, e, k, φ ∪ {init(ρ)}⟩ ⊢ C ⇝ ⟨s_{o}, e_{o}, φ_{o}⟩ ⟨τ.s, e, k, φ⟩ ⊢ ref(ρ).C ⇝ ⟨s_{o}, e_{o}, φ_{o}⟩ ref.

2 Soundness

In this section, we prove the soundness of our typing rules by following the standard formalism of Wright and Felleisen [6]. Before presenting the main theorem, we need a few properties of our typing rules.

The first property is that the typing judgement ⟨s, e, k, φ⟩ ⊢ C ⇝ ⟨s_{o}, e_{o}, φ_{o}⟩ can be instantiated to a more concrete judgement by substituting the free variables occurring in the judgement. Lemma 1 formalizes this property.

Lemma 1 (Substitution) If ⟨s, e, k, φ⟩ ⊢ C ⇝ ⟨s_{o}, e_{o}, φ_{o}⟩, then for any substitution S, ⟨Ss, Se, Sk, Sφ⟩ ⊢ SC ⇝ ⟨Ss_{o}, Se_{o}, Sφ_{o}⟩.

Proof We prove by the case analysis of ⟨s, e, k, φ⟩ ⊢ C ⇝ ⟨s_{o}, e_{o}, φ_{o}⟩. Since most cases are obvious, we prove just two nontrivial cases and omit the rest of the proofs.

• case C = fn(∀α⃗, ρ⃗.C_{f} : τ_{1}→^{φ_{f}}τ_{2}).C′

Suppose ⟨s, e, k, φ⟩ ⊢ fn(∀α⃗, ρ⃗.C_{f} : τ_{1}→^{φ_{f}}τ_{2}).C′ ⇝ ⟨s_{o}, e_{o}, φ_{o}⟩. Then by fn,

⟨ϵ, τ_{1}.e, ϵ, ϵ⟩ ⊢ C_{f} ⇝ ⟨τ_{2}, τ_{1}.e, φ′_{f}⟩φ′_{f} ⊆ φ_{f} α_{i}, ρ_{i} ∉ FTV(e)  (1)

⟨(∀(α⃗, ρ⃗).τ_{1}→^{φ_{f}}τ_{2}).s, e, k, φ⟩ ⊢ C′ ⇝ ⟨s_{o}, e_{o}, φ_{o}⟩.  (2)

Let S′ = S[β_{i}/α_{i}, η_{i}/ρ_{i}] for new β_{i}, η_{i}. Since α_{i}, ρ_{i} ∉ FTV(e), S′e = Se. Then by I.H.,

(1) implies

{⟨ϵ, (S′τ_{1}).Se, ϵ, ϵ⟩ ⊢ S′C_{f} ⇝ ⟨S′τ_{2}, (S′τ_{1}).Se, S′φ′_{f}⟩ \atop S′φ′_{f} ⊆ S′φ_{f} β_{i}, η_{i} ∉ FTV(Se).}  (3)

By I.H. and applying S to (2),

⟨S(∀(α⃗, ρ⃗).τ_{1}→^{φ_{f}}τ_{2}).Ss, Se, Sk, Sφ⟩ ⊢ SC′ ⇝ ⟨Ss_{o}, Se_{o}, Sφ_{o}⟩.

Since S(∀(α⃗, ρ⃗).τ_{1}→^{φ_{f}}τ_{2}) ≡ ∀(β⃗, η⃗).S′τ_{1} →^{S′φ_{f}}S′τ_{2},

⟨∀(β⃗, η⃗).S′τ_{1} →^{S′φ_{f}}S′τ_{2}.Ss, Se, Sk, Sφ⟩ ⊢ SC′ ⇝ ⟨Ss_{o}, Se_{o}, Sφ_{o}⟩.  (4)

Now, by applying fn to (3) and (4),

⟨Ss, Se, Sk, Sφ⟩ ⊢ fn(∀β⃗, η⃗.S′C_{f} : S′τ_{1} →^{S′φ_{f}}S′τ_{2}).SC′ ⇝ ⟨Ss_{o}, Se_{o}, Sφ_{o}⟩

and this means

⟨Ss, Se, Sk, Sφ⟩ ⊢ S(fn(∀α⃗, ρ⃗.C_{f} : τ_{1}→^{φ_{f}}τ_{2}).C′) ⇝ ⟨Ss_{o}, Se_{o}, Sφ_{o}⟩.

• case C = tapp(τ⃗, r⃗).C′ Suppose ⟨(∀(α⃗, ρ⃗).τ).s, e, k, φ⟩ ⊢ tapp(τ⃗, r⃗).C′ ⇝ ⟨s_{o}, e_{o}, φ_{o}⟩ then for new β_{i}, η_{i},

⟨(∀(β⃗, η⃗).[β_{i}/α_{i}, η_{i}/ρ_{i}]τ).s, e, k, φ⟩ ⊢ tapp(τ⃗, r⃗).C′ ⇝ ⟨s_{o}, e_{o}, φ_{o}⟩.

Then by tapp,

⟨[τ_{i}/β_{i}, r_{i}/η_{i}]([β_{i}/α_{i}, η_{i}/ρ_{i}]τ).s, e, k, φ⟩ ⊢ C′ ⇝ ⟨s_{o}, e_{o}, φ_{o}⟩.  (5)

By I.H. and applying S to (5),

⟨S([τ_{i}/β_{i}, r_{i}/η_{i}]([β_{i}/α_{i}, η_{i}/ρ_{i}]τ).s), Se, Sk, Sφ⟩ ⊢ SC′ ⇝ ⟨Ss_{o}, Se_{o}, Sφ_{o}⟩.

Since β_{i}, η_{i}’s are new type variables,

S([τ_{i}/β_{i}, r_{i}/η_{i}]([β_{i}/α_{i}, η_{i}/ρ_{i}]τ).s) ; {≡ \atop [(Sτ_{i})/β_{i}, (Sr_{i})/η_{i}](S[β_{i}/α_{i}, η_{i}/ρ_{i}]τ).Ss} .

Thus we have

⟨[(Sτ_{i})/β_{i}, (Sr_{i})/η_{i}](S[β_{i}/α_{i}, η_{i}/ρ_{i}]τ).Ss, Se, Sk, Sφ⟩ ⊢ SC′ ⇝ ⟨Ss_{o}, Se_{o}, Sφ_{o}⟩. (6)

By applying tapp to (6),

⟨(∀(β⃗, η⃗).S[β_{i}/α_{i}, η_{i}/ρ_{i}]τ).Ss, Se, Sk, Sφ⟩ ⊢ tapp(Sτ⃗, Sr⃗).SC′ ⇝ ⟨Ss_{o}, Se_{o}, Sφ_{o}⟩

and this implies

⟨(S(∀(α⃗, ρ⃗).τ).s), Se, Sk, Sφ⟩ ⊢ S(tapp(τ⃗, r⃗).SC′) ⇝ ⟨Ss_{o}, Se_{o}, Sφ_{o}⟩.
□

Lemma 2 states that the quantified type variables or region variables can be instantiated to arbitrary types or regions, respectively.

Lemma 2 (Instantiation) If H ⊧ Λ(α⃗, ρ⃗).fn(τ_{1}→^{φ_{f}}τ_{2}, C_{f}, E_{f}) : ∀(α⃗, ρ⃗).τ_{1}→^{φ_{f}}τ_{2},

then H ⊧ [τ_{i}/α_{i}, r_{i}/ρ_{i}]fn(τ_{1}→^{φ_{f}}τ_{2}, C_{f}, E_{f}) : [τ_{i}/α_{i}, r_{i}/ρ_{i}](τ_{1}→^{φ_{f}}τ_{2}).

Proof By H ⊧ Λ(α⃗, ρ⃗).fn(τ_{1}→^{φ_{f}}τ_{2}, C_{f}, E_{f}) : ∀(α⃗, ρ⃗).τ_{1}→^{φ_{f}}τ_{2}, we have H ⊧ E_{f} : e and H ⊧

fn(τ_{1}→^{φ_{f}}τ_{2}, C_{f}, E_{f}) : τ_{1}→^{φ_{f}}τ_{2} α_{i}, ρ_{i} ∉ FTV(e); that is,

⟨ϵ, τ_{1}.e, ϵ, ϵ⟩ ⊢ C_{f} ⇝ ⟨τ_{2}, τ_{1}.e, φ′_{f}⟩ φ′_{f} ⊆ φ_{f}.  (7)

Let S = [τ_{i}/α_{i}, r_{i}/ρ_{i}]. Since α_{i}, ρ_{i} ∉ FTV(e), we have Se = e and H ⊧ SE_{f} : e. By (7) and Lemma 1, ⟨ϵ, S(τ_{1}.e), ϵ, ϵ⟩ ⊢ SC_{f} ⇝ ⟨Sτ_{2}, S(τ_{1}.e), Sφ′_{f}⟩ Sφ′_{f} ⊆ Sφ_{f}.

Since H ⊧ fn(S(τ_{1}→^{φ_{f}}τ_{2}), SC_{f}, SE_{f}) : S(τ_{1}→^{φ_{f}}τ_{2}), H ⊧ S fn(τ_{1}→^{φ_{f}}τ_{2}, C_{f}, E_{f}) : S(τ_{1}→^{φ_{f}}τ_{2}). □

Lemma 3 states that any extension of the stack bottom does not affect the typability of a given machine configuration and Lemma 4 states the monotonicity of effects. Since the proofs of Lemma 3 and 4 are trivial we omit them.

Lemma 3 (Stack Bottom Extensibility) If ⟨s, e, k, φ⟩ ⊢ C ⇝ ⟨s_{o}, e_{o}, φ_{o}⟩, then for any s′, ⟨s.s′, e, k, φ⟩ ⊢ C ⇝ ⟨s_{o}.s′, e_{o}, φ_{o}⟩.

Lemma 4 (Effect monotonicity)

(1) If ⟨s, e, k, φ⟩ ⊢ C ⇝ ⟨s_{o}, e_{o}, φ_{o}⟩, then for any φ′, ⟨s, e, k, φ ∪ φ′⟩ ⊢ C ⇝ ⟨s_{o}, e_{o}, φ_{o} ∪ φ′⟩.

(2) If ⟨s, e, k, φ⟩ ⊢ C ⇝ ⟨s_{o}, e_{o}, φ_{o}⟩ and φ′ ⊆ φ, then ⟨s, e, k, φ′⟩ ⊢ C ⇝ ⟨s_{o}, e_{o}, φ′_{o}⟩ and φ′_{o} ⊆ φ_{o}.

Lemma 5 describes the typing of commands under the configuration with a non-nil continuation: after typing the current code, our typing mechanism gets a pair of an environment and commands from the continuation and keeps typing the new commands under the new environment.

Lemma 5 (Continuation) If ⟨s_{1}, e_{1}, ϵ, φ_{1}⟩ ⊢ C_{1} ⇝ ⟨s_{2}, e′, φ_{2}⟩ and ⟨s_{2}.s_{3}, e_{2}, k_{2}, φ_{2} ∪ φ′⟩ ⊢ C_{2} ⇝ ⟨s, e, φ⟩, then ⟨s_{1}.s_{3}, e_{1}, (e_{2}, C_{2}).k_{2}, φ_{1} ∪ φ′⟩ ⊢ C_{1} ⇝ ⟨s, e, φ⟩.

Proof We prove by induction on the length of C_{1}.

• case C_{1} = nil

By assumption, s_{2} = s_{1}, e′ = e_{1}, φ_{2} = φ_{1}, and ⟨s_{2}.s_{3}, e_{2}, k_{2}, φ_{2} ∪ φ′⟩ ⊢ C_{2} ⇝ ⟨s, e, φ⟩. Then by nilk,

⟨s_{1}.s_{3}, e_{1}, (e_{2}, C_{2}).k_{2}, φ′ ∪ φ_{1}⟩ ⊢ nil ⇝ ⟨s, e, φ⟩.

• case C_{1} = frame.C′

By assumption, s_{1} = τ.s′_{1} for some s′_{1} such that

⟨τ.s′_{1}, e_{1}, ϵ, φ_{1}⟩ ⊢ frame.C′ ⇝ ⟨s_{2}, e′, φ_{2}⟩  (8)
⟨s_{2}.s_{3}, e_{2}, k_{2}, φ_{2} ∪ φ′⟩ ⊢ C_{2} ⇝ ⟨s, e, φ⟩.  (9)

Then by (8) and frame,

⟨s′_{1}, τ.e_{1}, ϵ, φ_{1}⟩ ⊢ C′ ⇝ ⟨s_{2}, e′, φ_{2}⟩  (10)

and by (10), (9), and I.H.,

⟨s′_{1}.s_{3}, τ.e_{1}, (e_{2}, C_{2}).k_{2}, φ_{1} ∪ φ′⟩ ⊢ C′ ⇝ ⟨s, e, φ⟩.  (11)

Thus by (11) and frame,

⟨τ.s′_{1}.s_{3}, e_{1}, (e_{2}, C_{2}).k_{2}, φ_{1} ∪ φ′⟩ ⊢ frame.C′ ⇝ ⟨s, e, φ⟩.

• case C_{1} = deframe.C′ By assumption, e_{1} = τ.e′_{1} such that

⟨s_{1}, τ.e′_{1}, ϵ, φ_{1}⟩ ⊢ deframe.C′ ⇝ ⟨s_{2}, e′, φ_{2}⟩  (12)
⟨s_{2}.s_{3}, e_{2}, k_{2}, φ_{2} ∪ φ′⟩ ⊢ C_{2} ⇝ ⟨s, e, φ⟩.  (13)

Then by (12) and deframe,

⟨s_{1}, e′_{1}, ϵ, φ_{1}⟩ ⊢ C′ ⇝ ⟨s_{2}, e′, φ_{2}⟩  (14)

and by (13), (14), and I.H.,

⟨s_{1}.s_{3}, e′_{1}, (e_{2}, C_{2}).k_{2}, φ′ ∪ φ_{1}⟩ ⊢ C′ ⇝ ⟨s, e, φ⟩.  (15)

Thus by (15) and deframe,

⟨s_{1}.s_{3}, τ.e′_{1}, (e_{2}, C_{2}).k_{2}, φ′ ∪ φ_{1}⟩ ⊢ deframe.C′ ⇝ ⟨s, e, φ⟩.

• case C_{1} = fetch(n).C′ By assumption, e_{1} = τ_{0}. · · · .τ_{n}.e′_{1} such that

⟨s_{1}, τ_{0}. · · · .τ_{n}.e′_{1}, ϵ, φ_{1}⟩ ⊢ fetch(n).C′ ⇝ ⟨s_{2}, e′, φ_{2}⟩  (16)
⟨s_{2}.s_{3}, e_{2}, k_{2}, φ_{2} ∪ φ′⟩ ⊢ C_{2} ⇝ ⟨s, e, φ⟩.  (17)

Then by (16) and fetch,

⟨τ_{n}.s_{1}, τ_{0}. · · · .τ_{n}.e′_{1}, ϵ, φ_{1}⟩ ⊢ C′ ⇝ ⟨s_{2}, e′, φ_{2}⟩  (18)

and by (18), (17), and I.H.,

⟨τ_{n}.s_{1}.s_{3}, τ_{0}. · · · .τ_{n}.e′_{1}, (e_{2}, C_{2}).k_{2}, φ′ ∪ φ_{1}⟩ ⊢ C′ ⇝ ⟨s, e, φ⟩.  (19)

Thus by (19) and fetch,

⟨τ_{n}.s_{1}.s_{3}, τ_{0}. · · · .τ_{n}.e′_{1}, (e_{2}, C_{2}).k_{2}, φ′ ∪ φ_{1}⟩ ⊢ fetch(n).C′ ⇝ ⟨s, e, φ⟩.

• case C_{1} = quote(p).C′ Let τ = type of(p) then by assumption,

⟨s_{1}, e_{1}, ϵ, φ_{1}⟩ ⊢ quote(p).C′ ⇝ ⟨s_{2}, e′, φ_{2}⟩  (20)

⟨s_{2}.s_{3}, e_{2}, k_{2}, φ_{2} ∪ φ′⟩ ⊢ C_{2} ⇝ ⟨s, e, φ⟩.  (21)

Then by (20) and quote,

⟨τ.s_{1}, e_{1}, ϵ, φ_{1}⟩ ⊢ C′ ⇝ ⟨s_{2}, e′, φ_{2}⟩  (22)

and by (22), (21), and I.H,

⟨τ.s_{1}.s_{3}, e_{1}, (e_{2}, C_{2}).k_{2}, φ′ ∪ φ_{1}⟩ ⊢ C′ ⇝ ⟨s, e, φ⟩.  (23)

Thus by (23) and quote, ⟨s_{1}.s_{3}, e_{1}, (e_{2}, C_{2}).k_{2}, φ′ ∪ φ_{1}⟩ ⊢ quote(p).C′ ⇝ ⟨s, e, φ⟩.

• case C_{1} = add.C′

By assumption, s_{1} = i.i.s′_{1} such that

⟨i.i.s′_{1}, e_{1}, ϵ, φ_{1}⟩ ⊢ add.C′ ⇝ ⟨s_{2}, e′, φ_{2}⟩  (24)
⟨s_{2}.s_{3}, e_{2}, k_{2}, φ_{2} ∪ φ′⟩ ⊢ C_{2} ⇝ ⟨s, e, φ⟩.  (25)

Then by (24) and add,

⟨i.s′_{1}, e_{1}, ϵ, φ_{1}⟩ ⊢ C′ ⇝ ⟨s_{2}, e′, φ_{2}⟩  (26)

and by (26), (25), and I.H.,

⟨i.s′_{1}.s_{3}, e_{1}, (e_{2}, C_{2}).k_{2}, φ′ ∪ φ_{1}⟩ ⊢ C′ ⇝ ⟨s, e, φ⟩.  (27)

Thus by (27) and add, ⟨i.i.s′_{1}.s_{3}, e_{1}, (e_{2}, C_{2}).k_{2}, φ′ ∪ φ_{1}⟩ ⊢ add.C′ ⇝ ⟨s, e, φ⟩.

• case C_{1} = cond(C_{t}, C_{f}).C′

By assumption, s_{1} = b.s′_{1} such that

⟨b.s′_{1}, e_{1}, ϵ, φ_{1}⟩ ⊢ cond(C_{t}, C_{f}).C′ ⇝ ⟨s_{2}, e′, φ_{2}⟩  (28)
⟨s_{2}.s_{3}, e_{2}, k_{2}, φ_{2} ∪ φ′⟩ ⊢ C_{2} ⇝ ⟨s, e, φ⟩.  (29)

Then by (28) and cond,

⟨s′_{1}, e_{1}, ϵ, ϵ⟩ ⊢ C_{t} ⇝ ⟨s_{b}, e_{b}, φ_{b_{1}}⟩  ⟨s′_{1}, e_{1}, ϵ, ϵ⟩ ⊢ C_{f} ⇝ ⟨s_{b}, e_{b}, φ_{b_{2}}⟩  (30)
⟨s_{b}, e_{b}, ϵ, φ_{b_{1}} ∪ φ_{b_{2}} ∪ φ_{1}⟩ ⊢ C′ ⇝ ⟨s_{2}, e′, φ_{2}⟩.  (31)

and by applying Lemma 3 to (30),

⟨s′_{1}.s_{3}, e_{1}, ϵ, ϵ⟩ ⊢ C_{t} ⇝ ⟨s_{b}.s_{3}, e_{b}, φ_{b_{1}}⟩  ⟨s′_{1}.s_{3}, e_{1}, ϵ, ϵ⟩ ⊢ C_{f} ⇝ ⟨s_{b}.s_{3}, e_{b}, φ_{b_{2}}⟩. (32)

By applying I.H. to (31) and (29),

⟨s_{b}.s_{3}, e_{b}, (e_{2}, C_{2}).k_{2}, φ_{b_{1}} ∪ φ_{b_{2}} ∪ φ_{1} ∪ φ′⟩ ⊢ C′ ⇝ ⟨s, e, φ⟩  (33)

and by (32), (33), and cond, ⟨b.s′_{1}.s_{3}, e_{1}, (e_{2}, C_{2}).k_{2}, φ_{1} ∪ φ′⟩ ⊢ cond(C_{t}, C_{f}).C′ ⇝ ⟨s, e, φ⟩.

• case C_{1} = fn(∀α⃗, ρ⃗.C_{f} : τ_{1}→^{φ_{f}}τ_{2}).C′

By assumption,

⟨s_{1}, e_{1}, ϵ, φ_{1}⟩ ⊢ fn(∀α⃗, ρ⃗.C_{f} : τ_{1}→^{φ_{f}}τ_{2}).C′ ⇝ ⟨s_{2}, e′, φ_{2}⟩  (34)
⟨s_{2}.s_{3}, e_{2}, k_{2}, φ_{2} ∪ φ′⟩ ⊢ C_{2} ⇝ ⟨s, e, φ⟩.  (35)

Then by (34) and fn,

⟨ϵ, τ_{1}.e_{1}, ϵ, ϵ⟩ ⊢ C_{f} ⇝ ⟨τ_{2}, τ_{1}.e_{1}, φ′_{f}⟩ φ′_{f} ⊑ φ_{f} α_{i}, ρ_{i} ∉ FTV(e_{1})  (36)
⟨(∀(α⃗, ρ⃗).τ_{1}→^{φ_{f}}τ_{2}).s_{1}, e_{1}, ϵ, φ_{1}⟩ ⊢ C′ ⇝ ⟨s_{2}, e′, φ_{2}⟩  (37)

and by (37), (35), and I.H.,

⟨(∀(α⃗, ρ⃗).τ_{1}→^{φ_{f}}τ_{2}).s_{1}.s_{3}, e_{1}, (e_{2}, C_{2}).k_{2}, φ′ ∪ φ_{1}⟩ ⊢ C′ ⇝ ⟨s, e, φ⟩.  (38)

Thus by (38), (36), and fn,

⟨s_{1}.s_{3}, e_{1}, (e_{2}, C_{2}).k_{2}, φ′ ∪ φ_{1}⟩ ⊢ fn(∀α⃗, ρ⃗.C_{f} : τ_{1}→^{φ_{f}}τ_{2}).C′ ⇝ ⟨s, e, φ⟩.

• case C_{1} = rfn(∀α⃗, ρ⃗.C_{f} : τ_{1}→^{φ_{f}}τ_{2}).C′

The proof of this case is same for the case C_{1} = fn(∀α⃗, ρ⃗.C_{f} : τ_{1}→^{φ_{f}}τ_{2}).C′.

• case C_{1} = app.C′ By assumption, s_{1} = τ_{1}.τ_{1}→^{φ_{f}}τ_{2}.s′_{1} such that

⟨τ_{1}.τ_{1}→^{φ_{f}}τ_{2}.s′_{1}, e_{1}, ϵ, φ_{1}⟩ ⊢ app.C′ ⇝ ⟨s_{2}, e′, φ_{2}⟩  (39)
⟨s_{2}.s_{3}, e_{2}, k_{2}, φ_{2} ∪ φ′⟩ ⊢ C_{2} ⇝ ⟨s, e, φ⟩.  (40)

Then by (39) and app,

⟨τ_{2}.s′_{1}, e_{1}, ϵ, φ_{1} ∪ φ_{f}⟩ ⊢ C′ ⇝ ⟨s_{2}, e′, φ_{2}⟩  (41)

and by (40), (41), and I.H.,

⟨τ_{2}.s′_{1}.s_{3}, e_{1}, (e_{2}, C_{2}).k_{2}, φ′ ∪ φ_{1} ∪ φ_{f}⟩ ⊢ C′ ⇝ ⟨s, e, φ⟩.  (42)

Thus by (42) and app,

⟨τ_{1}.τ_{1}→^{φ_{f}}τ_{2}.s′_{1}.s_{3}, e_{1}, (e_{2}, C_{2}).k_{2}, φ′ ∪ φ_{1}⟩ ⊢ app.C′ ⇝ ⟨s, e, φ⟩.

• case C_{1} = tapp(τ⃗, r⃗).C′ By assumption, s_{1} = (∀(α⃗, ρ⃗).τ).s′_{1} such that

⟨(∀(α⃗, ρ⃗).τ).s′_{1}, e_{1}, ϵ, φ_{1}⟩ ⊢ tapp(τ⃗, r⃗).C′ ⇝ ⟨s_{2}, e′, φ_{2}⟩  (43)

⟨s_{2}.s_{3}, e_{2}, k_{2}, φ_{2} ∪ φ′⟩ ⊢ C_{2} ⇝ ⟨s, e, φ⟩.  (44)

Let S = [τ_{i}/α_{i}, r_{i}/ρ_{i}] then by tapp,

⟨Sτ.s′_{1}, e_{1}, ϵ, φ_{1}⟩ ⊢ C′ ⇝ ⟨s_{2}, e′, φ_{2}⟩  (45)

and by (44), (45), and I.H.,

⟨Sτ.s′_{1}.s_{3}, e_{1}, (e_{2}, C_{2}).k_{2}, φ′ ∪ φ_{1}⟩ ⊢ C′ ⇝ ⟨s, e, φ⟩.  (46)

Thus by (46) and tapp,

⟨(∀(α⃗, ρ⃗).τ).s′_{1}.s_{3}, e_{1}, (e_{2}, C_{2}).k_{2}, φ′ ∪ φ_{1}⟩ ⊢ tapp(τ⃗, r⃗).C′ ⇝ ⟨s, e, φ⟩.

• case C_{1} = ref(ρ).C′ By assumption, s_{1} = τ.s′_{1} such that

⟨τ.s′_{1}, e_{1}, ϵ, φ_{1}⟩ ⊢ ref(ρ).C′ ⇝ ⟨s_{2}, e′, φ_{2}⟩  (47)
⟨s_{2}.s_{3}, e_{2}, k_{2}, φ_{2} ∪ φ′⟩ ⊢ C_{2} ⇝ ⟨s, e, φ⟩.  (48)

Then by (47) and ref,

⟨ref_{ρ}τ.s′_{1}, e_{1}, ϵ, φ_{1} ∪ {init(ρ)}⟩ ⊢ C′ ⇝ ⟨s_{2}, e′, φ_{2}⟩  (49)

and by (48), (49), and I.H.,

⟨ref_{ρ}τ.s′_{1}.s_{3}, e_{1}, (e_{2}, C_{2}).k_{2}, φ′ ∪ φ_{1} ∪ {init(ρ)}⟩ ⊢ C′ ⇝ ⟨s, e, φ⟩.  (50)

Thus by (50) and ref,

⟨τ.s′_{1}.s_{3}, e_{1}, (e_{2}, C_{2}).k_{2}, φ′ ∪ φ_{1}⟩ ⊢ ref(ρ).C′ ⇝ ⟨s, e, φ⟩.

• case C_{1} = get.C′ By assumption, s_{1} = ref_{ρ}τ.s′_{1} such that

⟨ref_{ρ}τ.s′_{1}, e_{1}, ϵ, φ_{1}⟩ ⊢ get.C′ ⇝ ⟨s_{2}, e′, φ_{2}⟩  (51)
⟨s_{2}.s_{3}, e_{2}, k_{2}, φ_{2} ∪ φ′⟩ ⊢ C_{2} ⇝ ⟨s, e, φ⟩.  (52)

Then by (51) and get,

⟨τ.s′_{1}, e_{1}, ϵ, φ_{1} ∪ {read(ρ)}⟩ ⊢ C′ ⇝ ⟨s_{2}, e′, φ_{2}⟩  (53)

and by (52), (53), and I.H.,

⟨τ.s′_{1}.s_{3}, e_{1}, (e_{2}, C_{2}).k_{2}, φ′ ∪ φ_{1} ∪ {read(ρ)}⟩ ⊢ C′ ⇝ ⟨s, e, φ⟩.  (54)

Thus by (54) and get,

⟨ref_{ρ}τ.s′_{1}.s_{3}, e_{1}, (e_{2}, C_{2}).k_{2}, φ′ ∪ φ_{1}⟩ ⊢ get.C′ ⇝ ⟨s, e, φ⟩.

• case C_{1} = set.C′

By assumption, s_{1} = τ.ref_{ρ}τ.s′_{1} such that

⟨τ.ref_{ρ}τ.s′_{1}, e_{1}, ϵ, φ_{1}⟩ ⊢ set.C′ ⇝ ⟨s_{2}, e′, φ_{2}⟩  (55)

⟨s_{2}.s_{3}, e_{2}, k_{2}, φ_{2} ∪ φ′⟩ ⊢ C_{2} ⇝ ⟨s, e, φ⟩.  (56)

Then by (55) and set,

⟨unit.s′_{1}, e_{1}, ϵ, φ_{1} ∪ {write(ρ)}⟩ ⊢ C′ ⇝ ⟨s_{2}, e′, φ_{2}⟩  (57)

and by (56), (57), and I.H.,

⟨unit.s′_{1}.s_{3}, e_{1}, (e_{2}, C_{2}).k_{2}, φ′ ∪ φ_{1} ∪ {write(ρ)}⟩ ⊢ C′ ⇝ ⟨s, e, φ⟩.  (58)

Thus by (58) and set,

⟨τ.ref_{ρ}τ.s′_{1}.s_{3}, e_{1}, (e_{2}, C_{2}).k_{2}, φ′ ∪ φ_{1}⟩ ⊢ set.C′ ⇝ ⟨s, e, φ⟩.
□

Theorem 6 states that if a machine configuration has a type, its next configuration, if any, will have the same type. Since effects annotated on types may not occur, effects can be reduced after one step transition.

Lemma 6 (Subject Reduction) If (S, H, E, C, K, φ) ⇝ (s_{o}, e_{o}, φ_{o}) and (S, H, E, C, K, φ)⇒M, then M ⇝ (s_{o}, e_{o}, φ′_{o}) and φ′_{o} ⊆ φ_{o}.

Proof We prove by the case analysis of the transition relation(⇒).

• case (S, H, E, nil, (E′, C).K, φ)⇒(S, H, E′, C, K, φ)

By assumption, there exist s, e, k, and e′ such that H ⊧ S : s, H ⊧ E : e, H ⊧ K : k, H ⊧ E′ : e′, H ⊧ (E′, C).K : (e′, C).k, and

⟨s, e, (e′, C).k, φ⟩ ⊢ nil ⇝ ⟨s_{o}, e_{o}, φ_{o}⟩.

Then by nilk, ⟨s, e′, k, φ⟩ ⊢ C ⇝ ⟨s_{o}, e_{o}, φ_{o}⟩ and (S, H, E′, C, K, φ) ⇝ (s_{o}, e_{o}, φ_{o}).

• case (v.S, H, E, frame.C, K, φ)⇒(S, H, v.E, C, K, φ)

Since by assumption (v.S, H, E, frame.C, K, φ) ⇝ (s_{o}, e_{o}, φ_{o}), there exist τ, s, e and k such that H ⊧ v : τ, H ⊧ S : s, H ⊧ E : e, H ⊧ K : k and

⟨τ.s, e, k, φ⟩ ⊢ frame.C ⇝ ⟨s_{o}, e_{o}, φ_{o}⟩.

By frame, ⟨s, τ.e, k, φ⟩ ⊢ C ⇝ ⟨s_{o}, e_{o}, φ_{o}⟩. Since H ⊧ v.E : τ.e,

(S, H, v.E, C, K, φ) ⇝ (s_{o}, e_{o}, φ_{o}) and φ_{o} ⊆ φ_{o}.

• case (S, H, v.E, deframe.C, K, φ)⇒(S, H, E, C, K, φ)

There exist s, e, τ, and k such that H ⊧ S : s, H ⊧ E : e, H ⊧ v : τ, H ⊧ K : k, and ⟨s, τ.e, k, φ⟩ ⊢ deframe.C ⇝ ⟨s_{o}, e_{o}, φ_{o}⟩. Then by deframe, ⟨s, e, k, φ⟩ ⊢ C ⇝ ⟨s_{o}, e_{o}, φ_{o}⟩, and (S, H, E, C, K, φ) ⇝ (s_{o}, e_{o}, φ_{o}).

• case (S, H, v_{0}. · · · .v_{n}.E, fetch(n).C, K, φ)⇒(v_{n}.S, H, v_{0}. · · · .v_{n}.E, C, K, φ) There exist s, e, τ_{i} (i = 0, ⋯, n), and k such that H ⊧ S : s, H ⊧ E : e, H ⊧ v_{i} : τ_{i}, H ⊧ K : k and ⟨s, τ_{0}. · · · .τ_{n}.e, k, φ⟩ ⊢ fetch(n).C ⇝ ⟨s_{o}, e_{o}, φ_{o}⟩. Then by fetch, ⟨τ_{n}.s, τ_{0}. · · · .τ_{n}.e, k, φ⟩ ⊢ C ⇝ ⟨s_{o}, e_{o}, φ_{o}⟩ and

(v_{n}.S, H, E, C, K, φ) ⇝ (s_{o}, v_{o}, φ_{o}).

• case (S, H, E, quote(p).C, K, φ)⇒(p.S, H, E, C, K, φ)

There exist s, e, and k such that H ⊧ S : s, H ⊧ E : e, H ⊧ K : k and

⟨s, e, k, φ⟩ ⊢ quote(p).C ⇝ ⟨s_{o}, e_{o}, φ_{o}⟩.

Let τ = type of(p) then by quote, ⟨τ.s, e, k, φ⟩ ⊢ C ⇝ ⟨s_{o}, e_{o}, φ_{o}⟩ and

(p.S, H, E, C, K, φ) ⇝ (s_{o}, e_{o}, φ_{o}).

• case (i_{2}.i_{1}.S, H, E, add.C, K, φ)⇒(i_{1} + i_{2}.S, H, E, C, K, φ)

There exist s, e, and k such that H ⊧ S : s, H ⊧ i_{j} : i (j = 1, 2), H ⊧ E : e, H ⊧ K : k and ⟨i.i.s, e, k, φ⟩ ⊢ add.C ⇝ ⟨s_{o}, e_{o}, φ_{o}⟩. Then by add, ⟨i.s, e, k, φ⟩ ⊢ C ⇝ ⟨s_{o}, e_{o}, φ_{o}⟩ and H ⊧ i_{i} + i_{2} : i. Thus,

(i_{i} + i_{2}.S, H, E, C, K, φ) ⇝ (s_{o}, e_{o}, φ_{o}).

• case (true.S, H, E, cond(C_{1}, C_{2}).C, K, φ)⇒(S, H, E, C_{1}.C, K, φ) By the same reasoning, there exist s, e, and k such that H ⊧ S : s, H ⊧ E : e, H ⊧ K : k and ⟨b.s, e, k, φ⟩ ⊢ cond(C_{1}, C_{2}).C ⇝ ⟨s_{o}, e_{o}, φ_{o}⟩. Then by cond,

⟨s, e, ϵ, ϵ⟩ ⊢ C_{1} ⇝ ⟨s_{b}, e_{b}, φ_{b_{1}}⟩  ⟨s, e, ϵ, ϵ⟩ ⊢ C_{2} ⇝ ⟨s_{b}, e_{b}, φ_{b_{2}}⟩  (59)
⟨s_{b}, e_{b}, k, φ_{b_{1}} ∪ φ_{b_{2}} ∪ φ⟩ ⊢ C ⇝ ⟨s_{o}, e_{o}, φ_{o}⟩.  (60)

By applying Lemma 4 to (60),

⟨s_{b}, e_{b}, k, φ_{b_{1}} ∪ φ⟩ ⊢ C ⇝ ⟨s_{o}, e_{o}, φ′_{o}⟩ φ′_{o} ⊆ φ_{o}  (61)

for some φ′_{o} and by applying Lemma 4 to (59),

⟨s, e, ϵ, φ⟩ ⊢ C_{1} ⇝ ⟨s_{b}, e_{b}, φ_{b_{1}} ∪ φ⟩.  (62)

Thus by (62) and (61),

⟨s, e, k, φ⟩ ⊢ C_{1}.C ⇝ ⟨s_{o}, e_{o}, φ′_{o}⟩ and φ′_{o} ⊆ φ_{o}.

• case (false.S, H, E, cond(C_{1}, C_{2}).C, K, φ)⇒(S, H, E, C_{1}.C, K, φ) The proof of this case is same for the case

(true.S, H, E, cond(C_{1}, C_{2}).C, K, φ)⇒(S, H, E, C_{1}.C, K, φ).

• case (S, H, E, fn(∀α⃗, ρ⃗.C_{f} : τ_{1}→^{φ_{f}}τ_{2}).C, K, φ)⇒ (Λ(α⃗, ρ⃗).fn(τ_{1}→^{φ_{f}}τ_{2}, C_{f}, E).S, H, E, C, K, φ)

There exist s, e, and k such that H ⊧ S : s, H ⊧ E : e, H ⊧ K : k and

⟨s, e, k, φ⟩ ⊢ fn(∀α⃗, ρ⃗.C_{f} : τ_{1}→^{φ_{f}}τ_{2}).C ⇝ ⟨s_{o}, e_{o}, φ_{o}⟩.

Then by fn,

⟨ϵ, τ_{1}.e, ϵ, ϵ⟩ ⊢ C_{f} ⇝ ⟨τ_{2}, τ_{1}.e, φ′_{f}⟩ φ′_{f} ⊑ φ_{f} α_{i}, ρ_{i} ∉ FTV(e)  (63)
⟨(∀(α⃗, ρ⃗).τ_{1}→^{φ_{f}}τ_{2}).s, e, k, φ⟩ ⊢ C ⇝ ⟨s_{o}, e_{o}, φ_{o}⟩.  (64)

By (63) and H ⊧ E : e,

H ⊧ fn(τ_{1}→^{φ_{f}}τ_{2}, C_{f}, E) : τ_{1}→^{φ_{f}}τ_{2}  (65)

and by (65), (63), and H ⊧ E : e,

H ⊧ Λ(α⃗, ρ⃗).fn(τ_{1}→^{φ_{f}}τ_{2}, C_{f}, E) : ∀(α⃗, ρ⃗).τ_{1}→^{φ_{f}}τ_{2}.  (66)

Thus by (64) and (66),

(Λ(α⃗, ρ⃗).fn(τ_{1}→^{φ_{f}}τ_{2}, C_{f}, E).S, H, E, C, K, φ) ⇝ (s_{o}, e_{o}, φ_{o}).

• case (S, H, E, rfn(∀α⃗, ρ⃗.C_{f} : τ_{1}→^{φ_{f}}τ_{2}).C, K, φ)⇒ (Λ(α⃗, ρ⃗).rfn(τ_{1}→^{φ_{f}}τ_{2}, C_{f}, E).S, H, E, C, K, φ)

The proof of this case is same for the case whose code is fn(∀α⃗, ρ⃗.C_{f} : τ_{1}→^{φ_{f}}τ_{2}).C.

• case (v.fn(τ_{1}→^{φ_{f}}τ_{2}, C_{f}, E_{f}).S, H, E, app.C, K, φ)⇒(S, H, v.E_{f}, C_{f}, (E, C).K, φ)

There exist s, e, and k such that H ⊧ v : τ_{1}, H ⊧ fn(τ_{1}→^{φ_{f}}τ_{2}, C_{f}, E_{f}) : τ_{1}→^{φ_{f}}τ_{2}, H ⊧ S : s,

H ⊧ E : e, H ⊧ K : k and

⟨τ_{1}.τ_{1}→^{φ_{f}}τ_{2}.s, e, k, φ⟩ ⊢ app.C ⇝ ⟨s_{o}, e_{o}, φ_{o}⟩.  (67)

Since H ⊧ fn(τ_{1}→^{φ_{f}}τ_{2}, C_{f}, E_{f}) : τ_{1}→^{φ_{f}}τ_{2}, H ⊧ E_{f} : e_{f} and

⟨ϵ, τ_{1}.e_{f}, ϵ, ϵ⟩ ⊢ C_{f} ⇝ ⟨τ_{2}, τ_{1}.e_{f}, φ′_{f}⟩ φ′_{f} ⊆ φ_{f}.  (68)

By (67) and app,

⟨τ_{2}.s, e, k, φ ∪ φ_{f}⟩ ⊢ C ⇝ ⟨s_{o}, e_{o}, φ_{o}⟩  (69)

and by (69) and Lemma 4,

⟨τ_{2}.s, e, k, φ ∪ φ′_{f}⟩ ⊢ C ⇝ ⟨s_{o}, e_{o}, φ′_{o}⟩ φ′_{o} ⊆ φ_{o}  (70)

for some φ′_{o}. By (68), (70), and Lemma 5,

⟨s, τ_{1}.e_{f}, (e, C).k, φ⟩ ⊢ C_{f} ⇝ ⟨s_{o}, e_{o}, φ′_{o}⟩

which means

(S, H, v.E_{f}, C_{f}, (E, C).K, φ) ⇝ (s_{o}, e_{o}, φ′_{o}) φ′_{o} ⊆ φ_{o}.

• case (v.rfn(τ_{1}→^{φ_{f}}τ_{2}, C_{f}, E_{f}).S, H, E, app.C, K, φ)⇒

(S, H, v.rfn(τ_{1}→^{φ_{f}}τ_{2}, C_{f}, E_{f}).E_{f}, C_{f}, (E, C).K, φ)

The proof of this case is same for the case

(v.rfn(τ_{1}→^{φ_{f}}τ_{2}, C_{f}, E_{f}).S, H, E, app.C, K, φ)⇒(S, H, v.E_{f}, C_{f}, (E, C).K, φ).

• case (Λ(α⃗, ρ⃗).fn(τ_{1}→^{φ_{f}}τ_{2}, C_{f}, E_{f}).S, H, E, tapp(τ⃗, r⃗).C, K, φ)⇒

([τ_{i}/α_{i}, r_{i}/ρ_{i}]fn(τ_{1}→^{φ_{f}}τ_{2}, C_{f}, E_{f}).S, H, E, C, K, φ)

There exist s, e, and k such that

H ⊧ Λ(α⃗, ρ⃗).fn(τ_{1}→^{φ_{f}}τ_{2}, C_{f}, E_{f}) : ∀(α⃗, ρ⃗).τ_{1}→^{φ_{f}}τ_{2},  (71)

H ⊧ S : s, H ⊧ E : e, H ⊧ K : k and

⟨∀(α⃗, ρ⃗).τ_{1}→^{φ_{f}}τ_{2}.s, e, k, φ⟩ ⊢ tapp(τ⃗, r⃗).C ⇝ ⟨s_{o}, e_{o}, φ_{o}⟩.

Then by tapp,

⟨[τ_{i}/α_{i}, r_{i}/ρ_{i}](τ_{1}→^{φ_{f}}τ_{2}).s, e, k, φ⟩ ⊢ C ⇝ ⟨s_{o}, e_{o}, φ_{o}⟩.  (72)

Let S ≡ [τ_{i}/α_{i}, r_{i}/ρ_{i}] then by (71) and Lemma 2,

H ⊧ S fn((τ_{1}→^{φ_{f}}τ_{2}), C_{f}, E_{f}) : S(τ_{1}→^{φ_{f}}τ_{2}).  (73)

Thus by (72) and (73),

(S fn((τ_{1}→^{φ_{f}}τ_{2}), C_{f}, E_{f}).S, H, E, C, K, φ) ⇝ (s_{o}, e_{o}, φ_{o}).

• case (Λ(α⃗, ρ⃗).rfn(τ_{1}→^{φ_{f}}τ_{2}, C_{f}, E_{f}).S, H, E, tapp(τ⃗, r⃗).C, K, φ)⇒

([τ_{i}/α_{i}, r_{i}/ρ_{i}]rfn(τ_{1}→^{φ_{f}}τ_{2}, C_{f}, E_{f}).S, H, E, C, K, φ)

The proof of this case is same for the case

(Λ(α⃗, ρ⃗).fn(τ_{1}→^{φ_{f}}τ_{2}, C_{f}, E_{f}).S, H, E, tapp(τ⃗, r⃗).C, K, φ)⇒

([τ_{i}/α_{i}, r_{i}/ρ_{i}]fn(τ_{1}→^{φ_{f}}τ_{2}, C_{f}, E_{f}).S, H, E, C, K, φ).

• case (v.S, H, E, ref(ρ).C, K, φ)⇒(l_{ρ}.S, H[l_{ρ} → v], E, C, K, φ ∪ {init(ρ)}) l_{ρ} ∉ Dom(H) There exist s, e, and k such that H ⊧ v : τ, H ⊧ S : s, H ⊧ E : e, H ⊧ K : k and ⟨τ.s, e, k, φ⟩ ⊢ ref(ρ).C ⇝ ⟨s_{o}, e_{o}, φ_{o}⟩. Then by ref,

⟨ref_{ρ}τ.s, e, k, φ ∪ {init(ρ)}⟩ ⊢ C ⇝ ⟨s_{o}, e_{o}, φ_{o}⟩.  (74)

Let H′ = H[l_{ρ} ↦ v]. Since H′(l_{ρ}) = v and H ⊧ v : τ, H′ ⊧ v : τ. Therefore

H′ ⊧ l_{ρ} : ref_{ρ}τ, H′ ⊧ S : s, H′ ⊧ E : e, H′ ⊧ K : k.  (75)

By (74) and (75),

(l_{ρ}.S, H[l_{ρ} → v], E, C, K, φ ∪ {init(ρ)}) ⇝ (s_{o}, e_{o}, φ_{o}).

• case (l_{ρ}.S, H, E, get.C, K, φ)⇒(H(l_{ρ}).S, H, E, C, K, φ ∪ {read(ρ)}) l_{ρ} ∈ Dom(H)

There exist s, e, and k such that H ⊧ l_{ρ} : ref_{ρ}τ, H ⊧ S : s, H ⊧ E : e, H ⊧ K : k and ⟨ref_{l_{ρ}}τ.s, e, k, φ⟩ ⊢ get.C ⇝ ⟨s_{o}, e_{o}, φ_{o}⟩. Then by get,

⟨τ.s, e, k, φ ∪ {read(ρ)}⟩ ⊢ C ⇝ ⟨s_{o}, e_{o}, φ_{o}⟩.  (76)

Since H ⊧ l_{ρ} : ref_{ρ}τ and l_{ρ} ∈ Dom(H),

H ⊧ H(l_{ρ}) : τ  (77)

and by (76) and (77),

(H(l_{ρ}).S, H, E, C, K, ρ ∪ {read(ρ)}) ⇝ (s_{o}, e_{o}, φ_{o}).

• case (v.l_{ρ}.S, H, E, set.C, K, φ)⇒(().S, H[l_{ρ} → v], E, C, K, φ∪{write(ρ)}) l_{ρ} ∈ Dom(H)

There exist τ, s, e, and k such that H ⊧ v : τ, H ⊧ l_{ρ} : ref_{ρ}τ, H ⊧ S : s, H ⊧ E : e, H ⊧ K : k and ⟨τ.ref_{ρ}τ.s, e, k, φ⟩ ⊢ set.C ⇝ ⟨s_{o}, e_{o}, φ_{o}⟩. Then by set,

⟨unit.s, e, k, φ ∪ {write(ρ)}⟩ ⊢ C ⇝ ⟨s_{o}, e_{o}, φ_{o}⟩.  (78)

Let H′ = H[l_{ρ} ↦ v]. Since H′ ⊧ l_{ρ} : ref_{ρ}τ,

H′ ⊧ () : unit, H′ ⊧ S : s, H′ ⊧ E : e, H′ ⊧ K : k  (79)

and by (78) and (79),

(().S, H[l_{ρ} → v], E, C, K, φ ∪ {write(ρ)}) ⇝ (s_{o}, e_{o}, φ_{o}).
□

Lemma 7 (Progress) If (S, H, E, C, K, φ) ⇝ (s_{o}, e_{o}, φ_{o}) then either C and K are nil or there exsists M such that (S, H, E, C, K, φ)⇒M.

Proof If the configuration is typable, there exist s, e and k such that H ⊧ S : s, H ⊧ E : e, H ⊧ K : k, and ⟨s, e, k, φ⟩ ⊢ C ⇝ ⟨s_{o}, e_{o}, φ_{o}⟩. Since the code C is typable, there exists a rule last used during the typing of C. If the used rule is nil then C and K are nil. Otherwise we prove by the case analysis of the typing rules in Figure 4 that there exists a machine transition rule for each last used typing rule. Since the proof is obvious we omit the details. □

Now we prove the soundness theorem of our typing rules. Theorem 1 states that a machine configuration which has a type would not go wrong.

Theorem 1 (Soundness) Let C be a program. If (nil, ϕ, nil, C, nil, ϕ) ⇝ (s_{o}, e_{o}, φ_{o}) then either the machine transition sequence from (nil, ϕ, nil, C, nil, ϕ) is infinite or it stops with a final configuration M such that M ⇝ (s_{o}, e_{o}, φ′_{o}), and φ′_{o} ⊆ φ_{o}.

Proof By Lemma 6 and 7. □

When we extend our system to add new effects, the added effects should satisfy some properties to guarantee the soundness of the extended system. Since the restrictions on effects we made while proving Theorem 1 are only Lemma 4, we only need to check whether the new effects satisfy the lemma.

    λinitial.
       let counter = new initial in
           λinc. (counter := !counter + inc;
                  !counter)

==> compiled to etySECK

   fn (∀ρ.
         fetch (0); ref ρ; frame;
         fn (fetch (1); fetch (1); get; fetch (0);
             add; set; frame; deframe; fetch (1);
             get

: int →^{read(ρ),write(ρ)}int); deframe

:int\underrightarrow{init(ρ)}(int →^{init(ρ),write(ρ)}int))

   ;;

==> the result of type checking

: (∀ρ.int\underrightarrow{init(ρ)}(int →^{read(ρ),write(ρ)}int), nil, nil)

==> the result of actual run

   (Λρ.fn (fetch (0); ref ρ; frame;
           fn (fetch (1); fetch (1); get; fetch (0);
               add; set; frame; deframe; fetch (1);
               get

: int →^{read(ρ),write(ρ)}int); deframe

:int\underrightarrow{init(ρ)}(int →^{init(ρ),write(ρ)}int)),

   nil, nil)

Figure 5: Example program

3 Examples

Since our typing rules in Figure 3 and 4 are deterministic, implementation of a type checker is straightforward. Thus we omit a checking algorithm in this paper.

We present an example program from Talpin’s paper[5] and the type checking result of the program in Figure 5. The figure shows that our type checker verifies that annotated types and effects are valid and the result of the execution actually has the same type.

In order to show what happens to the code annotated with wrong types and effects, we present a modified code in Figure 6. The figure shows that since the return type of the outer function mismatches with the type the type checker expects, the type checker reports a type error.

Compilation from mini-ML to etySECK is trivial and we omit the detailed description of it. The key idea is to instantiate each polymorphic value when it is used by inserting a tapp instruction. In this case, we obtain the argument of the tapp instruction by unifying the

   fn (∀ρ.
         fetch (0); ref ρ; frame;
         fn (fetch (1); fetch (1); get; fetch (0);
             add; set; frame; deframe; fetch (1);
             get

: int →^{read(ρ),write(ρ)}int); deframe

:int\underrightarrow{init(ρ)}(int\underrightarrow{init(ρ)}int))

   ;;

==> the result of type checking

   Type Error: Function return type mismatch
   (nil,
    nil,
    nil,
    fn (∀ρ.
        fetch (0); ref ρ; frame;
        fn (fetch (1); fetch (1); get; fetch (0);
            add; set; frame; deframe; fetch (1);
            get

: int →^{read(ρ),write(ρ)}int); deframe

      :int\underrightarrow{init(ρ)}(int\underrightarrow{init(ρ)}int)),
    nil)
   DECLARED : int\underrightarrow{write(ρ)}int,

ACTUALLY : int →^{read(ρ),write(ρ)}int,

Figure 6: Example program Modified

polymorphic type and the type of the value at that point.

References

[1] P. J. Landin. The mechanical evaluation of expressions. The Computer Journal, 6(4):308– 320, January 1964.

[2] P. J. Landin. A correspondence between ALGOL 60 and Church’s lambda-notation: Part I. Communications of the ACM, 8(2):89–101, February 1965.

[3] P. J. Landin. A correspondence between ALGOL 60 and Church’s lambda-notation: Part II. Communications of the ACM, 8(3):158–165, March 1965.

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

[5] Jean-Piere Talpin and Pierre Jouvelot. Polymorphic type, region and effect inference. Journal of Functional Programming, 2(3):245–271, July 1992.

[6] Andrew K. Wright and Matthias Felleisen. A syntactic approach to type soundness. Technical Report TR91-160, Dept. of Computer Science, Rice University, (to appear in Information and Computation), June 1992.