A language is *type safe* if running a program in the language
cannot result in an *untrapped error*. A trapped error is
something like an exception or a message-not-found error, that is, it's
an error that is part of the defined behavior of the language.
An untrapped error is something like a segmentation fault, that is,
the program has run into an undefined state in which the language
doesn't define what should happen. A segmentation fault
is the underlying operating system catching the error, not the
language itself. It is the untrapped errors that hackers take advantage
of to break into computer systems. If you want to run untrusted
code without getting into trouble, then it's a good idea to only
run code that is in a type safe language!

Wright and Felleisen pioneered what has become the most flexible
approach to proving that a language is type safe in their 1992 paper
*A Syntactic Approach to Type Soundness*.
The general idea is to define a small-step operational semantics
for the language and show that if a program is well typed,
then it is either done reducing or it can reduce
to another well-typed program. The safety of an entire sequence
of reductions can then be proved by induction.
It is now common practice for language designers to prove type
safety for new language designs, or at least for interesting subsets
of the languages of interest.
Proving type safety does not require advanced mathematics and
isn't particularly challenging, except that it is often rather
tedious, requiring many technical lemmas in which it is easy
to make a mistake.

It turns out that the choice in formulation of the operational semantics can make a significant difference regarding how many lemmas, and how tedious, the proof of type safety becomes. In this blog post, I present an operational semantics that removes the need for many of the standard lemmas. The semantics is based on an abstract machine. The language will be the simply-typed lambda calculus in A-normal form, extended with recursive functions and a few primitive operators. Despite its small size, this language is Turing complete. This language is roughly equivalent to the target language discussed in my previous posts about Structural Induction and the ECD Machine. In the following I present the syntax, operational semantics, and type system of this language. Then I give the proof of type safety. The proof will rely on five lemmas, one lemma for each function or relation used in the operational semantics: the variable partial function, the partial function that defines the behavior of the primitive operators, the partial function for evaluating expression, the transition relation for the abstract machine, and the multi-transition relation . The lemma for the transition relation is the main event.

### Syntax

### Operational Semantics

We use the notation for the empty list.
Given a list ,
the notation is a larger list with
as the first
element and the rest of the elements are the same as .
We use lists of key-value pairs (*association lists*) to
represent mapping from variables to types (type environments) and
variables to values (environments). The following lookup (partial)
function finds the thing associated with a given key in an association
list.
Next we define the function,
which gives meaning to the
primitive operators.
The function maps expressions
to values, using environment .
The values of this language are constants and closures, as defined
below.
The definition of
uses the function
for variables, the function
for primitive operations, and turns functions to closures.
A stack is a list
of statement-environment pairs. The state
of the machine is simply a stack.
The top of the stack
contains the actively-executing statement and its environment. The
relation defines transitions
between states. There are only three transition rules, for primitive operators,
calling functions, and returning from functions.
We define in the usual way, as follows.
The semantics of this language is given by the following
function.
A state is *final* if it is of the form
and for
some .

### Type System

The types for the constants is given by the function. The function maps a primitive operator and argument types to the return type. The following presents the type rules for expressions, definitions, and statements. Our proof of type safety will require that we define notions of well-typed values, well-typed environments, well-typed stacks, and well-typed states.

### Proof of Type Safety

The first lemma proves that when an operator is applied to
values of the expected type, the result is a value whose type
matches the return type of the operator.

**Lemma** ( is safe)

If and for , then and ,
for some .

- If the operator is , then we have and . Then because , we know that for . Then and we have .
- If the operator is , then we have and . Then because , we know that for some . Then and we have .
- If the operator is , then we have and . Then because , we know that for . Then and we have .

The second lemma says that if you have an environment that is well-typed with respect to the type environment, and if a variable

*x*is associated with type

*T*in the type environment, then looking up

*x*in the environment produces a value that has type

*T*.

**Lemma**( is safe)

If and , then and for some .

*Proof.*We proceed by induction on .

- Case

But then we have a contradition with the premise , so this case is vacuously true. - Case :

Next we consider two cases, whether or not.- Case : Then and , so we conclude that .
- Case : Then and . By the induction hypothesis, we have and for some , which completes this case.

The next lemma proves that a well-typed expression evaluates to a value of the expected type.

**Lemma**( is safe)

If and , then and for some .

*Proof.*We proceed by cases on the expression .

- Case :

From we have and therefore . Also, we have , which completes this case. - Case :

From we have . We then apply the lookup is safe lemma to obtain and for some . Thus, we have and this case is complete. - Case :

We have . From we have , with . Together with , we conclude that .

Now for the fourth and most important lemma. This lemma states that if a state is well typed, then either the state is a final state or the state can transition to a new state of the same type. In the literature, this lemma is often split into two lemmas called

*progress*and

*preservation*. In the setting of an abstract machine, it's convenient to merge these two lemmas into one lemma. Note that the conclusion of this lemmas includes two alternatives: the state is final or it can take a step. The power of this lemma is that it rules out the third alternative, that the state is not final and can't take a step. Such a situation is referred to as "stuck" and corresponds to untrapped errors.

**Lemma**( is safe)

If , then either is a final state or and .

*Proof.*Because we know that , , , and . We proceed by cases on because the transition rule that will apply depends primarily on .

- Case :

We have and . So and for . Because is safe, we have and for . Because is safe, we have and for some . Thus, the current state takes the following transition. We have

and therefore - Case :

From we have and . Thus, we also have and . Because is safe, there exist and such that , , , and . The only way for to be true is for to be a closure. That is, . This closure is well typed, so we have and . We have what we need to know that the current state transitions as follows. We can deduce

and

so we have everything necessary to conclude - Case :

If the stack is empty, then is a final state and this case is complete. If the stack is not empty, we have . Then, because , we have , , , and . Because , we have and therefore and for some (because is safe). So the current state takes the following transition: We have , which is the last thing we needed to conclude that .

**Lemma**( is safe)

If and , then .

*Proof.*The proof is by induction on .

- Case : We already have .
- Case : Because is safe and deterministic (the three transition rules obviously do not overlap), we have . Then by the induction hypothesis, we conclude that .

**Theorem**(Type Safety)

If , then either

- and , or
- and for some , or
- (the program does not terminate).

*Proof.*Suppose that the program terminates. We have for some and . Because is safe, we have . Then because is safe, we know that either is final or it can take a step. But we know it can't take a step, so it must be final. So and . Then because is safe, we have and . If , then we have and . If , then , , and .

QED.

That's it! Type safety in just five easy lemmas.

In the transition rule Call, I think v_2 should equal to V(e_2, /rho), instead of V(e_1, /rho).

ReplyDeleteYes, thank you!

Delete