Syntactic Control of Interference Part 2

John C. Reynolds^{1}

December 23, 1994

CMU-CS-89-130

School of Computer Science Carnegie Mellon University Pittsburgh, PA 15213

This is a preprint of a paper that will appear in the Proceedings of the 16th International Colloquium on Automata, Languages, and Programming (Stresa, July 11–15, 1989), to be published in the Springer-Verlag Lecture Notes in Computer Science.

Abstract

In 1978, we proposed that Algol-like languages should be constrained so that aliasing between variables and, more generally, interference between commands or procedures would be syntactically detectable in a fail-safe manner. In particular, we proposed syntactic restrictions that prohibited interference between distinct identifiers, while permitting interference between qualifications of the same identifier. However, these restrictions had the unfortunate property that syntactic correctness was not preserved by beta reduction.

In the present paper, we show how this difficulty can be avoided by the use of a variant of conjunctive types. We also give an algorithm for typechecking explicitly typed programs.

1Research supported by NSF Grant CCR-8620191. A portion of the research was also sponsored by the Defense Advanced Research Projects Agency (DOD), ARPA Order No. 4976, under contract number F33615-87-C-1499, monitored by the Air Force Wright Aeronautical Laboratories, Wright-Patterson AFB, Ohio. The views and conclusions contained in this document are those of the authors and should not be interpreted as representing the official policies, either expressed or implied, of any agency of the US Government.

1. Introduction

Whenever a programming language combines assignment with a sufficiently powerful procedure mechanism, the phenomenon of “aliasing” appears, as well as various anomalies that are often called “interfering side effects”. These are all instances of the general phenomenon of interference: for example, two (phrases denoting) variables interfere if assigning to either one can affect the value of the other, two commands interfere if either one assigns to a variable that is evaluated or assigned to by the other, and two procedures interfere if either one assigns to a global variable that is evaluated or assigned to by the other.

Interference is not always undesirable; procedures that manipulate common global variables are widely used in programming, and collections of such procedures are the essence of “object-oriented” programming. But it would be desirable to constrain a programming language so that interference is syntactically detectable (in a fail-safe sense). In particular, such a constraint is necessary in a language that provides concurrent processing with shared variables, in order to enforce the protection of the shared variables by critical regions [4, 1, 3].

Eleven years ago, in [7], I proposed syntactic constraints to make interference detectable that were based on three principles:

• If no identifier occurring free in the phrase p interferes with any identifier occurring free in the phrase q, then p does not interfere with q.

In effect, all “channels” of interference must be named by identifiers.

• Distinct identifiers do not interfere.

One can still have interfering procedures (or other entities), but they must occur within a single object or, in other words, be named by different qualifications of the same identifier.

• Passive phrases, which perform no assignment or other actions that could cause interference, do not interfere with one another.

Passive phrases include both (side-effect-free) expressions and procedures that do not assign to global variables.

Unfortunately, the specific syntactic constraints described in [7] have the unhappy consequence that certain legal phrases beta-reduce to illegal phrases. In the present paper, we will use conjunctive types [2] to define constraints, based on the above principles, that avoid this problem. The essential change is that, instead of focusing on a relation between phrases (denoted by # in [7]) that asserts that the phrases do not interfere, we will focus on a relation between type assignments (denoted by ⊥ and called independence) that asserts that the capabilities represented by the type assignments cannot cause interference.

2. An Illustrative Language

To make our exposition concrete, we will use an Algol-like illustrative language [5] that is an extended lambda calculus with construction and selection operations for named tuples, a conditional construct, and some of the various operations for expressions and commands that are typically found in imperative languages. We will also introduce an operator ∥ that executes two command concurrently; our goal is to prohibit interference between the operands of ∥, so that the semantics of our language will be determinate. (In a more realistic language, indeterminacy would be permitted, but only under the control of critical regions.)

The following productions define the untyped abstract syntax of our language:

⟨phrase⟩ ::= ⟨identifier⟩  identifiers
| λ⟨identifier⟩: ⟨finite set of types⟩. ⟨phrase⟩  abstraction
| ⟨phrase⟩⟨phrase⟩  application
| ⟨⟨identifier⟩ ≡ ⟨phrase⟩, …, ⟨identifier⟩ ≡ ⟨phrase⟩⟩  tupling
| ⟨phrase⟩.⟨identifier⟩  selection
| if ⟨phrase⟩ then ⟨phrase⟩ else ⟨phrase⟩  conditionals
| 0 | 0.5 | ⟨phrase⟩ + ⟨phrase⟩  expressions
| ⟨phrase⟩ := ⟨phrase⟩ | ⟨phrase⟩; ⟨phrase⟩ | while ⟨phrase⟩ do ⟨phrase⟩ commands
| ⟨phrase⟩ ∥ ⟨phrase⟩  concurrency

Of course in a real language there would be additional operations for expressions and commands, but such operations are so similar to those we have included that they would add nothing but length to our exposition. On the other hand, there are language features, such as multiargument procedures, let definitions, recursion, and variable declarations, that we have omitted since they are syntactic sugar that can be defined in terms of the above language plus appropriate built-in procedures [5].

This illustrative language is similar to the recently proposed Forsythe language [6], except that it lacks the escape operator, the merging operation, and the treatment of assignment as a procedure call that occur in Forsythe.

Notice that lambda expressions contain explicit type information, which will be used to make typechecking feasible.

3. Types

As in [5] and [6], we distinguish between a data type, such as “integer” and “Boolean”, which denotes a set of values appropriate to some kind of variable, and a phrase type, such as “integer expression” or “proper procedure accepting an integer expression”, which denotes a set (or domain) of meanings appropriate to some kind of phrase. (The unqualified term “type” will always mean “phrase type”.)

We assume that the set of data types is equipped with a preorder ≤_{data}, and say that δ is a subtype of δ′ when δ ≤_{data} δ′. Specifically, we assume that int(eger), real, and bool(ean) are data types, and that int ≤_{data} real:

real int bool

More generally, we assume that the set of data types is equipped with two binary operations ˙⊔ and ˙⊓ such that δ_{1} ˙⊔ δ_{2} (δ_{1} ˙⊓ δ_{2}) is a finite complete set of upper (lower) bounds of δ_{1} and δ_{2}, i.e.

If δ ^{∈} δ_{1} ˙⊔ δ_{2} then δ_{1} ≤_{data} δ and δ_{2} ≤_{data} δ.

If δ_{1} ≤_{data} δ and δ_{2} ≤_{data} δ then there is a δ_{0} ^{∈} δ_{1} ˙⊔ δ_{2} such that δ_{0} ≤_{data} δ.

If δ ^{∈} δ_{1} ˙⊓ δ_{2} then δ ≤_{data} δ_{1} and δ ≤_{data} δ_{2}.

If δ ≤_{data} δ_{1} and δ ≤_{data} δ_{2} then there is a δ_{0} ^{∈} δ_{1} ˙⊓ δ_{2} such that δ ≤_{data} δ_{0}.

For phrase types, we use the canonical formalism for conjunctive types [6], in which there is no explicit conjunction operator, but certain contexts require an identifier or phrase to have all types belonging to some finite set, rather than a single type.

Corresponding to each data type δ, there are two phrase types: δ exp(ression), describing phrases that can be evaluated to obtain a value of data type δ, and δ acc(eptor), describing phrases whose execution can accept a value of data type δ. (What is usually called a δ variable is a phrase having both of the types δ exp and δ acc.) There is one additional primitive phrase type: comm(and).

If an object possesses a field of type θ that is named by an identifier ι, then the object has the type ι: θ. Notice that no type describes more than one field; instead an object with several fields has several types, each describing a single field.

If θ̂ is a finite set of types and θ is a type, then θ̂ ⟶ θ is a type describing a procedure whose call will have type θ when its parameter has all of the types in θ̂. Moreover, if such a procedure causes no assignment to a global variable, it will also have the type θ̂ ⟶_{P} θ and be said to be a passive procedure.

We will partition the set of phrase types into passive and active types. First, however, we note that, without loss of generality, we can require a procedure whose calls are passive to itself be passive and to have a passive parameter. Putting the matter the other way round, we require that in θ̂ ⟶ θ, θ must be active (i.e. not passive), and in θ̂ ⟶_{P} θ, θ must be active if any member of θ̂ is active.

Henceforth, we will use the following metavariables:

δ: data types
ϕ: passive phrase types
α: active phrase types
θ: arbitrary phrase types
ϕ̂: finite sets of passive phrase types
θ̂: finite sets of arbitrary phrase types
ι: identifiers .

(For brevity, we will call a finite set of phrase types passive when its members are all passive.) Then the sets of passive and active phrase types may be defined grammatically:

ϕ ::= δ exp | ϕ̂ ⟶_{P} ϕ | θ̂ ⟶_{P} α | ι: ϕ
α ::= δ acc | comm | θ̂ ⟶ α | ι: α
θ ::= ϕ | α

The subtype preorder is defined for phrase types and for finite sets of phrase types by mutual recursion. For phrase types,

δ exp ≤ δ′ exp when δ ≤_{data} δ′
δ acc ≤ δ′ acc when δ′ ≤_{data} δ

comm ≤ comm

\begin{matrix}θ̂ ⟶_{P} θ ≤ θ̂′ ⟶_{P} θ′ \\ θ̂ ⟶_{P} θ ≤ θ̂′ ⟶ θ′ \\ θ̂ ⟶ θ ≤ θ̂′ ⟶ θ′ \end{matrix} \} when θ̂′ ≤ θ̂ and θ ≤ θ′

ι: θ ≤ ι: θ′ when θ ≤ θ′ ,

and in any other case θ ≤ θ′ is false. For finite sets of phrase types,

θ̂ ≤ θ̂′ when (∀θ′ ^{∈} θ̂′)(∃θ ^{∈} θ̂) θ ≤ θ′ .

(Note that θ̂′ ⊆ θ̂ implies θ̂ ≤ θ̂′.) This definition of subtype implies

Proposition 1 If ϕ is passive and θ ≤ ϕ then θ is passive.

Proposition 2 If ϕ̂ is a passive subset of θ̂, and θ̂′ ≤ θ̂, then there exists a passive subset ϕ̂′ of θ̂′ such that ϕ̂′ ≤ ϕ̂.

θ̂ ϕ̂ θ̂′ ϕ̂′  ⊆ ≤ ⊆  ≤

Proof : Take ϕ̂′ to be the set of passive members of θ̂′. (End of Proof )

Now suppose two phrases p_{1} and p_{2} occur in some context, such as p_{1} ∥ p_{2}, that prohibits their interference. Then if some identifier is used actively in either one of p_{1} or p_{2}, it must not be used at all in the other (though it may occur in a vacuous context such as an argument to a constant procedure, or an object field that is never selected). To formalize this constraint, let θ̂_{1} and θ̂_{2} be the sets of types with which the identifier is used in p_{1} and p_{2} respectively. Then we require that θ̂_{1} ⊥ θ̂_{2} hold, where ⊥ is defined to be the symmetric relation on finite sets of phrase types such that

θ̂_{1} ⊥ θ̂_{2} if and only if θ̂_{1} = {} or θ̂_{2} = {} or θ̂_{1} ∪ θ̂_{2} is passive .

When θ̂_{1} ⊥ θ̂_{2} we say that θ̂_{1} and θ̂_{2} are independent. This relation satisfies:

Proposition 3 If θ̂_{1} ⊥ θ̂_{2} and θ̂′_{1} ⊆ θ̂_{1} then θ̂′_{1} ⊥ θ̂_{2}.

Proposition 4 If θ̂_{1} ⊥ θ̂_{2} and θ̂′_{1} ⊥ θ̂_{2} then (θ̂_{1} ∪ θ̂′_{1}) ⊥ θ̂_{2}.

Proposition 5 If θ̂_{1} and θ̂_{2} are subsets of θ̂ such that θ̂_{1} ⊥ θ̂_{2}, and θ̂′ ≤ θ̂, then there exist subsets θ̂′_{1} and θ̂′_{2} of θ̂′ such that θ̂′_{1} ⊥ θ̂′_{2}, θ̂′_{1} ≤ θ̂_{1}, and θ̂′_{2} ≤ θ̂_{2}.

[figure: θ̂; θ̂_{1}; θ̂_{2}; θ̂′; θ̂′_{1}; θ̂′_{2}; ⊆; ⊆; ⊥; ≤; ⊆; ⊆; ⊥; ≤; ≤]

Proof : If θ̂_{1} is empty, take θ̂′_{1} to be empty and θ̂′_{2} to be θ̂′. If θ̂_{2} is empty, take θ̂′_{2} to be empty and θ̂′_{1} to be θ̂′. If θ̂_{1} and θ̂_{2} are passive, take ϕ̂ to be θ̂_{1} ∪ θ̂_{2}, use Proposition 2, and then take both θ̂′_{1} and θ̂′_{2} to be ϕ̂′. (End of Proof )

Next we extend the operation ˙⊔ from data types to phrase types. (Eventually, we will need this operation to typecheck conditional constructs.) Specifically, we define ˙⊔ to map pairs of types into finite sets of types as follows:

δ_{1} exp ˙⊔ δ_{2} exp = { δ exp | δ ^{∈} δ_{1} ˙⊔ δ_{2} }
δ_{1} acc ˙⊔ δ_{2} acc = { δ acc | δ ^{∈} δ_{1} ˙⊓ δ_{2} }

comm ˙⊔ comm = {comm}

(θ̂_{1} ⟶_{P} θ_{1}) ˙⊔ (θ̂_{2} ⟶_{P} θ_{2}) = { (θ̂_{1} ∪ θ̂_{2}) ⟶_{P} θ | θ ^{∈} θ_{1} ˙⊔ θ_{2} }

\begin{matrix}(θ̂_{1} ⟶_{P} θ_{1}) ˙⊔ (θ̂_{2} ⟶ θ_{2}) \\ (θ̂_{1} ⟶ θ_{1}) ˙⊔ (θ̂_{2} ⟶_{P} θ_{2}) \\ (θ̂_{1} ⟶ θ_{1}) ˙⊔ (θ̂_{2} ⟶ θ_{2}) \end{matrix} \} = \{ (θ̂_{1} ∪ θ̂_{2}) ⟶ θ | θ ^{∈} θ_{1} ˙⊔ θ_{2} \}

ι: θ_{1} ˙⊔ ι: θ_{2} = { ι: θ | θ ^{∈} θ_{1} ˙⊔ θ_{2} } ,

and in any other case θ_{1} ˙⊔ θ_{2} = {}. Then

Proposition 6 θ_{1} ˙⊔ θ_{2} is a finite complete set of upper bounds of θ_{1} and θ_{2}, i.e.

(a) If θ ^{∈} θ_{1} ˙⊔ θ_{2} then θ_{1} ≤ θ and θ_{2} ≤ θ.

(b) If θ_{1} ≤ θ and θ_{2} ≤ θ then there is a θ_{0} ^{∈} θ_{1} ˙⊔ θ_{2} such that θ_{0} ≤ θ.

Proof : Each half of the proposition is proved separately by induction on the structure of θ. (End of Proof )

(Using Propositions 1 and 6a, the reader may verify that the members of θ_{1} ˙⊔ θ_{2} never violate the requirement that, when a procedural type has a passive result type, both the procedural type and its argument type must be passive.)

Moreover, we can define the operation ⊔, mapping pairs of finite sets of types into finite sets of types, such that

θ̂_{1} ⊔ θ̂_{2} = ⋃{ θ_{1} ˙⊔ θ_{2} | θ_{1} ^{∈} θ̂_{1} and θ_{2} ^{∈} θ̂_{2} } .

Then

Proposition 7 θ̂_{1} ⊔ θ̂_{2} is a least upper bound of θ̂_{1} and θ̂_{2}.

Now we define a type assignment to be a function from the set of identifiers to the set of finite sets of phrase types that maps all but a finite number of identifiers into the empty set. We say that a type assignment is passive when it maps every identifier into a passive set, and we use the following metavariables for type assignments:

Φ: passive type assignments
Θ: arbitrary type assignments .

We write [ ] for the type assignment that maps every identifier into the empty set, and [ Θ | ι: θ̂] for the type assignment such that [ Θ | ι: θ̂]ι = θ̂ and [ Θ | ι: θ̂]ι′ = Θι′ when ι′ ≠ ι. We also write [ ι_{1}: θ̂_{1} | … | ι_{n}: θ̂_{n}] to abbreviate [ … [ [ ] | ι_{1}: θ̂_{1} ] … | ι_{n}: θ̂_{n}].

We define the relations ⊆, ≤, ⊥, and the operation ∪ on type assignments by pointwise extension:

Θ ⊆ Θ′ =^{def} (∀ι) Θι ⊆ Θ′ι

Θ ≤ Θ′ =^{def} (∀ι) Θι ≤ Θ′ι

Θ ⊥ Θ′ =^{def} (∀ι) Θι ⊥ Θ′ι

(Θ ∪ Θ′)ι =^{def} Θι ∪ Θ′ι .

As a consequence, Propositions 2 to 5 can be extended from finite sets of types to type assignments:

Proposition 8 If Φ is a passive subset (in the pointwise-extended sense) of Θ, and Θ′ ≤ Θ, then there exists a passive subset Φ′ of Θ′ such that Φ′ ≤ Φ.

Proposition 9 If Θ_{1} ⊥ Θ_{2} and Θ′_{1} ⊆ Θ_{1} then Θ′_{1} ⊥ Θ_{2}.

Proposition 10 If Θ_{1} ⊥ Θ_{2} and Θ′_{1} ⊥ Θ_{2} then (Θ_{1} ∪ Θ′_{1}) ⊥ Θ_{2}.

Proposition 11 If Θ_{1} and Θ_{2} are subsets of Θ such that Θ_{1} ⊥ Θ_{2}, and Θ′ ≤ Θ, then there exist subsets Θ′_{1} and Θ′_{2} of Θ′ such that Θ′_{1} ⊥ Θ′_{2}, Θ′_{1} ≤ Θ_{1}, and Θ′_{2} ≤ Θ_{2}.

4. Typings and their Inference Rules

If Θ is a type assignment, p is a phrase, and θ is a type, then the formula Θ ⊢ p : θ, called a typing, asserts that the phrase p has the type θ when its free identifiers are assigned types by Θ. When θ̂ is a finite set of types, we write Θ ⊢ p : θ̂ to abbreviate the finite set of typings

{ Θ ⊢ p : θ | θ ^{∈} θ̂} .

The valid typings of our illustrative language are those that are provable from the following rules of inference:

• Identifiers

\overline{Θ ⊢ ι : θ} when θ ^{∈} Θι

• Subtypes

\frac{Θ ⊢ p : θ}{Θ ⊢ p : θ′} when θ ≤ θ′

• Abstraction

[ Φ | ι: θ̂] ⊢ p : θ Θ ⊢ (λι: θ̂_{0}. p) : θ̂ ⟶_{P} θ

when θ̂ ⊆ θ̂_{0}, Φ ⊆ Θ, Φ is passive, and if θ is passive then θ̂ is passive

\frac{[ Θ | ι: θ̂] ⊢ p : α}{Θ ⊢ (λι: θ̂_{0}. p) : θ̂ ⟶ α} when θ̂ ⊆ θ̂_{0}

• Application

Θ_{1} ⊢ p_{1} : θ̂ ⟶_{P} θ Θ_{2} ⊢ p_{2} : θ̂ Θ ⊢ p_{1} p_{2} : θ

when Θ_{1} ⊆ Θ, Θ_{2} ⊆ Θ, Θ_{1} ⊥ Θ_{2} and if θ is passive then θ̂ is passive

\begin{matrix}Θ_{1} ⊢ p_{1} : θ̂ ⟶ α \\ Θ_{2} ⊢ p_{2} : θ̂ \\ Θ ⊢ p_{1} p_{2} : α \end{matrix} when Θ_{1} ⊆ Θ, Θ_{2} ⊆ Θ, and Θ_{1} ⊥ Θ_{2}

• Tupling

\frac{Θ ⊢ p_{k} : θ}{Θ ⊢ ⟨ι_{1} ≡ p_{1}, …, ι_{k} ≡ p_{k}, …, ι_{n} ≡ p_{n}⟩ : (ι_{k}: θ)}

• Field Selection

\frac{Θ ⊢ p : (ι: θ)}{Θ ⊢ p.ι : θ}

• Conditionals

Θ ⊢ p_{1} : bool exp
Θ ⊢ p_{2} : θ
Θ ⊢ p_{3} : θ
Θ ⊢ if p_{1} then p_{2} else p_{3} : θ

• Arithmetic Expressions

Θ ⊢ 0 : int exp

Θ ⊢ 0.5 : real exp

Θ ⊢ p_{1} : int exp
Θ ⊢ p_{2} : int exp
Θ ⊢ p_{1} + p_{2} : int exp

Θ ⊢ p_{1} : real exp Θ ⊢ p_{2} : real exp Θ ⊢ p_{1} + p_{2} : real exp

• Commands

Θ ⊢ p_{1} : δ acc
Θ ⊢ p_{2} : δ exp
Θ ⊢ p_{1} := p_{2} : comm

Θ ⊢ p_{1} : comm Θ ⊢ p_{2} : comm Θ ⊢ p_{1} ; p_{2} : comm

Θ ⊢ p_{1} : bool exp
Θ ⊢ p_{2} : comm
Θ ⊢ while p_{1} do p_{2} : comm

• Concurrency

Θ_{1} ⊢ p_{1} : comm Θ_{2} ⊢ p_{2} : comm Θ ⊢ p_{1} ∥ p_{2} : comm when Θ_{1} ⊆ Θ, Θ_{2} ⊆ Θ, and Θ_{1} ⊥ Θ_{2}

In the rules for an application p_{1}p_{2}, notice that the requirement Θ_{1} ⊥ Θ_{2} prohibits interference between p_{1} and p_{2} (just as with the concurrent construction p_{1} ∥ p_{2}), so that a procedure must not interfere with its argument. This is the basic mechanism that insures that reduction preserves syntactic correctness.

In the rules for abstraction, the condition θ̂ ⊆ θ̂_{0} (where θ̂_{0} is the finite set of types occurring explicitly in the lambda expression) restricts the procedural type that can be inferred; this restriction is introduced to make typechecking feasible.

In what follows, we will prove several propositions by induction on the size of a proof, using the above rules, of a typing, with a case analysis over the different inference rules that may occur at the root of the proof tree. Fortunately, most of the inference rules fall into one of two classes that can be treated uniformly in such a case analysis:

• An inference rule is called a normal rule if it is equivalent to a (possibly infinite) set

of rules of the form

Θ ⊢ p_{1} : θ̂_{1}
⋮
Θ ⊢ p_{n} : θ̂_{n}
Θ ⊢ ε(p_{1}, …, p_{n}) : θ

where Θ, p_{1}, …, p_{n} are metavariables, ε(p_{1}, …, p_{n}) is a phrase constructed from p_{1}, …, p_{n} without using binding operations, θ̂_{1}, …, θ̂_{n} are finite sets of types not containing metavariables, θ is a type not containing metavariables, and if θ is passive then θ̂_{1}, …, θ̂_{n} are passive.

• An inference rule is called a noninterference rule if it is equivalent to a (possibly infinite) set of rules of the form

\begin{matrix}Θ_{1} ⊢ p_{1} : θ̂_{1} \\ Θ_{2} ⊢ p_{2} : θ̂_{2} \\ Θ ⊢ ε(p_{1}, p_{2}) : θ \end{matrix} when Θ_{1} ⊆ Θ, Θ_{2} ⊆ Θ, and Θ_{1} ⊥ Θ_{2}

where Θ_{1}, Θ_{2}, Θ, p_{1}, and p_{2} are metavariables, ε(p_{1}, p_{2}) is a phrase constructed from p_{1} and p_{2} without using binding operations, θ̂_{1} and θ̂_{2} are finite sets of types not containing metavariables, θ is a type not containing metavariables, and if θ is passive then θ̂_{1} and θ̂_{2} are passive.

For example, when k and n are integers such that 1 ≤ k ≤ n, θ is a type, and ι_{1}, …, ι_{n} are identifiers, let R_{nkθι_{1}...ι_{n}} be the rule

\frac{Θ ⊢ p_{k} : \{θ\}}{Θ ⊢ ⟨ι_{1} ≡ p_{1}, …, ι_{k} ≡ p_{k}, …, ι_{n} ≡ p_{n}⟩ : (ι_{k}: θ)}

Then the inference rule for object construction is equivalent to the set of rules

{ R_{nkθι_{1}...ι_{n}} | 1 ≤ k ≤ n and θ is a type and ι_{1}, …, ι_{n} are identifiers } ,

and is therefore a normal rule.

On the other hand, when θ̂ is a finite set of types and α is an active type, let R_{θ̂α} be the rule

\begin{matrix}Θ_{1} ⊢ p_{1} : \{θ̂ ⟶ α\} \\ Θ_{2} ⊢ p_{2} : θ̂ \\ Θ ⊢ p_{1} p_{2} : α \end{matrix} when Θ_{1} ⊆ Θ, Θ_{2} ⊆ Θ, and Θ_{1} ⊥ Θ_{2}

Then the second inference rule for application is equivalent to the set of rules

{ R_{θ̂α} | θ̂ is a finite set of types and α is a type } ,

and is therefore a noninterference rule.

The reader may verify that, except for the rule for identifiers and the two rules for abstraction, every inference rule is either a normal rule or a noninterference rule.

Proposition 12 If Θ′ ≤ Θ and Θ ⊢ p : θ then Θ′ ⊢ p : θ.

Proof : By induction on the proof size of Θ ⊢ p : θ.

(1) If the proof root is the rule for identifiers, then p is an identifier ι and θ ^{∈} Θι. Since Θ′ι ≤ Θι, there is a θ′ ^{∈} Θ′ι such that θ′ ≤ θ. Then the identifier rule gives Θ′ ⊢ ι : θ′ and the subtype rule gives Θ′ ⊢ ι : θ.

(2) If the proof root is a normal rule, then p must have the form ε(p_{1}, …, p_{n}), and the premisses of the rule must have the forms Θ ⊢ p_{1} : θ̂_{1}, …, Θ ⊢ p_{n} : θ̂_{n}. By the induction hypothesis (applied to each member of each θ̂_{i}), Θ′ ⊢ p_{1} : θ̂_{1}, …, Θ′ ⊢ p_{n} : θ̂_{n}, and by the rule used at the root, Θ′ ⊢ ε(p_{1}, …, p_{n}) : θ.

(3) If the proof root is a noninterference rule, then p must have the form ε(p_{1}, p_{2}) and the premisses of the rule must have the forms Θ_{1} ⊢ p_{1} : θ̂_{1} and Θ_{2} ⊢ p_{2} : θ̂_{2}, where Θ_{1} and Θ_{2} are subsets of Θ such that Θ_{1} ⊥ Θ_{2}. By Proposition 11, there are subsets Θ′_{1} and Θ′_{2} of Θ′ such that Θ′_{1} ⊥ Θ′_{2}, Θ′_{1} ≤ Θ_{1}, and Θ′_{2} ≤ Θ_{2}. By the induction hypothesis, Θ′_{1} ⊢ p_{1} : θ̂_{1} and Θ′_{2} ⊢ p_{2} : θ̂_{2}, and by the rule used at the root, Θ′ ⊢ ε(p_{1}, p_{2}) : θ.

(4) If the proof root is the first rule for abstraction, then its premiss has the form [ Φ | ι: θ̂] ⊢ ⋯, where Φ is a passive subset of Θ. By Proposition 8, there is a passive subset Φ′ of Θ′ such that Φ′ ≤ Φ. Then [ Φ′ | ι: θ̂] ≤ [ Φ | ι: θ̂], and thus the induction hypothesis allows us to replace [ Φ | ι: θ̂] by [ Φ′ | ι: θ̂], and the rule at the root allows us to replace Θ by Θ′.

The more straightforward case where the proof root is the second rule for abstraction is left to the reader. (End of Proof )

Proposition 13 (a) If ϕ is passive and Θ ⊢ p : ϕ then there exists a passive Φ ⊆ Θ such that Φ ⊢ p : ϕ.

(b) If ϕ̂ is passive and Θ ⊢ p : ϕ̂ then there exists a passive Φ ⊆ Θ such that Φ ⊢ p : ϕ̂.

Proof : By induction on the proof size of Φ ⊢ p : ϕ or Φ ⊢ p : ϕ̂. Within the induction step, we prove (a) by case analysis of the proof root and then show that (b) follows from (a).

(a1) If the proof root is the rule for identifiers, then p is an identifier ι and ϕ ^{∈} Θι, so that one can take Φ to be [ ι: {ϕ}].

(a2) If the proof root is a normal rule, then p must have the form ε(p_{1}, …, p_{n}) and the premisses of the rule must have the forms Θ ⊢ p_{1} : ϕ̂_{1}, …, Θ ⊢ p_{n} : ϕ̂_{n}, where the ϕ̂_{i}’s are passive. By the induction hypothesis there are passive Φ_{1}, …, Φ_{n} ⊆ Θ such that Φ_{1} ⊢ p_{1} : ϕ̂_{1}, …, Φ_{n} ⊢ p_{n} : ϕ̂_{n}. Let Φ be Φ_{1} ∪ ⋯ ∪ Φ_{n}, which is a passive subset of Θ. Then, since Φ_{i} ⊆ Φ implies Φ ≤ Φ_{i}, Proposition 12 gives Φ ⊢ p_{1} : ϕ̂_{1}, …, Φ ⊢ p_{n} : ϕ̂_{n}, and the rule used at the root gives Φ ⊢ ε(p_{1}, …, p_{n}) : ϕ.

(a3) If the proof root is a noninterference rule, then p must have the form ε(p_{1}, p_{2}) and the premisses of the rule must have the forms Θ_{1} ⊢ p_{1} : ϕ̂_{1} and Θ_{2} ⊢ p_{2} : ϕ̂_{2}, where Θ_{1} and Θ_{2} are subsets of Θ such that Θ_{1} ⊥ Θ_{2}, and ϕ̂_{1} and ϕ̂_{2} are passive. By the induction hypothesis there are passive Φ_{1} ⊆ Θ_{1} and Φ_{2} ⊆ Θ_{2} such that Φ_{1} ⊢ p_{1} : ϕ̂_{1} and Φ_{2} ⊢ p_{2} : ϕ̂_{2}. Let Φ be Φ_{1} ∪ Φ_{2}, which is a passive subset of Θ. Then Φ_{1} and Φ_{2} are subsets of Φ that, since they are passive, satisfy Φ_{1} ⊥ Φ_{2}. Thus the rule used at the root gives Φ ⊢ ε(p_{1}, p_{2}) : ϕ.

(a4) If the proof root is the first rule for abstraction, then its premiss has the form [ Φ | ι: θ̂] ⊢ ⋯, where Φ ⊆ Θ is passive. Then, since Φ is a subset of itself, we can replace Θ by Φ in the consequence of the rule.

The proof root cannot be the second rule for abstraction, since the consequence of this rule never has the form Θ ⊢ p : ϕ for passive ϕ.

(b) If Θ ⊢ p : ϕ̂, then Θ ⊢ p : ϕ_{i} for each of the finitely many ϕ_{i} ^{∈} ϕ̂. From (a), for each ϕ_{i} there is a passive Φ_{i} ⊆ Θ such that Φ_{i} ⊢ p : ϕ_{i}. Let Φ be the union of these Φ_{i}, which is a passive subset of Θ. Then, since Φ_{i} ⊆ Φ implies Φ ≤ Φ_{i}, Proposition 12 gives Φ ⊢ p : ϕ_{i} for each ϕ_{i}, and thus Φ ⊢ p : ϕ̂. (End of Proof )

Proposition 14 If θ̂_{1} and θ̂_{2} are subsets of θ̂ such that θ̂_{1} ⊥ θ̂_{2}, and Θ ⊢ p : θ̂, then there exist subsets Θ_{1} and Θ_{2} of Θ such that such that Θ_{1} ⊥ Θ_{2}, Θ_{1} ⊢ p : θ̂_{1}, and Θ_{2} ⊢ p : θ̂_{2}.

[figure: θ̂; θ̂_{1}; θ̂_{2}; Θ; Θ_{1}; Θ_{2}; ⊆; ⊆; ⊥; ⊢ p:; ⊆; ⊆; ⊥; ⊢ p:; ⊢ p:]

Proof : If θ̂_{1} is empty, take Θ_{1} to be empty and Θ_{2} to be Θ. If θ̂_{2} is empty, take Θ_{2} to be empty and Θ_{1} to be Θ. If θ̂_{1} and θ̂_{2} are passive, take ϕ̂ to be θ̂_{1} ∪ θ̂_{2}, use Proposition 13b, and then take both Θ_{1} and Θ_{2} to be Φ. (End of Proof )

With these preliminaries, we can prove the basic relationship between typings and substitutions. We write (p_{1}/ι → p_{2}) to denote the result of substituting p_{2} for the free occurrences of ι in p_{1}, with renaming to avoid identifier collisions.

Proposition 15 If [ Θ_{1} | ι: θ̂] ⊢ p_{1} : θ, Θ_{2} ⊢ p_{2} : θ̂, and Θ_{1} and Θ_{2} are subsets of Θ such that Θ_{1} ⊥ Θ_{2}, then Θ ⊢ (p_{1}/ι → p_{2}) : θ.

Proof : By induction on the proof size of [ Θ_{1} | ι: θ̂] ⊢ p_{1} : θ.

(1) If the proof root is the rule for identifiers, then p_{1} is an identifier ι′ and θ ^{∈} [ Θ_{1} | ι: θ̂]ι′. If ι′ = ι then θ ^{∈} θ̂ and (p_{1}/ι → p_{2}) = p_{2}, so that Θ_{2} ⊢ p_{2} : θ̂ gives Θ_{2} ⊢ (p_{1}/ι → p_{2}) : θ and, since Θ_{2} ⊆ Θ implies Θ ≤ Θ_{2}, Proposition 12 gives Θ ⊢ (p_{1}/ι → p_{2}) : θ. On the other hand, if ι′ ≠ ι then θ ^{∈} Θ_{1}ι′ and (p_{1}/ι → p_{2}) = ι′, so that Θ_{1} ⊢ (p_{1}/ι → p_{2}) : θ and, since Θ_{1} ⊆ Θ implies Θ ≤ Θ_{1}, Proposition 12 gives Θ ⊢ (p_{1}/ι → p_{2}) : θ.

(2) If the proof root is a normal rule, then p_{1} must have the form ε(p_{11}, …, p_{1n}), which is constructed from p_{11}, …, p_{1n} without using binding operators, and the premisses of the rule must have the form

[ Θ_{1} | ι: θ̂] ⊢ p_{11} : θ̂_{1}  …  [ Θ_{1} | ι: θ̂] ⊢ p_{1n} : θ̂_{n} .

By the induction hypothesis (applied to each member of each θ̂_{i}),

Θ ⊢ (p_{11}/ι → p_{2}) : θ̂_{1}  …  Θ ⊢ (p_{1n}/ι → p_{2}) : θ̂_{n} ,

and by the rule at the root,

Θ ⊢ ε((p_{11}/ι → p_{2}), …, (p_{1n}/ι → p_{2})) : θ .

But since ε is constructed without binding operators,

ε((p_{11}/ι → p_{2}), …, (p_{1n}/ι → p_{2})) = (ε(p_{11}, …, p_{1n})/ι → p_{2}) = (p_{1}/ι → p_{2}) .

(3) If the proof root is a noninterference rule, then p_{1} must have the form ε(p_{11}, p_{12}), which is constructed from p_{11} and p_{12} without using binding operators, and the premisses of the rule must have the forms

[ Θ_{11} | ι: θ̂_{1} ] ⊢ p_{11} : θ̂′_{1} and [ Θ_{12} | ι: θ̂_{2} ] ⊢ p_{12} : θ̂′_{2} ,

where

Θ_{11} ⊆ Θ_{1} Θ_{12} ⊆ Θ_{1} Θ_{11} ⊥ Θ_{12}
θ̂_{1} ⊆ θ̂ θ̂_{2} ⊆ θ̂ θ̂_{1} ⊥ θ̂_{2} .

Then, since Θ_{2} ⊢ p_{2} : θ̂, Proposition 14 shows that there are Θ_{21} and Θ_{22} such that

Θ_{21} ⊆ Θ_{2} Θ_{22} ⊆ Θ_{2} Θ_{21} ⊥ Θ_{22}
Θ_{21} ⊢ p_{2} : θ̂_{1} Θ_{22} ⊢ p_{2} : θ̂_{2} .

Since Θ_{1} ⊥ Θ_{2}, Proposition 9 gives

Θ_{11} ⊥ Θ_{21} Θ_{12} ⊥ Θ_{22} Θ_{11} ⊥ Θ_{22} Θ_{12} ⊥ Θ_{21} .

Then the induction hypothesis (applied to each member of θ̂′_{1} and θ̂′_{2}) gives

Θ_{11} ∪ Θ_{21} ⊢ (p_{11}/ι → p_{2}) : θ̂′_{1} Θ_{12} ∪ Θ_{22} ⊢ (p_{12}/ι → p_{2}) : θ̂′_{2} .

By Proposition 10, (Θ_{11} ∪ Θ_{21}) ⊥ (Θ_{12} ∪ Θ_{22}). Thus the rule used at the root gives

Θ ⊢ ε((p_{11}/ι → p_{2}), (p_{12}/ι → p_{2})) : θ ,

or, since ε is constructed without binding operators,

Θ ⊢ (p_{1}/ι → p_{2}) : θ .

(4) If the proof root is the first abstraction rule, then its instance must have the form

\frac{[ [ Φ_{1} | ι: ϕ̂] | ι′: θ̂′] ⊢ p′_{1} : θ′}{[ Θ_{1} | ι: θ̂] ⊢ (λι′: θ̂_{0}. p′_{1}) : θ̂′ ⟶_{P} θ′}

where θ̂′ ⊆ θ̂_{0}, Φ_{1} ⊆ Θ_{1} is passive, and ϕ̂ ⊆ θ̂ is passive. Moreover, since renaming obviously preserves typings, we can assume without loss of generality that ι′ is distinct from ι and does not occur free in p_{2}, and thus that Θ_{2} maps ι′ into the empty set.

Since ϕ̂ is a passive subset of θ̂ and Θ_{2} ⊢ p_{2} : θ̂, by Proposition 13b there is a passive Φ_{2} ⊆ Θ_{2} such that Φ_{2} ⊢ p_{2} : ϕ̂. Since ι′ ≠ ι, the premiss of the abstraction rule instance can be rewritten as

[ [ Φ_{1} | ι′: θ̂′] | ι: ϕ̂] ⊢ p′_{1} : θ′ ,

and since Φ_{2}ι′ is empty and Φ_{1} and Φ_{2} are passive,

[ Φ_{1} | ι′: θ̂′] ⊥ Φ_{2} and [ Φ_{1} | ι′: θ̂′] ∪ Φ_{2} = [ Φ_{1} ∪ Φ_{2} | ι′: θ̂′] .

Thus the induction hypothesis gives

[ Φ_{1} ∪ Φ_{2} | ι′: θ̂′] ⊢ (p′_{1}/ι → p_{2}) : θ′ ,

and, since Φ_{1} ∪ Φ_{2} is a passive subset of Θ, the first abstraction rule gives

Θ ⊢ (λι′: θ̂_{0}. (p′_{1}/ι → p_{2})) : θ̂′ ⟶_{P} θ′ .

Finally, since ι′ is distinct from ι and does not occur free in p_{2},

((λι′: θ̂_{0}. p′_{1})/ι → p_{2}) = λι′: θ̂_{0}. (p′_{1}/ι → p_{2}) .

The simpler case of the second abstraction rule is left to the reader. (End of Proof )

Notice, however, that the converse of Proposition 15 does not hold. For example, suppose

p_{1} is (x.a)(x.b)
p_{2} is ⟨a ≡ y, b ≡ z⟩
ι is x
Θ is [ y: {{comm} ⟶ comm} | z: {comm}]
θ is comm

Then Θ ⊢ (p_{1}/ι → p_{2}) : θ is

[ y: {{comm} ⟶ comm} | z: {comm}] ⊢ (⟨a ≡ y, b ≡ z⟩.a)(⟨a ≡ y, b ≡ z⟩.b) : comm ,

which is a valid typing. However, there are no Θ_{1}, Θ_{2} ⊆ Θ and θ̂ such that

[ Θ_{1} | x: θ̂] ⊢ (x.a)(x.b) : comm

Θ_{2} ⊢ ⟨a ≡ y, b ≡ z⟩ : θ̂ ,

since the second typing requires every member of θ̂ to be either b: comm or a: θ̂′ ⟶ comm where comm ^{∈} θ̂′, which makes the first typing impossible.

From Proposition 15, the reader may verify that beta reduction preserves typings:

Proposition 16 If Θ ⊢ (λι: θ̂_{0}. p_{1})p_{2} : θ then Θ ⊢ (p_{1}/ι → p_{2}) : θ.

The reader may also verify that the reduction of tuples, and its inverse, preserves typings:

Proposition 17 Θ ⊢ ⟨ι_{1} ≡ p_{1}, …, ι_{k} ≡ p_{k}, …, ι_{n} ≡ p_{n}⟩.ι_{k} : θ iff Θ ⊢ p_{k} : θ.

5. Typechecking

To show that the typings defined in the previous section can be checked, we define a computable typechecking function Ψ, which accepts a type assignment and a phrase. Essentially Ψ(Θ_{0}, p) produces a finite set θ̂ of types such that Θ_{0} ⊢ p : θ holds if and only if there is a member of θ̂ that is a subtype of θ. However, Ψ(Θ_{0}, p) also produces additional information: the θ ^{∈} θ̂ are paired with type assignments Θ ⊆ Θ_{0} that are just sufficient to give Θ ⊢ p : θ. Thus Ψ(Θ_{0}, p) is a set of pairs, each consisting of a type assignment and a type. This function is defined by induction on the structure of phrases:

Ψ(Θ_{0}, ι) = { ⟨[ ι: {θ}], θ⟩ | θ ^{∈} Θ_{0}ι }
Ψ(Θ_{0}, λι: θ̂_{0}. p) =

{ ⟨Θ, θ̂ ⟶_{P} θ⟩ | ⟨[ Θ | ι: θ̂], θ⟩ ^{∈} Ψ([ Θ_{0} | ι: θ̂_{0} ], p) and Θι = {} and Θ passive } ∪

{ ⟨Θ, θ̂ ⟶ θ⟩ | ⟨[ Θ | ι: θ̂], θ⟩ ^{∈} Ψ([ Θ_{0} | ι: θ̂_{0} ], p) and Θι = {} and Θ not passive }

Ψ(Θ_{0}, p_{1}p_{2}) = { ⟨Θ_{1} ∪ Θ_{2}, θ⟩ | Θ_{1} ⊥ Θ_{2} and

(∃θ̂) ((⟨Θ_{1}, θ̂ ⟶_{P} θ⟩ ^{∈} Ψ(Θ_{0}, p_{1}) or ⟨Θ_{1}, θ̂ ⟶ θ⟩ ^{∈} Ψ(Θ_{0}, p_{1})) and

(∃η ^{∈} θ̂ ⇒ Ψ(Θ_{0}, p_{2})) (Θ_{2} = ⋃_{θ′^{∈}θ̂}[ηθ′]_{1} and (∀θ′ ^{∈} θ̂) [ηθ′]_{2} ≤ θ′)) }

Ψ(Θ_{0}, ⟨ι_{1} ≡ p_{1}, …, ι_{n} ≡ p_{n}⟩) = ⋃_{k=1}^{n}{ ⟨Θ, ι_{k}: θ⟩ | ⟨Θ, θ⟩ ^{∈} Ψ(Θ_{0}, p_{k}) }

Ψ(Θ_{0}, p.ι) = { ⟨Θ, θ⟩ | ⟨Θ, ι: θ⟩ ^{∈} Ψ(Θ_{0}, p) }

Ψ(Θ_{0}, if p_{1} then p_{2} else p_{3}) =

{ ⟨Θ_{1} ∪ Θ_{2} ∪ Θ_{3}, θ⟩ | (∃θ_{1}, θ_{2}, θ_{3}) θ_{1} ≤ bool exp and θ ^{∈} θ_{2} ˙⊔ θ_{3} and
⟨Θ_{1}, θ_{1}⟩ ^{∈} Ψ(Θ_{0}, p_{1}) and ⟨Θ_{2}, θ_{2}⟩ ^{∈} Ψ(Θ_{0}, p_{2}) and ⟨Θ_{3}, θ_{3}⟩ ^{∈} Ψ(Θ_{0}, p_{3}) }

Ψ(Θ_{0}, 0) = {⟨[ ], int exp⟩}

Ψ(Θ_{0}, 0.5) = {⟨[ ], real exp⟩}

Ψ(Θ_{0}, p_{1} + p_{2}) = { ⟨Θ_{1} ∪ Θ_{2}, int exp⟩ | (∃θ_{1}, θ_{2}) θ_{1} ≤ int exp and θ_{2} ≤ int exp and

⟨Θ_{1}, θ_{1}⟩ ^{∈} Ψ(Θ_{0}, p_{1}) and ⟨Θ_{2}, θ_{2}⟩ ^{∈} Ψ(Θ_{0}, p_{2}) } ∪
{ ⟨Θ_{1} ∪ Θ_{2}, real exp⟩ | (∃θ_{1}, θ_{2}) θ_{1} ≤ real exp and θ_{2} ≤ real exp and
⟨Θ_{1}, θ_{1}⟩ ^{∈} Ψ(Θ_{0}, p_{1}) and ⟨Θ_{2}, θ_{2}⟩ ^{∈} Ψ(Θ_{0}, p_{2}) }

Ψ(Θ_{0}, p_{1} := p_{2}) = { ⟨Θ_{1} ∪ Θ_{2}, comm⟩ | (∃θ_{1}, θ_{2}, δ) θ_{1} ≤ δ acc and θ_{2} ≤ δ exp and

⟨Θ_{1}, θ_{1}⟩ ^{∈} Ψ(Θ_{0}, p_{1}) and ⟨Θ_{2}, θ_{2}⟩ ^{∈} Ψ(Θ_{0}, p_{2}) }

Ψ(Θ_{0}, p_{1} ; p_{2}) = { ⟨Θ_{1} ∪ Θ_{2}, comm⟩ | (∃θ_{1}, θ_{2}) θ_{1} ≤ comm and θ_{2} ≤ comm and

⟨Θ_{1}, θ_{1}⟩ ^{∈} Ψ(Θ_{0}, p_{1}) and ⟨Θ_{2}, θ_{2}⟩ ^{∈} Ψ(Θ_{0}, p_{2}) }

Ψ(Θ_{0}, while p_{1} do p_{2}) = { ⟨Θ_{1} ∪ Θ_{2}, comm⟩ | (∃θ_{1}, θ_{2}) θ_{1} ≤ bool exp and θ_{2} ≤ comm and

⟨Θ_{1}, θ_{1}⟩ ^{∈} Ψ(Θ_{0}, p_{1}) and ⟨Θ_{2}, θ_{2}⟩ ^{∈} Ψ(Θ_{0}, p_{2}) }

Ψ(Θ_{0}, p_{1} ∥ p_{2}) = { ⟨Θ_{1} ∪ Θ_{2}, comm⟩ | Θ_{1} ⊥ Θ_{2} and (∃θ_{1}, θ_{2}) θ_{1} ≤ comm and θ_{2} ≤ comm and

⟨Θ_{1}, θ_{1}⟩ ^{∈} Ψ(Θ_{0}, p_{1}) and ⟨Θ_{2}, θ_{2}⟩ ^{∈} Ψ(Θ_{0}, p_{2}) }

In the equation for Ψ(Θ_{0}, p_{1}p_{2}), the expression θ̂ ⇒ Ψ(Θ_{0}, p_{2}) denotes the finite set of all functions from θ̂ to Ψ(Θ_{0}, p_{2}), and [ηθ′]_{1} and [ηθ′]_{2} denote the first and second components of the pair ηθ′.

This typechecking function meets the following specification:

Proposition 18 (a) If ⟨Θ, θ⟩ ^{∈} Ψ(Θ_{0}, p) then Θ ⊆ Θ_{0} and Θ ⊢ p : θ and if θ is passive then Θ is passive.

(b) If Θ ⊆ Θ_{0} and Θ ⊢ p : θ then (∃⟨Θ′, θ′⟩ ^{∈} Ψ(Θ_{0}, p)) Θ′ ⊆ Θ and θ′ ≤ θ.

Proof : (a) By induction on the structure of p. We give the details of the case where p is an application p_{1}p_{2}, and leave the tedium of the remaining cases to the reader.

Suppose ⟨Θ, θ⟩ ^{∈} Ψ(Θ_{0}, p_{1}p_{2}). By the definition of Ψ, there are Θ_{1}, Θ_{2}, and θ̂ such that Θ = Θ_{1} ∪ Θ_{2}, Θ_{1} ⊥ Θ_{2}, and either ⟨Θ_{1}, θ̂ ⟶_{P} θ⟩ or ⟨Θ_{1}, θ̂ ⟶ θ⟩ belongs to Ψ(Θ_{0}, p_{1}). Also, there is a function η from θ̂ to Ψ(Θ_{0}, p_{2}) such that

Θ_{2} = ⋃_{θ′^{∈}θ̂}[ηθ′]_{1} and (∀θ′ ^{∈} θ̂) [ηθ′]_{2} ≤ θ′ .

For each θ′ ^{∈} θ̂, since ηθ′ ^{∈} Ψ(Θ_{0}, p_{2}), the induction hypothesis for p_{2} gives [ηθ′]_{1} ⊆ Θ_{0} and [ηθ′]_{1} ⊢ p_{2} : [ηθ′]_{2} and if [ηθ′]_{2} is passive then [ηθ′]_{1} is passive. Then, since [ηθ′]_{2} ≤ θ′, we have [ηθ′]_{1} ⊢ p_{2} : θ′ and, by Proposition 1, if θ′ is passive then [ηθ′]_{1} is passive. Thus, since Θ_{2} is the union of [ηθ′]_{1} over θ′ ^{∈} θ̂, we have Θ_{2} ⊆ Θ_{0} and Θ_{2} ⊢ p_{2} : θ̂ and if θ̂ is passive then Θ_{2} is passive.

By the induction hypothesis for p_{1}, we have Θ_{1} ⊆ Θ_{0} and either Θ_{1} ⊢ p_{1} : θ̂ ⟶_{P} θ and Θ_{1} is passive (since θ̂ ⟶_{P} θ is passive) or Θ_{1} ⊢ p_{1} : θ̂ ⟶ θ. Thus Θ = Θ_{1} ∪ Θ_{2} ⊆ Θ_{0} and, by the inference rules for application, Θ ⊢ p_{1}p_{2} : θ. Moreover, if θ is passive then our restrictions on procedural types prohibit the type θ̂ ⟶ θ and insure that θ̂ is passive, so that Θ_{1} and Θ_{2}, and thus Θ, are passive.

(b) By induction on the proof size of Θ ⊢ p : θ. We give the details of the case where the proof root is an application rule, and leave the remaining cases to the reader.

Suppose Θ ⊆ Θ_{0} and the root of the proof of Θ ⊢ p : θ is one of the inference rules for application. Then p = p_{1}p_{2}, either Θ_{1} ⊢ p_{1} : θ̂ ⟶_{P} θ or Θ_{1} ⊢ p_{1} : θ̂ ⟶ θ, and Θ_{2} ⊢ p_{2} : θ̂, where Θ_{1} and Θ_{2} are subsets of Θ such that Θ_{1} ⊥ Θ_{2}. By the induction hypothesis for p_{1} and the definition of ≤ for procedural types, there are Θ′_{1}, θ̂′, and θ′ such that either

⟨Θ′_{1}, θ̂′ ⟶_{P} θ′⟩ or ⟨Θ′_{1}, θ̂′ ⟶ θ′⟩ belong to Ψ(Θ_{0}, p_{1}), Θ′_{1} ⊆ Θ_{1}, θ̂ ≤ θ̂′, and θ′ ≤ θ.

Since θ̂ ≤ θ̂′, for any θ′′ ^{∈} θ̂′ there will be a θ̄^{∈} θ̂ such that θ̄ ≤ θ′′ and, since Θ_{2} ⊢ p_{2} : θ̂, Θ_{2} ⊢ p_{2} : θ̄. Then by the induction hypothesis for p_{2} there is a ⟨Θ̄′, θ̄′⟩ ^{∈} Ψ(Θ_{0}, p_{2}) such that Θ̄′ ⊆ Θ_{2} and θ̄′ ≤ θ̄. Let η be a function mapping each θ′′ ^{∈} θ̂′ into such a pair ⟨Θ̄′, θ̄′⟩. Then η is a function from θ̂′ to Ψ(Θ_{0}, p_{2}) such that [ηθ′′]_{1} ⊆ Θ_{2} and [ηθ′′]_{2} ≤ θ′′ hold for all θ′′ ^{∈} θ̂′. Let Θ′_{2} = ⋃_{θ′′^{∈}θ̂′}[ηθ′′]_{1}, so that Θ′_{2} ⊆ Θ_{2}.

Since Θ′_{1} ⊆ Θ_{1}, Θ′_{2} ⊆ Θ_{2}, and Θ_{1} ⊥ Θ_{2}, we have Θ′_{1} ⊥ Θ′_{2} by Proposition 9. This completes the conditions needed to show that, by the definition of Ψ,

⟨Θ′_{1} ∪ Θ′_{2}, θ′⟩ ^{∈} Ψ(Θ_{0}, p_{1}p_{2})

and also Θ′_{1} ∪ Θ′_{2} ⊆ Θ and θ′ ≤ θ. (End of Proof )

To illustrate type checking, we consider a example that is similar to one of the problematic examples at the end of [7]. Suppose [ n: {int exp}] ⊆ Θ_{0}. Then

⟨[ n: {int exp}], int exp⟩ ^{∈} Ψ(Θ_{0}, n)
⟨[ n: {int exp}], int exp⟩ ^{∈} Ψ(Θ_{0}, n + 1)
⟨[ n: {int exp}], a: int exp⟩ ^{∈} Ψ(Θ_{0}, ⟨a ≡ n + 1, b ≡ ⋯⟩)
⟨[ n: {int exp}], int exp⟩ ^{∈} Ψ(Θ_{0}, ⟨a ≡ n + 1, b ≡ ⋯⟩.a) ,

where ⋯ can be any phrase, even one that has no typing. Moreover, if we abstract on any identifier other than n, we get

⟨[ n: {int exp}], {} ⟶_{P} int exp⟩ ^{∈} Ψ(Θ_{0}, λc: · · · . ⟨a ≡ n + 1, b ≡ ⋯⟩.a)

⟨[ n: {int exp}], int exp⟩ ^{∈} Ψ(Θ_{0}, (λc: · · · . ⟨a ≡ n + 1, b ≡ ⋯⟩.a)(⋯)) .

Thus each term of the reduction sequence

(λc: · · · . ⟨a ≡ n + 1, b ≡ ⋯⟩.a)(⋯) ⟹ ⟨a ≡ n + 1, b ≡ ⋯⟩.a ⟹ n + 1

takes on the type int exp under any type assignment containing [ n: {int exp}].

6. The Remaining Problems

Beyond the progress reported here, much remains to be done:

• The efficiency of the typechecking algorithm needs to be understood and, if possible, improved.

• There is need for an alternative form of procedure that can interfere with its argument. Such a construct seems to be necessary to define active procedures recursively (as can be seen by considering the right side of the fixed-point equation Y f = f(Y f) when f is active). Another motivation is the desire to regard assignment as a procedure call (as in [6]), so that x := x + 1 becomes an abbreviation for x(x + 1). We speculate that such procedures might be obtained by abstracting on qualified identifiers (e.g. on x.a rather than simply x).

• A substantial generalization is needed to deal with goto’s, escapes, or other operations that require continuation semantics.

• A semantic model is needed that will make it evident that distinct identifiers possess noninterfering meanings.

Despite these problems, however, the present work illustrates the utility of conjunctive types. It seems possible that their application to the syntactic control of interference may generalize to the syntactic treatment of a variety of program properties.

Acknowledgements The author wishes to thank Bob Tennent and Steve Brookes for their encouragement, and Mary and Edward Reynolds for their patience.

References

[1] Brinch Hansen, P. Structured Multiprogramming. Communications of the ACM, vol. 15 (1972), pp. 574–578.

[2] Coppo, M., Dezani-Ciancaglini, M., and Venneri, B. Functional Characters of Solvable Terms. Zeitschrift für Mathematische Logik und Grundlagen der Mathematik, vol. 27 (1981), pp. 45–58.

[3] Hoare, C. A. R. Monitors: An Operating System Structuring Concept. Communications of the ACM, vol. 17 (1974), pp. 549–557. Corrigendum in (2) 18, February 1975, p. 95.

[4] Hoare, C. A. R. Towards a Theory of Parallel Programming. in: Operating Systems Techniques, Proceedings of a Seminar, Queen’s University, Belfast, August 30– September 3, 1971, edited by C. A. R. Hoare and R. H. Perrott. A.P.I.C. Studies in Data Processing, vol. 9, Academic Press, London, 1972, pp. 61–71.

[5] Reynolds, J. C. The Essence of Algol. in: Algorithmic Languages, Proceedings of the International Symposium on Algorithmic Languages, Amsterdam, October 26–29, edited by J. W. de Bakker and J. C. van Vliet. North-Holland, Amsterdam, 1981, pp. 345–372.

[6] Reynolds, J. C. Preliminary Design of the Programming Language Forsythe. Report, no. CMU–CS–88–159, Carnegie Mellon University, Computer Science Department, June 21, 1988.

[7] Reynolds, J. C. Syntactic Control of Interference. in: Conference Record of the Fifth Annual ACM Symposium on Principles of Programming Languages, Tucson, Arizona, January 23–25. 1978, pp. 39–46.