Principals in Programming Languages: Technical Results

Steve Zdancewic Dan Grossman ^{∗} Cornell University

June 16, 1999

Abstract

This is the companion technical report for “Principals in Programming Languages” [20]. See that document for a more readable version of these results.

In this paper, we describe two variants of the simply typed λ-calculus extended with a notion of principal. The results are languages in which intuitive statements like “the client must call open to obtain a file handle” can be phrased and proven formally.

The first language is a two-agent calculus with references and recursive types, while the second language explores the possibility of multiple agents with varying amounts of type information. We use these calculi to give syntactic proofs of some type abstraction results that traditionally require semantic arguments.

1 Introduction

Programmers often have a notion of principal in mind when designing the structure of a program. Examples of such principals include modules of a large system, a host and its clients, and, in the extreme, individual functions. Dividing code into such agents is useful for composing programs. Moreover, with the increasing use of extensible systems, such as web browsers, databases [6], and operating systems [7, 3, 2], this notion of principal becomes critical for reasoning about potentially untrusted agents interfacing with host-provided code.

In this paper, we incorporate the idea of principal into variants of the simply-typed λ-calculus. Doing so allows us to formalize statements about agent interaction. For instance, a client must call open to obtain a file handle. As a motivating example, we consider the problem of type abstraction in extensible systems.

Consider a host-provided interface for an abstract type of file handles, fh, and operations to create and use them:

(* File handle implemented as int *)
abstype fh

open : string → fh read : fh → int

The principals in this scenario are the host implementation of the interface and its clients. Each principal’s “view of the world” corresponds to its knowledge regarding fh. In particular, the host knows that fh = int, while clients do not.

The conventional wisdom is that using abstract datatypes in a type-safe language prevents agents from directly accessing host data. Instead, a client may only manipulate such data via a host-provided interface. To formalize this wisdom, it is necessary to prove theorems that say, “agent code can not violate type abstractions provided by the host”. For instance, a client should not be able to treat an object of type fh as though it were an integer, even though the host implements it that way.

∗This material is based on work supported in part by the AFOSR grant F49620-97-1-0013, ARPA/RADC grant F30602-1-0317, and National Science Foundation Graduate Fellowships. Any opinions, findings, and conclusions or recommendations expressed in this publication are those of the authors and do not reflect the views of these agencies.

How do we prove such properties? One way of phrasing the result is to say that the agent behaves parametrically with respect to the type fh. Using this observation, we can encode the agent program in a language like Girard’s System F [5], the polymorphic λ-calculus [16]:

Λfh.λhost : {open : string → fh, read : fh → int}.agent code

Here, the type fh is held abstract by encoding the agent as a polymorphic function. We can then appeal to Reynolds’ parametricity results [17] to conclude that the agent respects the host’s interface.

Unfortunately, these representation independence results are proven using semantic arguments based on a model of the language (see Mitchell’s work [11], for example). We are unaware of any similar results for languages including multiple features of modern languages, such as references, recursive types, objects, threads, and control operators.

Our calculus circumvents this problem by syntactically distinguishing between agents with different type information. We do this by “coloring” host code and client code with different colors and tracking how these colors intermingle during evaluation. By using different semantics for each principal, we force the client to respect the abstract types provided by the host. This separation of principals provides hooks that enable us to prove some type abstraction properties syntactically.

To see why these new mechanisms are useful, consider the evaluation of our agent code when “linked” against a host implementation:

(Λfh.λhost : τ_{h}.agent code) int host code ⟼ (λhost : {int/fh}τ_{h}.{int/fh}agent code) host code ⟼ {host code/host}{int/fh}agent code

Where τ_{h} = {open : string → fh, read : fh → int}. In this scheme, linking is encoded as application. In one step of the standard operational semantics, the host-type is substituted throughout the agent code. It is impossible to talk about the type fh remaining abstract within the client because fh is replaced by int. After a second step, host code is substituted throughout agent code and all distinctions between principals are lost.

The next section describes a two-agent setting including recursive types and state sufficient for proving interesting properties about the file handle example. Detailed proofs of soundness and some abstraction properties are shown. Section 3 introduces a multiagent calculus without mutable references which provides for multiple agents and abstract types. We then revisit the safety properties and language extensions of Section 2. The final sections conclude with related work and other potential uses for principals in programming languages.

2 The Two-agent Language

2.1 Syntax

This section describes a variant of the simply-typed λ-calculus with two principals, an agent and a host. The language maintains a syntactic distinction between host and agent code throughout evaluation. The host exports one abstract type, t, implemented as type τ_{h}.

Figure 1 gives the syntax for the two-agent calculus. Types, τ, include a base type (b), the host’s abstract type (t), function types, reference types, μ-type variables (α), and recursive types. The terms of the language are agent terms (A), agent values (Â), host terms (H), and host values (Ĥ). The metavariable x_{a} ranges over agent variables which are disjoint from host variables, ranged over by x_{h}. The metavariable c ranges over values of base type.

Heap labels (ξ^{τ}), like constants, are not “owned” by either the agent or the host. They are, however, labeled with the type of the value referred to by the label. The level of abstraction of a given reference is decided when the reference is created. This means that the host must decide a priori whether a reference to a value of type τ_{h} should be abstract. A reference of type τ_{h} ref can never alias a reference of type t ref.

It is helpful to think of terms generated by A and H as having different colors (indicated by the subscripts a and h respectively) that indicate to which principal each belongs. As observed in the introduction, agent

τ ::= t | b | τ → τ′ | τ ref

| α | μα.τ

A ::= x_{a} | c | ξ^{τ} | λx_{a}:τ. A | A A′ |

ref_{τ} A | !A | A:= A′ |

roll_{μα.τ} A | unroll_{μα.τ} A | ⌜⌞H⌝⌟_{h}^{τ}

Â ::= c | λx_{a}:τ. A | ξ^{τ} | | roll_{μα.τ} Â |

⌜⌞Ĥ⌝⌟t_{h}

H ::= x_{h} | c | ξ^{τ} | λx_{h}:τ. H | H H′ |

ref_{τ} H | !H | H:= H′ |

roll_{μα.τ} H | unroll_{μα.τ} H | ⌜⌞A⌝⌟_{a}^{τ}

Ĥ ::= c | λx_{h}:τ. H | ξ^{τ} | roll_{μα.τ} Ĥ

Figure 1: Two-agent Syntax

and host terms mix during evaluation. To keep track of this intermingling, agent terms contain embedded host terms of the form ⌜⌞H⌝⌟_{h}^{τ}. Intuitively, the brackets delimit a piece of h-colored code, where H is exported to the agent at type τ. Dually, host terms may contain embedded agents.

The type annotations on the embeddings keep track of values of type t during execution. In particular, a host term of type τ_{h} may be embedded in an agent term. If the annotation is t, then the agent has no information about the form of the term inside the embedding. Thus, an embedding with annotation t containing a host value is an agent value.

In order to keep track of the host’s extra information about the type t, we introduce an operation Δ_{h} that converts a type τ with possible occurrences of t to a “concrete” view seen by the host. This operation essentially substitutes τ_{h} for t in τ except under references. The definition of Δ_{h} is:

Δ_{h}(b) = b
Δ_{h}(t) = τ_{h}
Δ_{h}(τ → τ′) = Δ_{h}(τ) → Δ_{h}(τ′)
Δ_{h}(μα.τ) = μα.Δ_{h}(τ)
Δ_{h}(τ ref) = τ ref

2.2 Notation

Before describing the semantics, we define some convenient notions. Let e range over both agent and host terms, and let ê range over both agent and host values. The color of e is a if e is an A term; otherwise e’s color is h. Note that both terms in a syntactically correct application are the same color. Since the host and agent terms share some semantic rules, we use polychromatic rules to range over both agent and host terms. The intention is that all terms mentioned in them have the same color –hence the term polychromatic. Such rules can be thought of as short-hand for two analogous rules, one for each color.

We use κ to range over colors and write κ^{∘} for the opposite color, so that a^{∘} = h and h^{∘} = a. Where the color of a variable or typing judgment is clear from context or unimportant, we drop the subscript κ to simplify presentation.

We write {e′/x_{κ}}e for the capture-avoiding substitution of e′ for x_{κ} in e. Note that substitution crosses embeddings. Terms are equal up to α-conversion, where substituted variables are of the same color.

2.3 Two-agent Dynamic Semantics

We model the heap (memory) as a partial function M : Labels → V alues × Agents such that if M is defined on ξ^{τ}, M(ξ^{τ}) = (ê, κ) for some value ê of color κ. The static semantics ensure that type annotations on labels agree with the value in the heap. The heap may contain self-referential data structures.

Figure 2 describes a small-step operational semantics for the two-agent calculus. The transitions are of the form (M, e) ⟼ (M′, e′), indicating that in the configuration where the heap has shape M, the term e steps in one step to e′, possibly updating the heap to M′. The first three polychromatic rules establish a callby-value semantics, while (Pμ3) makes unroll the left inverse of roll. The remainder of the polychromatic rules allow evaluation to continue when the immediate subterms are not values.

The host and agent dynamic rules, described next, either propagate embeddings in an appropriate fashion, or mediate access to the heap.

Rules (AH) and (HA) allow evaluation to proceed within embeddings. Inside embeddings, the rules for the opposite color apply. These “context switches” ensure that terms evaluate in the appropriate context for their color. If an embedded value is exported to the outer principal at type b, the outer agent can strip away the embedding and use that value (rules (AConst) and (HConst)).

Rules (AHfn) and (HAfn) maintain the distinction between agent and host code. For example, suppose the agent contains a host function that is being exported at type τ^{1} → τ^{2}. In this case the agent does know that the embedding contains a function, so the agent can apply it to an argument of a suitable type. If instead the function had been exported at type t, the agent would not have been able to apply it. The subtlety is that the host type of the function may be more specific than the agent type, such as when τ^{1} = t.

Thus, (AHfn) converts an embedded host function to an agent function with argument of type τ. The body of the agent function is an embedding of the host code, except that, as the argument now comes from the agent, every occurrence of the original argument variable, x_{h}, is replaced by an embedding of the agent’s argument variable, ⌜⌞x_{a}⌝⌟_{a}^{τ}. This embedding is exported to the host at type τ, the type the host originally expected for the function argument. The rule for hosts, (HAfn), is symmetric, except that because the host may use t as τ_{h}, the type of the argument is refined by applying Δ_{h}.

The rule (HStrip) lets the host “open up” an agent value that is really an embedded host value. This allows the host to use a value that has been embedded abstractly in the agent.

The rules (Aμ) and (Hμ), propagate the embeddings through roll terms when the annotations on the embedding make this permissible. As with the function annotations, the host rule refines the type.

The agent creates new heap labels using rule (ARef). When the agent dereferences a host’s heap entry, (A!), the result depends on the last agent to store to that location. If it was the agent, dereferencing returns the stored value. If the host last wrote to the memory, the contents are returned as an embedded host value. The level of abstraction is determined by the type annotation on the heap label. This allows the host to export references to the agent at more abstract types such that dereference preserves the abstraction. Assignment of an agent value to a location, (AAssn), also marks that heap entry with that agent’s color. The rule (ALab) is similar to (HStrip) in that the agent pulls out an agent label from within nested embeddings. Note that the type annotation on the label is forced by the static semantics to be the same as the annotation on the embedding–in effect, the host and agent must agree about the type of references, even if the host knows more.

The host versions of the rules for creating labels and manipulating references are similar.

The crucial point is that any attempt by the agent to treat a value of type t as a function, reference, or constant will lead to a stuck configuration (no rule will apply). More generally, we ensure that any configuration in which an abstract value appears in an “active position” is stuck. This fact, along with the stuck configurations of the simply-typed λ-calculus, is enough to prove the safety properties of Section 2.5.

2.4 Two-agent Static Semantics

Figure 3 describes the static semantics for the two-agent calculus. In the type well-formedness rules, Ξ is a set of μ-type variables currently in scope. The judgment Ξ ⊢ τ istype indicates that τ is a well-formed type with free variables in Ξ. Implicit in the heap well-formedness and term typing judgments are antecedents ∅ ⊢ τ istype for the types mentioned in the rule.

A heap-type, Ψ, is a set of labels describing M. We think of Ψ as a mapping from labels to their types: Ψ(ξ^{τ}) = τ. The judgment ⊢ M : Ψ says that the heap, M, is well-formed with type Ψ. The rule (HAlab)

Polychrome Steps

(P1)  (M, e_{1} e_{2}) ⟼ (M′, e′_{1} e_{2})  if (M, e_{1}) ⟼ (M′, e′_{1})
(P2)  (M, ê e) ⟼ (M′, ê e′)  if (M, e) ⟼ (M′, e′)
(Pβ)  (M, (λx:τ. e) ê) ⟼ (M, {ê/x}e)
(Pμ1) (M, roll_{τ} e) ⟼ (M′, roll_{τ} e′) if (M, e) ⟼ (M′, e′)
(Pμ2)  (M, unroll_{τ} e) ⟼ (M′, unroll_{τ} e′) if (M, e) ⟼ (M′, e′)
(Pμ3) (M, unroll_{μα.τ} roll_{μα.τ} ê) ⟼ (M, ê)
(P!)  (M, !e) ⟼ (M′, !e′)  if (M, e) ⟼ (M′, e′)
(PRef1)  (M, ref_{τ} e) ⟼ (M′, ref_{τ} e′)  if (M, e) ⟼ (M′, e′)
(PAssn1)  (M, e_{1} := e_{2}) ⟼ (M′, e′_{1} := e_{2})  if (M, e_{1}) ⟼ (M′, e′_{1})
(PAssn2)  (M, ê:= e_{2}) ⟼ (M′, ê:= e′_{2})  if (M, e_{2}) ⟼ (M′, e′_{2})

Agent Steps

(AH) (M, ⌜⌞H⌝⌟_{h}^{τ}) ⟼ (M′, ⌜⌞H′⌝⌟_{h}^{τ}) if (M, H) ⟼ (M′, H′)
(AConst)  (M, ⌜⌞c⌝⌟b_{h}) ⟼ (M, c)
(AHfn)  (M, ⌜⌞λx_{h}:τ. H⌝⌟_{h}^{τ^{1}→τ^{2}}) ⟼ (M, λx_{a}:τ^{1}. ⌜⌞{⌜⌞x_{a}⌝⌟_{a}^{τ}/x_{h}}H⌝⌟_{h}^{τ^{2}})
(Aμ)  (M, ⌜⌞roll_{μα.τ} Ĥ⌝⌟_{h}^{μα.τ′}) ⟼ (M, roll_{μα.τ′} ⌜⌞Ĥ⌝⌟_{h}^{{μα.τ′/α}τ′})
(ARef) (M, ref_{τ} Â) ⟼ (M[ξ^{τ} ↦ (Â, a)], ξ^{τ}) (ξ^{τ} fresh)
(AAssn)  (M, ξ^{τ} := Â) ⟼ (M[ξ^{τ} ↦ (Â, a)], Â)
(A!)  (M, !ξ^{τ}) ⟼ \{ \begin{matrix}(M, Â) & if M(ξ^{τ}) = (Â, a) \\ (M, ⌜⌞Ĥ⌝⌟_{h}^{τ}) & if M(ξ^{τ}) = (Ĥ, h) \end{matrix}
(ALab)  (M, ⌜⌞ξ^{τ} ⌝⌟_{h}^{τ ref}) ⟼ (M, ξ^{τ})

Host Steps

(HA) (M, ⌜⌞A⌝⌟_{a}^{τ}) ⟼ (M′, ⌜⌞A′⌝⌟_{a}^{τ}) if (M, A) ⟼ (M′, A′)
(HConst)  (M, ⌜⌞c⌝⌟b_{a}) ⟼ (M, c)
(HAfn)  (M, ⌜⌞λx_{a}:τ. A⌝⌟_{a}^{τ^{1}→τ^{2}}) ⟼ (M, λx_{h}:Δ_{h}(τ^{1}). ⌜⌞{⌜⌞x_{h}⌝⌟_{h}^{τ}/x_{a}}A⌝⌟_{a}^{τ^{2}})
(HStrip)  (M, ⌜⌞⌜⌞Ĥ⌝⌟t_{h}⌝⌟_{a}^{τ_{h}}) ⟼ (M, Ĥ)
(Hμ)  (M, ⌜⌞roll_{μα.τ} Â⌝⌟_{a}^{μα.τ}) ⟼ (M, roll_{μα.Δ_{h}(τ)} ⌜⌞Â⌝⌟_{a}^{{μα.τ/α}τ})
(HRef) (M, ref_{τ} Ĥ) ⟼ (M[ξ^{τ} ↦ (Ĥ, h)], ξ^{τ}) (ξ^{τ} fresh)
(HAssn)  (M, ξ^{τ} := Ĥ) ⟼ (M[ξ^{τ} ↦ (Ĥ, a)], Ĥ)
(H!)  (M, !ξ^{τ}) ⟼ \{ \begin{matrix}(M, Ĥ) & if M(ξ^{τ}) = (Ĥ, h) \\ (M, ⌜⌞Â⌝⌟_{a}^{τ}) & if M(ξ^{τ}) = (Â, a) \end{matrix}
(HLab)  (M, ⌜⌞ξ^{τ} ⌝⌟_{a}^{τ ref}) ⟼ (M, ξ^{τ})

Figure 2: Two-agent Dynamic Semantics Program

(Prog) \frac{⊢ M : Ψ Ψ; ∅ ⊢ e : τ}{⊢ (M, e) : τ}

Type Well-Formedness

(Tvar1)  Ξ ⊢ t istype  (Tconst)  Ξ ⊢ b istype
(Tvar2)  \overline{Ξ ⊢ α istype}(α ∈ Ξ)  (Tμ)  \frac{Ξ∪\{α\} ⊢ τ istype}{Ξ ⊢ μα.τ istype}(α ∉ Ξ)
(T →)  \frac{Ξ ⊢ τ istype Ξ ⊢ τ′ istype}{Ξ ⊢ τ → τ′ istype}  (Tref)  \frac{Ξ ⊢ τ istype}{Ξ ⊢ τ ref istype}

Heap Well-Formedness

(Hempty)  ⊢ ∅ : ∅
(HAlab) \frac{⊢ M : Ψ Ψ[ξ^{τ} : τ]; ∅ ⊢_{a} Â : τ}{⊢ M[ξ^{τ} ↦ (Â, a)] : Ψ[ξ^{τ} : τ]}  (HHlab) \frac{⊢ M : Ψ Ψ[ξ^{τ} : τ]; ∅ ⊢_{h} Ĥ : τ′ Δ_{h}(τ) = τ′}{⊢ M[ξ ↦ (Ĥ, h)] : Ψ[ξ^{τ} : τ]}

Polychrome Rules

(Pvar)  Ψ; Γ ⊢ x : Γ(x)  (Pconst)  Ψ; Γ ⊢ c : b
(Papp) \frac{Ψ; Γ ⊢ e : τ′ → τ Ψ; Γ ⊢ e′ : τ′}{Ψ; Γ ⊢ e e′ : τ}  (Plab)  \frac{Ψ(ξ^{τ}) = τ}{Ψ; Γ ⊢ ξ^{τ} : τ ref}
(Proll)  \frac{Ψ; Γ ⊢ e : \{μα.τ/α\}τ}{Ψ; Γ ⊢ roll_{μα.τ} e : μα.τ}  (Punroll)  \frac{Ψ; Γ ⊢ e : μα.τ}{Ψ; Γ ⊢ unroll_{μα.τ} e : \{μα.τ/α\}τ}

Agent Rules

(HinA)  \frac{Ψ; Γ ⊢_{h} H : τ′ Δ_{h}(τ) = τ′}{Ψ; Γ ⊢_{a} ⌜⌞H⌝⌟_{h}^{τ} : τ}  (Afn)  \frac{Ψ; Γ[x_{a} : τ′] ⊢_{a} A : τ}{Ψ; Γ ⊢_{a} λx_{a}:τ′. A : τ′ → τ}
(Aref)  \frac{Ψ; Γ ⊢_{a} A : τ}{Ψ; Γ ⊢_{a} ref_{τ} A : τ ref}  (Abang)  \frac{Ψ; Γ ⊢_{a} A : τ ref}{Ψ; Γ ⊢ !A : τ}
(Aassn) \frac{Ψ; Γ ⊢_{a} A : τ ref Ψ; Γ ⊢_{a} A′ : τ}{Ψ; Γ ⊢_{a} A:= A′ : τ}

Host Rules

(AinH)  \frac{Ψ; Γ ⊢_{a} A : τ}{Ψ; Γ ⊢_{h} ⌜⌞A⌝⌟_{a}^{τ} : Δ_{h}(τ)}  (Hfn)  \frac{Ψ; Γ[x_{h} : τ′] ⊢_{h} H : τ}{Ψ; Γ ⊢_{h} λx_{h}:τ′. H : τ′ → τ} (Δ_{h}(τ′) = τ′)
(Href)  \frac{Ψ; Γ ⊢_{h} H : τ′ Δ_{h}(τ) = τ′}{Ψ; Γ ⊢_{h} ref_{τ} H : τ ref}  (Hbang)  \frac{Ψ; Γ ⊢_{h} H : τ ref}{Ψ; Γ ⊢ !H : Δ_{h}(τ)}
(Hassn) \frac{Ψ; Γ ⊢_{h} H : τ ref Ψ; Γ ⊢_{h} H′ : τ′ Δ_{h}(τ) = τ′}{Ψ; Γ ⊢_{h} H:= H′ : τ′}

Figure 3: Two-agent Static Semantics ensures that agent heap-values have an appropriate typing. Similarly, (HHlab) says that a host can store to a heap location a value whose type is a refinement of the annotation on the label. For example, if τ_{h} = b then the agent may store only embedded host constants (i.e. ⌜⌞c⌝⌟t_{h}) to the location ξt, whereas the host may store a regular constant (c) to the same location. Upon dereference, the agent will always obtain a constant embedded at type t (see rule (A!) of the dynamic semantics).

A typing context, Γ, maps variables (of either color) to types. Judgments Ψ; Γ ⊢_{κ} e : τ say that the term e with color κ is well-formed with type τ relative to heap-type Ψ (for labels occurring in e), and context Γ (for free variables occurring in e). The polychromatic rules are standard, as is the introduction rule for agent functions. For host functions, the only difference is that the type annotation for the argument to a function must be concrete. (We could allow abstract type annotations in the host functions, but then application would need an additional condition to check that the argument to the function is compatible. Since the host knows that t = τ_{h}, this does not limit expressiveness.)

The rule (Plab) says that heap references always have the type ascribed to the label. The rules for creating references, performing assignment, and dereferencing a label allow the host to refine the type of the value being stored or read, while preventing the agent from doing so.

The interesting typing rules are those for embeddings. Rule (HinA) says that an embedded host term, H, exported to the agent at type τ (which may contain occurrences of t) has type τ if the host is able to show that the “actual” type of H is Δ_{h}(τ). In other words, the host may hide type information from the agent by replacing some occurrences of τ_{h} with t in the exported type. The rule for agents embedded inside of host terms, (AinH), is dual in that the host refines the types provided by the agent.

2.5 Safety Properties

In this section, we explore properties of the two-agent calculus including soundness and some type abstraction theorems. These properties are not intended to be as general or as “realistic” as possible. Rather, they convey the flavor of some statements that are provable using syntactic arguments.

2.5.1 Two-agent Type Soundness

The following lemmas establish type soundness:

Lemma 2.1 (Canonical Forms) Assuming Ψ; ∅ ⊢ ê: τ, if τ =

• b, then ê = c for some c.

• τ′ → τ′′, then ê = λx:τ′. e′ for some x and e′.

• t, then ê = ⌜⌞Ĥ⌝⌟t_{h} for some Ĥ of type τ_{h}.

• τ ref, then ê = ξ^{τ} for some label ξ^{τ}.

• μα.τ, then ê = roll_{μα.τ} e′ for some e′ of type {μα.τ/α}τ.

Proof (sketch): By inspection of the dynamic semantics and the form of values. □

Lemma 2.2 (Substitution) If Ψ; Γ[x : τ′] ⊢ e : τ and Ψ; ∅ ⊢ e′ : τ′ and x and e′ have the same color then Ψ; Γ ⊢ {e′/x}e : τ.

Proof: By induction on the typing derivation for Ψ; Γ[x : τ′] ⊢ e : τ. Since x and e′ have the same color, the substitution is syntactically well formed. We proceed by cases on the last rule of the derivation, omitting those that follow by straightforward induction:

(Pconst) Immediate, since substitution has no effect.

(Pvar) Then e = y and there are two sub-cases:

x = y Then τ = τ′ and the result follows by assumption. x ≠ y Then {e′/x}y = y and by strengthening, since x ∉ F V (y), and the assumptions we have

Ψ; Γ ⊢ y : τ.

(Plab) Follows immediately since substitution has no effect.

(Afn) Then e = λx_{a}:τ^{1}. A and τ = τ^{1} → τ^{2} for some x_{a}, A, τ^{1}, and τ^{2}. Furthermore, it must be the case that Ψ; Γ[x : τ′][x_{a} : τ^{1}] ⊢_{a} A : τ^{2}. By the side condition, x ≠ x_{a}, so {e′/x}λx_{a}:τ^{1}. A = λx_{a}:τ^{1}. {e′/x}A. The inductive hypothesis yields Ψ; Γ[x_{a} : τ] ⊢_{a} {e′/x}A : τ^{2}, so by (Afn) the result follows.

(Hfn) This case is similar to the one above.

□

Lemma 2.3 (Weakening) (i) If Γ′ ⊇ Γ then Ψ; Γ ⊢_{κ} e : τ implies Ψ; Γ′ ⊢_{κ} e : τ.

(ii) If Ψ′ ⊇ Ψ then Ψ; Γ ⊢_{κ} e : τ implies Ψ′; Γ ⊢_{κ} e : τ.

Proof (sketch): By induction on the first typing derivation. □

Lemma 2.4 (Preservation) If ⊢ M : Ψ, Ψ; ∅ ⊢ e : τ and (M, e) ⟼ (M′, e′) then for some Ψ′, Dom(M′) ⊇ Dom(M), Ψ′ ⊇ Ψ, ⊢ M′ : Ψ′, and Ψ′; ∅ ⊢ e′ : τ.

Proof: The proof proceeds by cases on the transition step taken. The agent steps do not differ significantly from the corresponding host-cases, except that the substitution Δ_{h} is unnecessary since the agent can never refine type information. Since duplicating the proofs is, for the most part, unilluminating, we show as an example the case for (AHfn); the rest are elided. Similarly, those cases that follow by straightforward induction and the Weakening Lemma are omitted.

(Pβ) Then e = (λx:τ^{1}. e^{1})ê for some τ^{1}, e^{1}, ê. By assumption, the last rule used in type-checking e must be (Papp), so it follows that Ψ; [x : τ^{1}] ⊢ e^{1} : τ and Ψ; ∅ ⊢ ê : τ^{1}. By Substitution, it follows that Ψ; ∅ ⊢ {ê/x}e^{1} : τ, and, since M doesn’t change, the result holds.

(Pμ3) Then e = unroll_{μα.τ} roll_{μα.τ} ê for some ê. The last two rules in the typing derivation must have been (Proll) followed by (Punroll), thus we have Ψ; ∅ ⊢ ê: {μα.τ/α}τ. Since Ψ; ∅ ⊢ e : {μα.τ/α}τ and M doesn’t change, we’re done.

(HA) In this case, e = ⌜⌞A⌝⌟_{a}^{τ′} for some A and its typing derivation ends in (AinH). We conclude Ψ; ∅ ⊢_{a} A : τ′ and that τ = Δ_{h}(τ′). Furthermore, we know (M, A) ⟼ (M′, A′), so by the inductive hypothesis: ⊢ M′ : Ψ′, Ψ′ ⊇ Ψ, Dom(M) ⊆ Dom(M′), and Ψ′; ∅ ⊢_{a} A′ : τ′. Thus the result follows by (AinH).

(HConst) By (AinH) and the definition of Δ_{h}, e has type b. By (Pconst), e′ = c has type b. M doesn’t change, so Ψ′ = Ψ.

(HAfn) Then e = ⌜⌞λx_{a}:τ^{1}. A⌝⌟_{a}^{τ^{1}→τ^{2}}. Since e is well-typed there is a derivation of this form:

\frac{\frac{Ψ; [x_{a} : τ^{1}] ⊢_{a} A : τ^{2}}{Ψ; ∅ ⊢_{a} λx_{a}:τ^{1}. A : τ^{1} → τ^{2}}}{Ψ; ∅ ⊢_{h} ⌜⌞λx_{a}:τ^{1}. A⌝⌟_{a}^{τ^{1}→τ^{2}} : Δ_{h}(τ^{1} → τ^{2})}

Note that from the definition of Δ_{h}, we have Δ_{h}(τ^{1} → τ^{2}) = Δ_{h}(τ^{1}) → Δ_{h}(τ^{2}). Also it is easy to show that Δ_{h}(Δ_{h}(τ^{1})) = Δ_{h}(τ^{1}). Thus it suffices to find the premise of the following derivation:

\frac{\frac{Ψ; [x_{h} : Δ_{h}(τ^{1})] ⊢_{a} \{⌜⌞x_{h}⌝⌟_{h}^{τ^{1}}/x_{a}\}A : τ^{2}}{Ψ; [x_{h} : Δ_{h}(τ^{1})] ⊢_{h} ⌜⌞\{⌜⌞x_{h}⌝⌟_{h}^{τ^{1}}/x_{a}\}A⌝⌟_{a}^{τ^{2}} : Δ_{h}(τ^{2})}}{Ψ; ∅ ⊢_{h} λx_{h}:Δ_{h}(τ^{1}). ⌜⌞\{⌜⌞x_{h}⌝⌟_{h}^{τ^{1}}/x_{a}\}A⌝⌟_{a}^{τ^{2}} : Δ_{h}(τ^{1}) → Δ_{h}(τ^{2})}

Fortunately, we also have this derivation:

\frac{Ψ; [x_{h} : Δ_{h}(τ^{1})] ⊢_{h} x_{h} : Δ_{h}(τ^{1}) Δ_{h}(τ^{1}) = Δ_{h}(τ^{1})}{Ψ; [x_{h} : Δ_{h}(τ^{1})] ⊢_{a} ⌜⌞x_{h}⌝⌟_{h}^{τ^{1}} : τ^{1}}

By weakening the premise of the original derivation and using the substitution lemma, we conclude the premise of the sufficient derivation.

(HStrip) In this case, e = ⌜⌞⌜⌞Ĥ⌝⌟t_{h}⌝⌟_{a}^{τ_{h}}, and since, by definition, Δ_{h}(τ_{h}) = τ_{h}, there is a derivation of the form:

\frac{\frac{Ψ; ∅ ⊢_{h} Ĥ : τ_{h} Δ_{h}(t) = τ_{h}}{Ψ; ∅ ⊢_{a} ⌜⌞Ĥ⌝⌟t_{h} : τ_{h}}}{Ψ; ∅ ⊢_{h} ⌜⌞⌜⌞Ĥ⌝⌟t_{h}⌝⌟_{a}^{τ_{h}} : Δ_{h}(τ_{h}) = τ_{h}}

The premise of the derivation is sufficient to complete this case of the proof.

(Hμ) Then e = ⌜⌞roll_{μα.τ′} Â⌝⌟_{a}^{μα.τ′}. By definition, Δ_{h}(μα.τ) = μα.Δ_{h}(τ), so we have the following derivation:

\frac{\frac{Ψ; ∅ ⊢_{a} Â : \{μα.τ′/α\}τ′}{Ψ; ∅ ⊢_{a} roll_{μα.τ′} Â : μα.τ′}}{Ψ; ∅ ⊢_{h} ⌜⌞roll_{μα.τ′} Â⌝⌟_{a}^{μα.τ′} : Δ_{h}(μα.τ′)}

Using the premise above, we also have this derivation:

\frac{\frac{Ψ; ∅ ⊢_{a} Â : \{μα.τ′/α\}τ′}{Ψ; ∅ ⊢_{h} ⌜⌞Â⌝⌟_{a}^{\{μα.τ′/α\}τ′} : \{μα.Δ_{h}(τ′)/α\}Δ_{h}(τ′)}}{Ψ; ∅ ⊢_{h} roll_{μα.Δ_{h}(τ′)} ⌜⌞Â⌝⌟_{a}^{\{μα.τ′/α\}τ′} : μα.Δ_{h}(τ′)}

which follows from applying the definition of Δ_{h} like so: Δ_{h}({μα.τ′/α}τ′) = {Δ_{h}(μα.τ′)/α}Δ_{h}(τ′) = {μα.Δ_{h}(τ′)/α}Δ_{h}(τ′). The result holds because, as already observed, Δ_{h}(μα.τ′) = μα.Δ_{h}(τ′).

(HRef) Then e = ref_{τ′} Ĥ and τ = τ′ ref. Since e is well typed, there is a derivation of the form:

\frac{Ψ; ∅ ⊢_{h} Ĥ : τ′′ Δ_{h}(τ′) = τ′′}{Ψ; ∅ ⊢_{h} ref_{τ′} Ĥ : τ′ ref}

We must show that there exists a Ψ′ ⊇ Ψ such that ⊢ M[ξ^{τ′} ↦ (Ĥ, h)] : Ψ′ and such that Ψ′; ∅ ⊢_{h} ξ^{τ′} : τ′ ref. Consider Ψ′ = Ψ[ξ^{τ′} : τ′]. Then by weakening the premise of the above derivation and applying the rule (HHlab) we have that ⊢ M[ξ^{τ′} ↦ (Ĥ, h)] : Ψ[ξ^{τ′} : τ′]. The rule (Plab) allows us to derive the rest of the result.

(Hassn) In this case, e = ξ^{τ} := Ĥ. Sine it is well typed there is the following derivation:

\frac{\frac{Ψ(ξ^{τ}) = τ}{Ψ; ∅ ⊢_{h} ξ^{τ} : τ ref} Ψ; ∅ ⊢_{h} Ĥ : τ′ Δ_{h}(τ) = τ′}{Ψ; ∅ ⊢_{h} ξ^{τ} := Ĥ : τ}

Note that since Ψ(ξ^{τ}) = τ we have Ψ[ξ^{τ} : τ] = Ψ and, by applying (HHlab) to the premises of the above derivation, we have:

\frac{⊢ M : Ψ Ψ[ξ^{τ} : τ]; ∅ ⊢_{h} Ĥ : τ′ Δ_{h}(τ) = τ′}{⊢ M[ξ^{τ} ↦ (Ĥ, h)] : Ψ[ξ^{τ} : τ]}

Which shows that the new heap is well typed under the same Ψ. The premise Ψ; ∅ ⊢_{h} ξ^{τ} : τ ref is what we need to complete this case of the proof.

(H!) We have e = !ξ^{τ′} and since e is well typed, there is this derivation:

\frac{\frac{Ψ(ξ^{τ′}) = τ′}{Ψ; ∅ ⊢_{h} ξ^{τ′} : τ′ ref}}{Ψ; ∅ ⊢_{h} !ξ^{τ′} : Δ_{h}(τ′)}

It follows that τ = Δ_{h}(τ′). There are two cases depending on the heap contents at label ξ^{τ′}:

M(ξ^{τ′}) = (Ĥ, h) The well-typedness of the heap must have been arrived at by an application of rule (HHlab), which means we have the following derivation:

\frac{⊢ M : Ψ Ψ[ξ^{τ′} : τ′]; ∅ ⊢_{h} Ĥ : τ′′ Δ_{h}(τ′) = τ′′}{⊢ M[ξ^{τ′} ↦ (Ĥ, h)] : Ψ[ξ^{τ′} : τ′]}

Since Ψ(ξ^{τ′}) = τ′ we have Ψ = Ψ[ξ^{τ′} : τ′] and it follows that Ψ; ∅ ⊢_{h} Ĥ : Δ(τ′), which is exactly what we want.

M(ξ^{τ′}) = (Â, a) In this case, the fact that M is well-typed follows from an application of (HAlab) with this derivation:

\frac{⊢ M : Ψ Ψ[ξ^{τ′} : τ′]; ∅ ⊢_{a} Â : τ′}{⊢ M[ξ^{τ′} ↦ (Â, a)] : Ψ[ξ^{τ′} : τ′]}

As before, we also know that Ψ = Ψ[ξ^{τ′} : τ′], so an application of (AinH) to the premise above yields Ψ; ∅ ⊢_{h} ⌜⌞Â⌝⌟_{a}^{τ′} : Δ_{h}(τ′) which is the desired result.

(Hlab) Here, e = ⌜⌞ξ^{τ′}⌝⌟_{a}^{τ′ ref} and we have the derivation:

\frac{\frac{Ψ(ξ^{τ′}) = τ′}{Ψ; ∅ ⊢_{a} ξ^{τ′} : τ′ ref}}{Ψ; ∅ ⊢_{h} ⌜⌞ξ^{τ′}⌝⌟_{a}^{τ′ ref} : Δ_{h}(τ′ ref)}

But, the definition of Δ_{h} ensures that Δ_{h}(τ′ ref) = τ′ ref. Thus we may use (Plab) with the premise of the above derivation to conclude that Ψ; ∅ ⊢_{h} ξ^{τ′} : τ′ ref. Since M doesn’t change, we’re done.

(AHfn) In this case, e = ⌜⌞λx_{h}:τ^{0}. H⌝⌟_{h}^{τ^{1}→τ^{2}} and the typing derivation is of the form:

\frac{\frac{Ψ; [x_{h} : τ^{0}] ⊢_{h} H : τ^{3}}{Ψ; ∅ ⊢_{h} λx_{h}:τ^{0}. H : τ^{0} → τ^{3} Δ_{h}(τ^{1} → τ^{2}) = τ^{0} → τ^{3}}}{Ψ; ∅ ⊢_{a} ⌜⌞λx_{h}:τ^{0}. H⌝⌟_{h}^{τ^{1}→τ^{2}} : τ^{1} → τ^{2}}

It suffices to find a derivation of this form for e′:

\frac{\frac{Ψ; [x_{a} : τ^{1}] ⊢_{h} \{⌜⌞x_{a}⌝⌟_{a}^{τ^{0}}/x_{h}\}H : τ^{3} τ^{3} = Δ_{h}(τ^{2})}{Ψ; [x_{a} : τ^{1}] ⊢_{a} ⌜⌞\{⌜⌞x_{a}⌝⌟_{a}^{τ^{0}}/x_{h}\}H⌝⌟_{h}^{τ^{2}} : τ^{2}}}{Ψ; ∅ ⊢_{a} λx_{a}:τ^{1}. ⌜⌞\{⌜⌞x_{a}⌝⌟_{a}^{τ^{0}}/x_{h}\}H⌝⌟_{h}^{τ^{2}} : τ^{1} → τ^{2}}

From the first derivation, it follows that τ^{3} = Δ_{h}(τ^{2}). Since τ^{0} = Δ_{h}(τ^{0}), we also have the following derivation:

\frac{Ψ; [x_{a} : τ^{0}] ⊢_{a} x_{a} : τ^{0}}{Ψ; [x_{a} : τ^{0}] ⊢_{h} ⌜⌞x_{a}⌝⌟_{a}^{τ^{0}} : Δ_{h}(τ^{0}) = τ^{0}}

By weakening the first premise of the derivation and applying the substitution lemma, we conclude the first premise of the second derivation, so the result holds.

□

Lemma 2.5 (Progress) If ⊢ M : Ψ and Ψ; ∅ ⊢ e : τ, then either e is a value or there exists an e′ such that (M, e) ⟼ (M′, e′).

Proof: By structural induction on e. Note that because e is well-typed, e cannot be a variable. We proceed by cases:

e = c, e = λx:τ. e′, e = ξ^{τ}, e = roll_{μα.τ} ê, or e = ⌜⌞Ĥ⌝⌟t_{h} Then e is a value and the lemma holds.

e = e′e′′ This case follows by straightforward induction in the case that e′ or e′′ is not a value—the transition is via rule (P1) or (P2). In the case that e′ and e′′ are both values, well-typedness of e and Canonical Forms yields that e′ = λx:τ. e′′′ and the transition is via rule (Pβ).

e = ref_{τ} e′ If e′ is not a value, then the transition is via rule (PRef1), otherwise either (Aref) or (Href) applies, depending on the color of e.

e = !e′ If e′ is not a value, then rule (P!) applies. Otherwise, well typedness of e yields that e′ has type τ ref for some type τ. Since e′ is a value, Canonical Forms tells us that e′ = ξ^{τ}. Either (A!) or (H!) applies depending on the color of e′.

e = e′:= e′′ If at least one of e′ and e′′ is not a value, then rules (PAssn1) or (PAssn2) apply. If both are values, then well-typedness of e yields that e′ has type τ ref, and so, by Canonical Forms, e′ = ξ^{τ}. One of (AAssn) or (HAssn) applies, depending on the color of e′.

e = roll_{μα.τ} e′ If e′ is not a value, then (Pμ1) applies.

e = unroll_{μα.τ} e′ If e′ is not a value, then (Pμ2) applies. Otherwise, well-typedness of e and Canonical Forms yields that e′ = roll_{μα.τ} ê, in which case (Pμ3) applies.

e = ⌜⌞e′⌝⌟_{κ}^{τ} If e′ is not a value, then, by the inductive hypothesis, either (AH) or (HA) applies. We consider the remaining cases, assuming that e′ is a value but e is not:

τ = τ′ ref Here, e′ must be of the form ξ^{τ′} (by Canonical Forms) and either (ALab) or (HLab) applies.

τ = b Then e = ⌜⌞c⌝⌟b_{κ} and one of (AConst) or (HConst) applies, depending on e’s color.

τ = μα.τ Then e = ⌜⌞roll_{μα.τ2} ê⌝⌟_{κ}^{μα.τ} by Canonical Forms on e′ and it follows that either (Aμ) or (Hμ) applies.

τ = τ^{1} → τ^{2} By Canonical forms, e′ = λx:τ′. e′′ and either (AHfn) or (HAfn) provides the transition.

κ = a, e′ = ⌜⌞Ĥ⌝⌟t_{h} In this case, (HStrip) applies.

□

Definition 2.6 (Stuck Terms) A configuration (M, e) is \underline{stuck} if e is not a value and there is no configuration (M′, e′) such that (M, e) ⟼ (M′, e′).

Theorem 2.7 (Type Soundness) If Ψ; ∅ ⊢ e : τ and ⊢ M : Ψ then there is no stuck (M′, e′) such that (M, e) ⟼^{∗} (M′, e′).

Proof: Follows from Preservation and Progress. □

erase(x) = x
erase(c) = c
erase(ξ^{τ}) = ξ
erase(λx:τ. e) = λx:{τ_{h}/t}τ. erase(e)
erase(e e′) = erase(e) erase(e′)
erase(ref_{τ} e) = ref_{{τ_{h}/t}τ} erase(e)
erase(e:= e′) = erase(e) := erase(e′)
erase(!e) = !erase(e)
erase(roll_{μα.τ} e) = roll_{{τ_{h}/t}μα.τ} erase(e)
erase(unroll_{μα.τ} e) = unroll_{{τ_{h}/t}μα.τ} erase(e)
erase(⌜⌞e⌝⌟_{κ}^{τ}) = erase(e)
erase(∅) = ∅
erase(M[ξ^{τ} ↦ (ê, κ)]) = erase(M)[ξ ↦ erase(ê)]
erase(M, e) = (erase(M), erase(e))

Figure 4: Two-agent erase translation

2.5.2 Two-agent Erasure

Given a term, if we ignore the distinction between colors, erase the embeddings, and replace t with τ_{h}, we have a simply-typed λ-calculus term. Formally, Figure 4 defines the erasure of a two-agent term. (All rules are polychromatic.) The following lemma states that erasure commutes with evaluation.

Lemma 2.8 (Erasure) Let e be any two-agent term such that Ψ; ∅ ⊢ e : τ. Then (M, e) ⟼^{∗} (M′, ê) iff erase(M, e) ⟼^{∗} erase(M′, ê).

Proof (sketch): First prove that substitution commutes with erasure. With that lemma in hand, the erasure lemma follows by induction on the source derivation. The proof is straightforward and not interesting so we omit it here. □

2.5.3 Two-agent Abstraction Properties

Before proving the type abstraction properties, we make a convenient definition, which allows us to perform substitutions in an open heap:

Definition 2.9 (Pre-Heap) If Γ is a typing context, we say that a finite map P : Labels → (T erms × Agents) is a Γ-pre-heap of type Ψ, written Γ ⊢ P : Ψ, if for every label ξ^{τ} such that P (ξ^{τ}) = (A, a) it is the case that Ψ; Γ ⊢_{a} A : τ and for every label ξ^{τ} such that P (ξ^{τ}) = (H, h) it is the case that Ψ; Γ ⊢_{h} H : τ′ and Δ_{h}(τ) = τ′.

Note that if Γ = ∅ then a pre-heap is just a normal heap. The difference is that pre-heaps can contain references to open terms in addition to values. Substitution over a Γ-pre-heap P is as follows: If Ψ; ∅ ⊢_{κ} ê: τ and Γ ⊢ P : Ψ and Γ(x_{κ}) = τ then {ê/x_{κ}}P is defined by:

• {ê/x_{κ}}∅ = ∅

• {ê/x_{κ}}(P [ξ^{τ′} ↦ (e, κ′)]) = ({ê/x_{κ}}P)[ξ^{τ′} ↦ ({ê/x_{κ}}e, κ′)]

Lemma 2.10 (Heap Substitution) If Γ[x_{κ} : τ] ⊢ P : Ψ and Γ(x_{κ}) = τ and Ψ; ∅ ⊢_{κ} ê : τ then Γ ⊢ {ê/x_{κ}}P : Ψ.

We write {e/x_{κ}}(P, e′) for ({e/x_{κ}}P, {e/x_{κ}}e′) whenever such a substitution is appropriate.

Definition 2.11 (Reachable Term) A term e′ is reachable from a configuration (M, e) if either

• e′ is a subterm of e

• For any label ξ^{τ}, a subterm of e, M(ξ^{τ}) = (ê, κ) and e′ is reachable from (M, ê).

Definition 2.12 (Host-free) If no host-term is reachable from the configuration (M, A) then (M, A) is said to be host-free.

We use the terminology reachable and host-free (defined as above) also for pairs (P, A) where P is a pre-heap and A is a (not-necessarily-closed) expression.

Lemma 2.13 (Value Abstraction) Let P be a pre-heap such that [x_{a} : t] ⊢ P : Ψ. Let Ĥ and Ĥ′ be host values such that Ψ; ∅ ⊢_{h} Ĥ : τ_{h} and Ψ; ∅ ⊢_{h} Ĥ′ : τ_{h}. Let A be an agent-term such that Ψ; [x_{a} : t] ⊢_{a} A : τ and further suppose that (P, A) is host-free and {⌜⌞Ĥ⌝⌟t_{h}/x_{a}}A is not a value. Let σ_{1} = {⌜⌞Ĥ⌝⌟t_{h}/x_{a}} and σ_{2} = {⌜⌞Ĥ′⌝⌟t_{h}/x_{a}}. Then there exists a term A′ and a [x_{a} : t]-pre-heap P′ such that:

1. [x_{a} : t] ⊢ P′ : Ψ′ where Ψ′ ⊇ Ψ

2. Ψ′; [x_{a} : t] ⊢_{a} A′ : τ

3. (P′, A′) is host-free

4. σ_{1}(P, A) ⟼ σ_{1}(P′, A′)

5. σ_{2}(P, A) ⟼ σ_{2}(P′, A′)

Proof: The proof goes by induction on the derivation that σ_{1}(p, A) transitions. Note that since A is host-free and Ĥ is a value, the only rules occurring in the derivation are polychromatic or agent-rules. We can eliminate all of the agent rules except (ARef), (AAssn) and (A!) since Ĥ is a value and there are no other reachable host-terms. Thus we proceed by cases on each of the remaining rules:

(P1), (P2), (Pμ1), (Pμ2), (P!), (PRef1), (PAssn1), or (PAssn2) These follow by straightforward induction and the definition of substitution. As an example, we show the case for (P1); the rest are similar. Since σ_{1}A transitions via rule (P1) and since ⌜⌞Ĥ⌝⌟t_{h} is a value, A must be of the form A^{1} A^{2} where σ_{1}A^{1} is not a value. This follows because σ_{1}A = σ_{1}(A^{1} A^{2}) = (σ_{1}A^{1}) (σ_{1}A^{2}) by the definition of substitution. Furthermore, the typing rule for applications yields that Ψ; [x_{a} : t] ⊢_{a} A^{1} : τ′ → τ for some τ′. Since A^{1} is a subterm of A, it follows from the definition of host-free that (P, A^{1}) is host-free. Thus the inductive hypothesis applies and we conclude that there is a term A′′ and a [x_{a} : t]-pre-heap P′′ such that Ψ′′; [x_{a} : t] ⊢_{a} A′′ : τ′ → τ, (P′′, A′′) is host-free, σ_{1}(P, A^{1}) ⟼ σ_{1}(P′′, A′′), and σ_{2}(P, A^{1}) ⟼ σ_{2}(P′′, A′′). Let Ψ′ = Ψ′′ and choose P′ = P′′ and A′ = (A′′ A^{2}). Claim: P′ and A′ satisfy properties 1 through 5. Property 1 holds by the inductive hypothesis and weakening since Ψ′ = Ψ′′ ⊇ Ψ and P′ = P′′. Property 2 follows from the well-typedness of A and the inductive hypothesis via rule (Papp). Property 3 follows from the inductive hypothesis and the observation that since A^{2} is a subterm of A it is host-free. Property 4 is established by an application of (P1) to the results of the inductive hypothesis: (σ_{1}P, (σ_{1}A^{1}) (σ_{1}A^{2})) ⟼ (σ_{1}P, (σ_{1}A′′) (σ_{1}A^{2})) which equals (σ_{1}P, σ_{1}(A′′ A^{2})) which is σ_{1}(P′, A′). Property 5 follows analogously.

(Pβ) Since it is well-typed, and, in particular, because x_{a} has type t and so can’t appear in the application position of an agent term, σ_{1}A is of the form σ_{1}((λy_{a}:τ. A^{1}) A^{2}) which, if x_{a} ≠ y_{a}, equals (by the definition of substitution) (λy_{a}:τ′. σ_{1}A^{1}) (σ_{1}A^{2}), or, if x_{a} = y_{a}, it equals (λy_{a}:τ′. A^{1}) (σ_{1}A^{2}). In the former case, the transition step yields {(σ_{1}A^{2})/y_{a}}(σ_{1}A^{1}), which, since x_{a} ≠ y_{a}, is σ_{1}({A^{2}/y_{a}}A^{1}), while in the latter case the transition yields {(σ_{1}A^{2})/y_{a}}A^{1} = σ_{1}({A^{2}/y_{a}}A^{1}. Choose A′ = {A^{2}/y_{a}}A^{1} and P′ = P. Again, since P is unchanged, Property 1 holds by assumption. Property 2: This follows from the Substitution Lemma and the assumption that A is well-typed. Property 3: P′ is clearly host-free since P is. A′ has no occurrences of host code since neither A^{1} nor A^{2} do and substitution doesn’t change the color of code. Property 4: follows from observations above about the transition step. Property 5: This follows analogously to 4 using the observation that σ_{2}A = σ_{2}(λy_{a}:τ′. A^{1}) (σ_{2}A^{2}) and following similar calculations of the transition step.

(Pμ3) In this case, σ_{1}A is of the form σ_{1}(unroll_{μα.τ} roll_{μα.τ′} A^{1}). Take A′ = A^{1} and P′ = P. Property 1 is trivial. Property 2 follows from the well-typedness of A, since the last two steps of the typing derivation must have been (Proll) followed by (Punroll). We conclude that Ψ; [x_{a} : t] ⊢_{a} A′ : {μα.τ′/α}τ′. Since A′ is a sub-term of A, the configuration (P′, A′) is host-free, satisfying Property 3. Property 4 is established via the definition of substitution: (σ_{1}P, σ_{1}A) = (σ_{1}P, unroll_{μα.τ′} roll_{μα.τ′} (σ_{1}A^{1})) which steps via (Pμ3) to (σ_{1}P, σ_{1}A^{1}) = σ_{1}(P, A^{1}) which is just σ_{1}(P′, A′). Similarly we have (σ_{2}P, σ_{2}A) = (σ_{2}P, unroll_{μα.τ′} roll_{μα.τ′} (σ_{2}A^{1})) which steps via (Pμ3) to (σ_{2}P, σ_{2}A^{1}) = σ_{2}(P, A^{1}), again, just σ_{2}(P′, A′).

(ARef) In this case, σ_{1}A = ref_{τ} Â and it follows that A = ref_{τ} A′′ for some A′′. Since σ_{1}(P, A) steps to (M, ξ^{τ}) for some M and fresh label, ξ^{τ}, we choose P′ = P [ξ ↦ (A′′, a)] and A′ = ξ^{τ}. It remains to verify properties 1 through 5. Property 1: By assumption we have Ψ; [x_{a} : t] ⊢_{a} ref_{τ} A′′ : τ ref, which must have been derived by an application of (Aref). It follows that Ψ; [x_{a} : t] ⊢_{a} A′′ : τ. Since P is an [x_{a} : t]-pre-heap with type Ψ and ξ^{τ} ∉ Dom(P), it follows that [x_{a} : t] ⊢ P [ξ ↦ A′′] : Ψ′ = Ψ[ξ^{τ} : τ], and hence Ψ′ ⊇ Ψ. Property 2: We must show that Ψ′; [x_{a} : t] ⊢_{a} ξ^{τ} : τ ref. We may conclude this via rule (Plab) since Ψ′(ξ^{τ}) = τ as constructed above. Property 3: Since P and A′′ are hostfree and the only terms reachable from (P′, ξ^{τ}) are those reachable from (P′, A′′) plus ξ^{τ} (an agent label), it follows that (P′, A′) is host-free as well. We verify Property 4 with the following calculation: σ_{1}(P, A) = (σ_{1}P, σ_{1}A) = (σ_{1}P, σ_{1}(ref_{τ} A′′)) = (σ_{1}P, ref_{τ} σ_{1}A′′) ⟼ ((σ_{1}P)[ξ^{τ} ↦ (σ_{1}A′′, a)], ξ^{τ}) = (σ_{1}(P [ξ^{τ} ↦ (A′′, a)]), ξ^{τ}) = σ_{1}(P [ξ^{τ} ↦ (A′′, a)], ξ^{τ}) = σ_{1}(P′, A′). Property 5 follows via the same calculation replacing σ_{1}by σ_{2}.

(AAssn) In this case, σ_{1}A = ξ^{τ} := Â it follows that A = ξ^{τ} := A′′ where A′′ is host-free. Take A′ = A′′ and choose P′ = P [ξ^{τ} ↦ (A′, a)]. Note that Ψ; [x_{a} : t] ⊢_{a} ξ^{τ} := A′′ : τ must have been derived via rule (AAssn) and so it follows that Ψ; [x_{a} : t] ⊢_{a} ξ^{τ} : τ ref which can be derived only via (Alab). Thus it must be the case that Ψ(ξ^{τ}) = τ. Likewise it must be the case that Ψ; [x_{a} : t] ⊢_{a} A′′ : τ. We first verify Property 1: By assumption, [x_{a} : t] ⊢ P : Ψ. By the definition of pre-heap and the type derivation for A′′ = A′, it follows that [x_{a} : t] ⊢ P [ξ^{τ} ↦ (A′, a)] : Ψ. Property 2 has already been observed to be a consequence of the original typing derivation. Property 3 follows since A′ is host free and the original P was also host-free. We verify Property 4 by the calculation: σ_{1}(P, A) = σ_{1}(P, ξ^{τ} := A′′) = (σ_{1}P, σ_{1}(ξ^{τ} := A′′)) = (σ_{1}P, ξ^{τ} := σ_{1}A′′) ⟼ ((σ_{1}P)[ξ^{τ} ↦ (σ_{1}A′′, a)], σ_{1}A′′) = (σ_{1}(P [ξ^{τ} ↦ (A′′, a)]), σ_{1}A′′) = σ_{1}(P [ξ^{τ} ↦ (A′′, a)], A′′) = σ_{1}(P′, A′). Property 5 follows analogously.

(A!) In this case, σ_{1}A = !ξ^{τ}, which means that A = !ξ^{τ}. Since (P, A) is host-free, it must be the case that P (ξ^{τ}) = (A′, a) for some A′. This is the A′ we seek, it also means that the transition step is determined to be of the first flavor listed in (A!). Let P′ = P. Then Property 1 follows since P is unchanged. Property 2 follows by the well-typedness of the pre-heap P. Property 3 holds since ξ^{τ} is a subterm of A which means that A′ is reachable from A and hence (P, A′) is also host-free. Property 4 is established as follows: σ_{1}(P, A) = (σ_{1}P, σ_{1}A) = (σ_{1}P, !ξ^{τ}). As noted above, P (ξ^{τ}) = (A′, a) implies that this must step via (A!) to (σ_{1}P, (σ_{1}A′)) = σ_{1}(P′, A′). Property 4 follows by a similar computation.

□

Using the Value Abstraction lemma, we prove the following:

Theorem 2.14 (Independence of Evaluation) Let M be a heap such that ⊢ M : Ψ. Let Ĥ and Ĥ′ be host values such that Ψ; ∅ ⊢_{h} Ĥ : τ_{h} and Ψ; ∅ ⊢_{h} Ĥ′ : τ_{h}. Let A be an agent-term such that Ψ; ∅ ⊢_{a} λx_{a}:t. A : t → b and further suppose that (M, λx_{a}:t. A) is host-free. Then:

(M, (λx_{a}:t. A)⌜⌞Ĥ⌝⌟t_{h}) ⟼^{∗} c

iff

(M, (λx_{a}:t. A)⌜⌞Ĥ′⌝⌟t_{h}) ⟼^{∗} c

Proof: After one step for each evaluation, the configurations are in a form so that the Value Abstraction lemma applies. Since that lemma preserves its own preconditions, inductively apply it to the rest of the evaluation. This shows that the two evaluation sequences must be in lock-step, and so halt with the same value, c. □

Lemma 2.15 (Constant Embeddings) If ⊢ M : Ψ and Ψ; [x_{κ} : b] ⊢ e : τ then (M, {c/x_{κ}}e) ⟼^{∗}

(M′, ê) if and only if (M, {⌜⌞c⌝⌟b_{κ^{∘}}/x_{κ}}e) ⟼^{∗} (M′, ê).

Proof (sketch): The proof goes by induction on the derivation of the evaluation sequence. The idea is to simply insert (AConst) or (HConst) steps whenever the embedding ⌜⌞c⌝⌟b_{κ^{∘}} appears. □

Theorem 2.16 (Host-provided Values) Suppose M is a heap such that ⊢ M : Ψ. Let Â = λy_{a}:b → t. A be an agent function such that Ψ; ∅ ⊢_{a} Â : τ and (M, Â) is host-free. Further suppose that Ψ; [x_{h} : b] ⊢_{h} ho : τ_{h} and (M, λx_{h}:b. ho) is agent-free. If (M, (λy_{a}:b → t. A) ⌜⌞λx_{h}:b. ho⌝⌟_{h}^{b→t}) ⟼^{∗} (M′, A′) then for any sub-term ⌜⌞Ĥ⌝⌟t_{h} of A′, there is a constant c and heap M′′ such that (M′′, {c/x_{h}}ho) ⟼^{∗} (M′′′, Ĥ).

Proof: After one step of evaluation, the configuration is (M, (λy_{a}:b → t. A) λx_{a}:b. ⌜⌞{⌜⌞x_{a}⌝⌟b_{a}/x_{h}}ho⌝⌟t_{h}). The following lemma applies because the only reachable host-embedding is of type t and nearly-agent free (the only freely occurring agent-terms are x_{a}). The lemma implies that under any sequence of transition steps, the only thing that can happen to a host-embedding is the substitution of a constant for x_{a}, after which it may take host-transition steps. But this says exactly that there is some memory configuration M′′ such that (M′′, {c/x_{a}}{⌜⌞x_{a}⌝⌟b_{a}/x_{h}}ho) ⟼ (M′′′, Ĥ). Since ho is agent-free, we have {c/x_{a}}{⌜⌞x_{a}⌝⌟b_{a}/x_{h}}ho = {⌜⌞c⌝⌟b_{a}/x_{h}}ho. The result follows from the Constant Embeddings lemma. □

Lemma 2.17 (Host-Provided Values (step)) Suppose M is a heap such that ⊢ M : Ψ. Let A be a closed agent term such that:

• If ⌜⌞H⌝⌟_{h}^{τ} is a host-embedding reachable from (M, A) then τ = t and H is nearly-agent free. That is, Ψ; [x_{a} : b] ⊢_{a} ⌜⌞H⌝⌟t_{h} : t, and x_{a} is the only agent-term reachable in (M, H).

• There are no agent colored labels that are reachable from (M, A) which point to host values. That is, if ξ^{τ} is an agent term reachable from (M, A) then M(ξ^{τ}) = (Â, a) for some Â.

Further suppose that (M, A) ⟼ (M′, A′). Then every agent label reachable from (M′, A′) points to an agent value, and, in addition, if ⌜⌞H′⌝⌟_{h}^{τ} is any host-embedding reachable from (M′, A′) then τ = t and one of the following is true:

1. ⌜⌞H′⌝⌟t_{h} is reachable from (M, A).

2. H′ = {c/x_{a}}H where ⌜⌞H⌝⌟t_{h} is reachable from (M, A).

3. There is some ⌜⌞H⌝⌟t_{h} reachable from (M, A) and (M, H) ⟼ (M′, H′) and H′ is agent-free.

Proof: Proof by induction on the derivation that (M, A) ⟼ (M′, A′). We proceed by cases:

(P1) Here, A is of the form A^{1} A^{2}. From the assumptions, it follows that the only host-embeddings reachable from (M, A^{1}) also satisfy the requirements for the lemma. We also know that (M, A^{1}) ⟼ (M′, A^{3}) for some A^{3} and that A′ = A^{3} A^{2}. Let ⌜⌞H′⌝⌟_{h}^{τ} be a host-embedding reachable from (M′, A′) and suppose it is not reachable from (M, A). By the lemma below, ⌜⌞H′⌝⌟_{h}^{τ} must be reachable from (M′, A^{3}) but not (M, A).

Lemma 2.18 The set of reachable host-embeddings for (M′, A^{2}) is also reachable from (M, A).

Proof: If an embedding is reachable from A^{2} it is either a subterm of A^{2} or reached via some reference in the heap. Since A^{2} doesn’t change, the only embeddings that could be affected by the transition step must have been reached via reference shared with the term A^{1}, which took the transition step. The heap can change in only two ways: by assignment via rule (AAssn) or (HAssn), in which case the subterm ξ^{τ} := ê must occur in A^{1} and hence be reachable from (M, A), or by creation of a new reference ((Aref) or (Href)) which cannot be referred to by A^{2} because the newly created label is fresh. □

The embedding part of the conclusion then follows from the inductive hypothesis, since any new hostembedding must fall into cases (2) or (3).

Now we must show that any agent-colored label reachable from (M′, A′) points to an agent value in the heap. By the inductive hypothesis all agent labels reachable from (M′, A^{3}) must point to agent values, so let ξ^{τ} be an agent label reachable from (M′, A^{2}). If ξ^{τ} is also reachable from (M′, A^{3}) we’re done, so assume it isn’t. If ξ^{τ} wasn’t reachable from (M, A^{1}) then the transition step could not affect it and hence, by assumption it must point to an agent value. If ξ^{τ} was reachable from (M, A^{1}) then there are two possible ways the value may have changed: If (AAssn) was used, then the label still points to an agent value. The other possibility was that (HAssn) was used, but this can’t happen. Why? If (HAssn) was applied to ξ^{τ} then the term H = ξ^{τ} := Ĥ appears as a subterm of A, but then, since ξ^{τ} pointed to an agent value, the host term, which must be in an embedding, is not nearly-agent free. This contradicts our assumptions about host-embeddings reachable from (M, A). Thus we conclude that any agent label reachable from (M′, A′) must point to an agent value.

(P2), (PAssn1), (PAssn2) These cases follow analogously to (P1).

(Pβ) In this case, A = (λy_{a}:τ′. A^{1}) Â. The heap doesn’t change, so let ⌜⌞H′⌝⌟_{h}^{τ} be a term reachable from (M, {Â/y_{a}}A^{1}) and suppose it is not reachable from (M, A). Since the terms changed affected by the substitution {Â/y_{a}} are exactly those containing free occurrences of y_{a}, any host-embeddings not in A must be of the form {Â/y_{a}}⌜⌞H⌝⌟t_{h}. By assumption, we have Ψ; [x_{a} : b] ⊢_{a} ⌜⌞H⌝⌟t_{h} : t, and it follows that y_{a} = x_{a} and consequently, by the Canonical Forms Lemma, Â = c for some constant c. Thus the new host-term is {c/x_{a}}⌜⌞H⌝⌟t_{h} = ⌜⌞{c/x_{a}}H⌝⌟t_{h} and hence clause 2 of the result is satisfied. Since the heap doesn’t change and labels reachable from (M′, A′) are a subset of those reachable from (M, A), the condition on agent-colored labels is also satisfied.

(Pμ1) In this case we have A = roll_{τ} A^{1} and that (M, A^{1}) ⟼ (M′, A^{2}). Since A^{1} is a subterm of A and A isn’t an embedding, it follows that any host-embeddings reachable from (M, A^{1}) are also reachable from (M, A). The result follows trivially from the inductive hypothesis.

(Pμ2), (P!), (PRef1) These follow analogously to the case for (Pμ1).

(Pμ3) The A = unroll_{μα.τ} roll_{μα.τ} A^{1}. Since the heap doesn’t change and all subterms of A^{1} are subterms of A, any host-embedding of A^{1} satisfies clause 1, while agent-colored labels still point to the same things.

(AH) Then A = ⌜⌞H⌝⌟t_{h}. Furthermore, (M, H) ⟼ (M′, H′). Since (M, H) is closed and nearly-agent free, it follows that (M, H) is agent-free. A simple argument by induction shows that agent- or host-freeness is preserved by transition steps. Thus we conclude H′ is agent-free and so clause 3 is satisfied. Since H is agent-free, any labels contained in H must point to host values and not agent values. Thus, even if H transitions via (HAssn), only locations that are already host-colored are affected. This suffices to show that the agent-colored label property still holds.

(AConst), (AHfn), (Aμ1), and (ALab) All of these cases are eliminated since all embedded host-terms that appear in A must have label t.

(ARef) Any host-embedding that is reachable from (M[ξ^{τ} ↦ (Â, a)], ξ^{τ}) is also reachable from (M, ref_{τ} Â) and so satisfies clause 1. The newly created label refers to an agent location, and by assumption all agent labels reachable from (M, Â) also point to agent values, so that part of the lemma is satisfied.

(types) τ ::= t | b | τ_{1} → τ_{2}
(labels) ℓ_{i} ::= i | ℓ_{i} : ℓ_{j}
(i-terms) e_{i} ::= x_{i} | c | λx_{i}:τ. e_{i} | e_{i} e′_{i}

| fix f_{i}(x_{i}:τ). e_{i} | ⌜⌞e_{j}⌝⌟_{ℓ_{j}}^{τ}

(i-primvals) v̂_{i} ::= c | λx_{i}:τ. e_{i}
(i-values) v_{i} ::= v̂_{i} | ⌜⌞v̂_{j}⌝⌟_{ℓ_{j}}^{t} (Δ_{i}(t) = t)

Figure 5: Multiagent Syntax

(A!) Then A = !ξ^{τ} and by assumption, we have M(ξ^{τ}) = (Â, a). From the definition of reachability, it follows that any host-embedding reachable from (M, M(ξ)) is also reachable from (M, A). Thus clause 1 is satisfied. Since any agent label reachable from (M, Â) is also reachable from (M, !ξ^{τ}) the condition on agent labels is satisfied.

(AAssn) As in (A!), all host-embeddings reachable from A′ are also reachable from A, satisfying clause 1. Also, since Â is stored as an agent value and every other agent label reachable from (M′, A′) is reachable from (M, A), the agent-label condition is met.

□

3 The Multiagent Language

So far, we have described a two-principal setting in which the host has strictly more information than the agent. Many interesting cases can be modeled in this fashion, but there are times when both principals wish to hide information or there are more than two agents involved. For example, we need a multiagent setting to prove safety properties about nested or mutually recursive abstract datatypes.

Another natural generalization is to allow an agent to export multiple abstract types. Once that has been introduced, agents should be able to share type information.

Generalizing the language these ways has another benefit: we can prove theorems once for a broad class of systems. The type abstraction properties for an instance of the system follow as corollaries.

Just as in the two-agent case it is straightforward (but tedious) to include products, sums and recursive types in the multiagent calculus. We also believe we can add state as in the two-agent case. The key technique is to record which agent last assigned to a location, and do the appropriate embedding on derefernce. However, we do not incorporate state in the development below.

3.1 Syntax

Figure 5 shows the syntax for the multiagent language. The types include a base type, b, function types, and type variables ranged over by t, u, and s.

Rather than just two “colors” of terms, we now assume that there are n agents, where n is fixed. In the syntax, the meta-variables i and j range over {1, …, n}.

Agent i’s terms include variables, x_{i}, non-recursive functions, λx_{i}:τ. e_{i}, recursive functions, fix f_{i}(x_{i}:τ). e_{i}, function applications, e_{i} e′_{i}, and embeddings ⌜⌞e_{j}⌝⌟_{ℓ_{j}}^{τ}. We include both recursive and non-recursive functions to simplify the dynamic semantics (see rule (4) in Figure 6).

An embedding containing a j-term is labeled with a list of agents beginning with j for reasons explained in the discussion of the semantics. We use the notation ℓ_{j} for a non-empty list of agents beginning with j. If ℓ_{i} and ℓ_{j} are two such lists, then ℓ_{i}:ℓ_{j} is ℓ_{i} appended to ℓ_{j} and rev(ℓ_{i}) is the list-reversal of ℓ_{i}.

The goal is a language in which each agent has limited knowledge of type information. Thus, we must somehow represent what an agent “knows” and ensure that agents sharing information do so consistently.

(1) \frac{e_{i}^{0} ⟼^{i} e_{i}^{1}}{e_{i}^{0} e_{i}^{2} ⟼^{i} e_{i}^{1} e_{i}^{2}}  (2) \frac{e_{i}^{0} ⟼^{i} e_{i}^{1}}{v_{i} e_{i}^{0} ⟼^{i} v_{i} e_{i}^{1}}  (3) \frac{e_{j}^{0} ⟼^{j} e_{j}^{1}}{⌜⌞e_{j}^{0}⌝⌟_{ℓ_{j}}^{τ} ⟼^{i} ⌜⌞e_{j}^{1}⌝⌟_{ℓ_{j}}^{τ}}

(4)  fix f_{i}(x_{i}:τ). e_{i} ⟼^{i} λx_{i}:τ. {fix f_{i}(x_{i}:τ). e_{i}/f_{i}}e_{i}
(5)  λx_{i}:τ. e_{i} v_{i} ⟼^{i} {v_{i}/x_{i}}e_{i}
(6)  ⌜⌞c⌝⌟b_{ℓ_{j}}  ⟼^{i} c
(7)  ⌜⌞v̂_{j}⌝⌟_{ℓ_{j}}^{τ} ⟼^{i} ⌜⌞v̂_{j}⌝⌟_{ℓ_{j}}^{Δ̄_{i}(τ)} (τ ≠ Δ_{i}(τ))
(8)  ⌜⌞⌜⌞v̂_{j}⌝⌟_{ℓ_{j}}^{u}⌝⌟_{ℓ_{k}}^{τ} ⟼^{i} ⌜⌞v̂_{j}⌝⌟_{ℓ_{j}:ℓ_{k}}^{τ} (u ∉ Dom(Δ_{k}), τ = Δ_{i}(τ))
(9) ⌜⌞λx_{j}:τ^{0}. e_{j}⌝⌟_{ℓ_{j}}^{τ^{1}→τ^{2}}  ⟼^{i} λx_{i}:τ^{1}. ⌜⌞{⌜⌞x_{i}⌝⌟_{i:rev(ℓ_{j})}^{τ^{0}}/x_{j}}e_{j}⌝⌟_{ℓ_{j}}^{τ^{2}} (x_{i} fresh, τ^{1} → τ^{2} = Δ_{i}(τ^{1} → τ^{2}))

Figure 6: Multiagent Dynamic Semantics: e_{i} ⟼^{i} e′_{i}

For example, agent i might know that fh = int. Agent j may or may not have this piece of information, but if j does know the realization of fh, that knowledge must be compatible with what i knows. (It shouldn’t be the case that j thinks fh = string.)

The consistency of the type information of the language is encapsulated in an “omniscient” map, Φ, that takes type variables to types. It is a finite map of the following form:

Φ::= ∅ | Φ[t = b] | Φ[t = s], s ∈ Dom(Φ) | Φ[t = s → u], s, u ∈ Dom(Φ)

Intuitively, Φ represents the “real” type alias information in the system. For instance in the situation above, Φ might be [fh = int]. In practice, Φ could be extracted from the source code of the agents and checked for consistency.

Accordingly, each principal will know some of the information contained in Φ. For each agent, i, let Δ_{i} be a subset of Dom(Φ). Each such Δ_{i} determines a map, Φ|_{Δ_{i}} obtained by restricting the domain of Φ to Δ_{i}. To simplify notation, we use Δ_{i}(t) for Φ|_{Δ_{i}}(t). Continuing the example above, we might have Δ_{i} = {fh} and Δ_{j} = {}, which says that i knows that fh is implemented as an integer while j does not. Agent i knows t means t ∈ Δ_{i}.

Note that since Δ_{i} and Δ_{j} are both restrictions of Φ, it is the case that for any t ∈ Dom(Δ_{i})∩Dom(Δ_{j}) we have Δ_{i}(t) = Δ_{j}(t). This restriction is not as prohibitive as it may appear. For example, we can encode the maps Δ_{i}(t) = s, Δ_{i}(s) = int, Δ_{j}(t) = int by rearranging the functions to be Δ_{i}(s) = t, Δ_{i}(t) = Δ_{j}(t) = int. This does not work in all cases, however, but it is sufficient to ensure Type Relations property (iii) (see Lemma 4.5)^{1}.

Each Δ_{i} extends naturally to a map from an arbitrary type τ as follows:

Δ_{i}(b) = b
Δ_{i}(t) = \{ \begin{matrix}t & t ∉ Dom(Δ_{i}) \\ Δ_{i}(t) & t ∈ Dom(Δ_{i}) \end{matrix}
Δ_{i}(τ^{1} → τ^{2}) = Δ_{i}(τ^{1}) → Δ_{i}(τ^{2})

Such a Δ_{i} determines a complete partial order, ⊑_{Δ_{i}}, on types. We denote the least upper bound of the sequence τ ⊑_{Δ_{i}} Δ_{i}(τ) ⊑_{Δ_{i}} Δ_{i}^{2}(τ) ⊑_{Δ_{i}} … by Δ̄_{i}(τ). Thus, Δ̄_{i}(τ) is the most concrete view of τ that agent i is able to determine from its knowledge. For succinctness, we write {Δ} for the set {Δ_{1}, …, Δ_{n}}.

Some key properties of these Δ maps are summarized below:

1In fact, resorting to this restrictive “omniscient” Φ is unnecessary. It is sufficient for our system to have a set of compatible Δ maps, where compatible is taken to mean that no collection of agents can relate (in the sense of Figure 8) two incompatible types (i.e. a base type and an arrow type). The Δ maps must further satisfy Lemma 3.7. The requirements on the Δ maps given here are sufficient, but not necessary to meet these requirements and can probably be considerably relaxed.

(const)  {Δ}; Γ ⊢_{i} c : b
(var)  {Δ}; Γ ⊢_{i} x_{i} : Γ(x_{i})

(app)  \frac{\{Δ\}; Γ ⊢_{i} e_{i} : τ′ → τ  \{Δ\}; Γ ⊢_{i} e′_{i} : τ′}{\{Δ\}; Γ ⊢_{i} e_{i} e′_{i} : τ}

(abs)  \frac{\{Δ\}; Γ[x_{i} : τ′] ⊢_{i} e′_{i} : τ  Δ_{i}(τ′) = τ′}{\{Δ\}; Γ ⊢_{i} λx_{i}:τ′. e′_{i} : τ′ → τ} (x_{i} ∉ Dom(Γ))

(fix)  \frac{\{Δ\}; Γ[f_{i} : τ′ → τ][x_{i} : τ′] ⊢_{i} e′_{i} : τ  Δ_{i}(τ′ → τ) = τ′ → τ}{\{Δ\}; Γ ⊢_{i} fix f_{i}(x_{i}:τ′). e′_{i} : τ′ → τ} (f_{i}, x_{i} ∉ Dom(Γ))

(embed)  \frac{\{Δ\}; Γ ⊢_{j} e_{j} : τ′  \{Δ\} ⊢ τ′ ≲_{ℓ_{j}:i} τ}{\{Δ\}; Γ ⊢_{i} ⌜⌞e_{j}⌝⌟_{ℓ_{j}}^{τ} : Δ̄_{i}(τ)}

Figure 7: Multiagent Static Semantics: {Δ}; Γ ⊢_{i} e_{i} : τ

Lemma 3.1 (Consistency) For any agents i and j and type variable t, if t ∈ Δ_{i} ∩ Δ_{j} then Δ_{i}(t) = Δ_{j}(t).

Proof: Immediate from the definition of Δ_{i} and Δ_{j}. □

Note that Δ_{i}(Δ_{j}(τ)) is not necessarily Δ_{j}(Δ_{i}(τ)).

Lemma 3.2 (Properties of Δ̄_{i}) For all agents i and types τ and τ′,

(i) Δ̄_{i}(b) = b

(ii) Δ̄_{i}(τ) = Δ̄_{i}(Δ_{i}(τ)) = Δ_{i}(Δ̄_{i}(τ))

(iii) Δ̄_{i}(τ → τ′) = Δ̄_{i}(τ) → Δ̄_{i}(τ′)

(iv) Δ̄_{i}(τ → τ′) = τ^{0} → τ^{1} for some τ^{0} and τ^{1}. In particular Δ̄_{i}(τ → τ′) ≠ b

(v) Δ̄_{i}(τ) = τ ⟺ Δ_{i}(τ) = τ

Proof: Immediate from the definition of Δ̄_{i}. □

The set of i-terms that are values depends on i’s available type information. In addition to the usual notion of values, given by i-primvals, a j-primval embedded in agent i is a value if i cannot determine any more type information about the value, i.e. ⌜⌞v̂_{j}⌝⌟_{ℓ_{j}}^{t} is a value if Δ_{i}(t) = t.

3.2 Dynamic Semantics

Figure 6 shows the operational semantics for agent i in the multiagent language.

Rules (1), (2), (4) and (5) establish a typical call-by-value semantics. Rule (3) allows evaluation inside embeddings and distinguishes i transitions from j transitions.

Rule (6) lets agent i pull a constant, exported at base type, out of an embedding. It corresponds to rules (A2) and (H2) of the two-agent scenario.

As in the two-agent case where the host had more type information than the agent, an agent can use its knowledge to refine the type of an embedded term. Previously, the substitution {τ_{h}/t} in rule (H3) served this purpose. Now, Δ̄_{i} captures the type refinement information available to agent i. Correspondingly, rule (7) allows i to refine the type of an embedded value.

Perhaps the most subtle issue is when to allow embeddings to be stripped away. In the two-agent case, rule (H4) let the host pull out its own value that had been embedded abstractly inside an agent. This was safe because the agent had strictly less information than the host. Now, however, an intermediary agent with more knowledge could contribute to the evaluation of a term. If we throw away that information by simply discarding the intermediary’s embedding brackets, it becomes difficult to track the relationship between the type of the term inside the embedding and the annotation on the embedding.

Thus we use lists of agents as the labels on embeddings. Intuitively, an agent “signs” the term if it participated in the evaluation. Rule (8) says that if there are nested embeddings, ⌜⌞⌜⌞v̂_{j}⌝⌟_{ℓ_{j}}^{u}⌝⌟_{ℓ_{k}}^{τ}, and the inner embedding, ⌜⌞v̂_{j}⌝⌟_{ℓ_{j}}^{u}, is a k-value (that is, u ∉ Dom(Δ_{k})), then the two embeddings can be collapsed into one, ⌜⌞v̂_{j}⌝⌟_{ℓ_{j}:ℓ_{k}}^{τ}. We lose no information about which agents have participated in the evaluation of the term, because we append the two lists. The idea, formalized in the next section, is that the type of the term inside an embedding is related, via the list of agents labeling the embedding, to the type annotation.

The most interesting rule is (9), which is really what tracks the principals. The embedded function is lifted to the outside. Its argument now belongs to the outer agent, i, instead of the inside agent, j. As such, it must be given the type that i thinks the argument should have. The body of the function is still a j-term embedded in an i-term so any occurrence of the new formal argument x_{i} must be embedded as an i-term inside a j-term. The corresponding type annotation must be the type which j expects the argument to have. Hence the function body is still abstract to i and when the function is applied, the actual argument will be held abstract from j. The only remaining issue is the agent list on the formal argument embeddings. Since the “inside type” and “outside type” have reversed roles, the agent-list must be in reverse order. Intuitively, the agents which successively provided the function argument type to i must undo their work in the body of the function which is a j-term.

3.3 Static Semantics

Figure 7 shows the multiagent static semantics. The rules are parameterized by the agent i. The judgment {Δ}; Γ ⊢_{i} e_{i} : τ should be read as, “Under type-maps Δ_{1}, …, Δ_{n} in context Γ, agent i can show that e_{i} has type τ”.

All of the rules except (embed) are essentially standard. The rules (abs) and (fix) have additional conditions that force an agent to use the most concrete type available for functions internal to the agent.

As alluded to previously, the issue of consistency between agents arises during type checking. For instance, we don’t want an agent to export an int as a function. Likewise, we don’t want an agent, or collection of agents, to violate the type abstractions represented by the Δ_{i}’s. Thus we need some way of relating the type of the expression inside the embedding to the typing annotation on the embedding.

We establish an agent-list indexed family of relations on types, τ ≲_{ℓ_{i}} τ′. Judgments of the form {Δ} ⊢ τ ≲_{ℓ_{i}} τ′, showing when two types may be related by the list ℓ_{i}, are given in Figure 8. These rules say that τ^{0} ≲_{i_{1}:i_{2}:...:i_{n}} τ^{n} if there exist types τ^{1}, …, τ^{n−1} such that agent i_{k} is able to show that τ^{k−1} = τ^{k} for k ∈ {1, …, n}. Informally, the agents are able to chain together their knowledge of type information to show that τ^{0} = τ^{n}.

The (embed) rule uses the ≲_{ℓ_{j}:i} relation to ensure that the type inside the embedding matches up with the annotation on the embedding. The agent i is appended to the list because, as the outermost agent, i is implicitly involved in evaluation of the term.

Why is this somewhat complicated mechanism necessary? To some extent, it’s not. It is clear that there must be some way of relating the type of a term inside an embedding to the type annotation on the embedding; otherwise, for example, an agent could export an integer as a string. We could have chosen to allow nested embeddings to be values, so long as each inner embedding was a value with respect to the enclosing agent (for example ⌜⌞⌜⌞3⌝⌟t_{i}⌝⌟s_{j} would be a k-value if s ∉ Dom(Δ_{k}) and t ∉ Dom(Δ_{j})). This allows embeddings to “pile up” in a way that is difficult to deal with syntactically and that complicates the dynamic semantics.

Instead, we allow rule (8) to collapse two embeddings and push the work of ensuring compatibility onto the ≲_{ℓ_{i}} relation. The lists contain all of the agents that have participated in the evaluation of the inner value because inconsistencies might arise otherwise. Consider three agents, i, j, and k such that Δ_{i}(t) = int, Δ_{j}(s) = t and Δ_{k} = ∅. Then collapsing the properly typed k-term ⌜⌞⌜⌞3⌝⌟t_{i}⌝⌟s_{j} to either ⌜⌞3⌝⌟s_{i} or ⌜⌞3⌝⌟s_{j} violates the type abstraction properties since neither i nor j knows that s abstracts an int. Alternately, if we were to use sets of agents, instead of (ordered) lists, the reasonable typing rules become too permissive.

(eq)  \frac{Δ̄_{i}(τ) = Δ̄_{i}(τ′)}{\{Δ\} ⊢ τ ≲_{i} τ′}

(trans) \frac{\{Δ\} ⊢ τ′ ≲_{ℓ_{i}} τ′′ \{Δ\} ⊢ τ′′ ≲_{ℓ_{j}} τ′}{\{Δ\} ⊢ τ ≲_{ℓ_{i}:ℓ_{j}} τ′}
Figure 8: Type relations: {Δ} ⊢ τ ≲_{ℓ_{i}} τ′

3.4 Type Soundness

We first need to prove several properties about related types. We can then follow a traditional approach to syntactic type soundness.

3.4.1 Type Relation Lemmas

Given the collection of Δ’s, we can construct a graph, with edges colored by agents, that captures the relation between types. In particular, let G({Δ}) = (V, E) where V, the vertices, is just the set of all types and E is a set of colored edges. For each agent i and types τ and τ′ there is an edge (τ, τ′)_{i} ∈ E if and only if either τ = τ′, Δ_{i}(τ) = τ′, or Δ_{i}(τ′) = τ. These edges are undirected, and the notation (τ, τ′)_{i} indicates that there is an i-colored edge from τ to τ′. Wherever {Δ} is clear from the context or unimportant, we write G instead of G({Δ}).

Given such a graph, G, a path of length k in the graph from τ to τ′ is a sequence of k edges in E (τ^{0}, τ^{1})_{i_{0}}, (τ^{1}, τ^{2})_{i_{1}},…,(τ^{k−1}, τ^{k})_{i_{k−1}} where τ^{0} = τ and τ^{k} = τ′ and i_{m} is an agent for each m. Since we will be concerned with paths with particular properties, we also define the notion of an i_{0}^{x_{0}}, i_{1}^{x_{1}}, …, i_{k}^{x_{k}}-path from τ to τ′. If x_{m} ≥ 0 is an integer for each m ∈ {1 … k}, and i_{m} is an agent for each m ∈ {1 … k} then an i_{0}^{x_{0}}, i_{1}^{x_{1}}, …, i_{k}^{x_{k}}-path from τ to τ′ is a path from τ to τ′ such that the first x_{0} edges are labeled by agent i_{0}, the next x_{1} edges are labeled i_{1}, etc. Similarly, we define a simple path labeled i in G to be a path where all the edges are labeled by the single agent i, in other words, an i^{x}-path.

Lemma 3.3 (Reflexivity of ≲) For every τ and ℓ_{i}, {Δ} ⊢ τ ≲_{ℓ_{i}} τ.

Proof: Proof by induction on the length of ℓ_{i}. If |ℓ_{i}| = 1 then ℓ_{i} = i. By definition, Δ̄_{i}(τ) = Δ̄_{i}(τ), so by the (eq) rule, we have {Δ} ⊢ τ ≲_{i} τ. In the inductive case, |ℓ_{i}| > 1, so ℓ_{i} = i, ℓ_{j}. By the inductive hypothesis, {Δ} ⊢ τ ≲_{ℓ_{j}} τ and {Δ} ⊢ τ ≲_{i} τ. By the (trans) rule (instantiated with τ), the result follows.

□

Lemma 3.4 (Idempotency in Lists) For all τ, τ′, agents i, and (possibly empty) lists ℓ and ℓ′:

i {Δ} ⊢ τ ≲_{i:i} τ′ iff {Δ} ⊢ τ ≲_{i} τ′.

ii For all agents lists of the form ℓ:i:i:ℓ′, {Δ} ⊢ τ ≲_{ℓ:i:i:ℓ′} τ′ iff {Δ} ⊢ τ ≲_{ℓ:i:ℓ′} τ′

Proof: Part (i): Assume {Δ} ⊢ τ ≲_{i:i} τ′ then there must exist a τ′′ such that {Δ} ⊢ τ ≲_{i} τ′′ and {Δ} ⊢ τ′′ ≲_{i} τ′. These can be derived only by using the (eq) rule, so we have Δ̄_{i}(τ) = Δ̄_{i}(τ′′) = Δ̄_{i}(τ), so by another application of (eq), {Δ} ⊢ τ ≲_{i} τ′. Conversely, assume {Δ} ⊢ τ ≲_{i} τ′. Then Δ̄_{i}(τ) = Δ̄_{i}(τ′). It follows by the (trans) rule by instantiating τ′′ with τ that {Δ} ⊢ τ ≲_{i:i} τ′. Part (ii): By induction on |ℓ| + |ℓ′|. The base case, 0, is part (i). For the inductive case, in either direction, the derivation must end with (trans). If this rule “splits” the agent list anywhere but “between i : i”, then the result is immediate from the inductive hypothesis and (trans). So consider the case where the “split” for the forward direction of the iff is ℓ : i and i : ℓ′. It can be shown by induction on the derivation that there must exist some τ^{3} such that {Δ} ⊢ τ′′ ≲_{i} τ^{3} and {Δ} ⊢ τ^{3} ≲_{ℓ′} τ′. This allows us to “move the split” by using (trans) with ℓ : i and i, then a second time with ℓ′, reducing us to a previous case. □

Lemma 3.5 (Simple Paths) If Δ̄_{i}(τ) = τ′ then there is a simple path labeled i from τ to τ′ in G.

Proof: From the definition of Δ̄_{i}(τ) there exists a k such that Δ_{i}^{k}(τ) = τ′. By induction on k it is easy to construct a simple path of length k labeled i in G. □

Lemma 3.6 (Type Relations are Paths) Let {Δ} be a consistent set of type maps and let ℓ_{i} = i_{0} : i_{1} : …: i_{k}, where i_{0} = i, be a list of agents. Then for all τ and τ′, {Δ} ⊢ τ ≲_{ℓ_{i}} τ′ if and only if there are non-negative integers x_{0}, x_{1}, …, x_{k} such that there is an i_{0}^{x_{0}}, i_{1}^{x_{1}}, …, i_{k}^{x_{k}}- path from τ to τ′ in G({Δ}).

Proof: Assume that {Δ} ⊢ τ ≲_{ℓ_{i}} τ′. We proceed by induction on the derivation of this fact. If the last step in the derivation was (eq) then ℓ_{i} = i and we have Δ̄_{i}(τ) = Δ̄_{i}(τ′). From the Simple Paths lemma, there is an i^{n}-path from τ to Δ̄_{i}(τ) and an i^{m}-path from τ′ to Δ̄_{i}(τ′). Since they are equal, there is an i^{n+m}-path from τ to τ′. If the last step of the derivation was (trans) then ℓ_{i} = ℓ′_{i} : ℓ_{j} for some ℓ′_{i} = i_{0} : i_{1} : …, i_{m} and ℓ_{j} = i_{m+1} : …: i_{k} and there exists a τ′′ such that {Δ} ⊢ τ ≲_{ℓ′_{i}} τ′′ and {Δ} ⊢ τ′′ ≲_{ℓ_{j}} τ′. By the inductive hypothesis, there is an i_{0}^{x_{0}}, i_{1}^{x_{1}}, …, i_{m}^{x_{m}}-path from τ to τ′′ and an i_{m+1}^{x_{m+1}}, …, i_{k}^{x_{k}}-path from τ′′ to τ′. By concatenating these paths, we get an i_{0}^{x_{0}}, i_{1}^{x_{1}}, …, i_{k}^{x_{k}}-path from τ to τ′.

Conversely, assume there is an i_{0}^{x_{0}}, i_{1}^{x_{1}}, …, i_{k}^{x_{k}}-path from τ to τ′. We prove by induction on the length of the path, len = ∑_{m=0}^{k} x_{m}, that {Δ} ⊢ τ ≲_{ℓ_{i}} τ′. For the base case, len = 0. Then it must be that τ = τ′. So by reflexivity of ≲, we are done. For the inductive case, len > 0. Let e be the first edge in the path. It belongs to some agent i_{m} and connects τ with some τ′′. By the definition of G({Δ}) and Lemma 3.2(ii), Δ̄_{i_{m}}(τ) = Δ̄_{i_{m}}(τ′′). So by (eq), τ ≲_{i_{m}} τ′′. By reflexivity of ≲, we know τ ≲_{i_{0}:...:i_{m−1}} τ. Furthermore, there is an i_{m}^{x_{m}−1}, i_{m+1}, … i_{k}-path from τ′′ to τ′. So by the inductive hypothesis, τ′′ ≲_{i_{m}:...:i_{k}} τ′. By two invocations of (trans), τ ≲_{i_{0}:...:i_{m}:i_{m}:...:i_{k}} τ′. By idempotency, we are done.

□

Lemma 3.7 (Type Relations) For all agents i and j and types τ^{0}, τ^{1}, τ^{2} and τ^{3}:

i If {Δ} ⊢ Δ̄_{i}(τ^{0}) ≲_{ℓ_{i}} τ^{1} then {Δ} ⊢ τ^{0} ≲_{ℓ_{i}} τ^{1}.

ii If {Δ} ⊢ τ^{0} ≲_{ℓ_{i}} τ^{1} then {Δ} ⊢ τ^{1} ≲_{rev(ℓ_{i})} τ^{0} where rev(ℓ_{i}) means reverse(ℓ_{i}).

iii If {Δ} ⊢ τ^{0} → τ^{1} ≲_{ℓ_{i}} τ^{2} → τ^{3} then {Δ} ⊢ τ^{0} ≲_{ℓ_{i}} τ^{2} and {Δ} ⊢ τ^{1} ≲_{ℓ_{i}} τ^{3}.

Proof: Unless mentioned otherwise, the proof in each case proceeds by induction on the derivation that {Δ} ⊢ τ ≲_{ℓ_{i}} τ′.

i If the last rule in the derivation was (eq) then ℓ_{i} = i and Δ̄_{i}(Δ̄_{i}(τ^{0})) = Δ̄_{i}(τ^{1}), but since Δ̄_{i}(τ^{0}) = Δ̄_{i}(Δ̄_{i}(τ^{0})), we also conclude that Δ̄_{i}(τ^{0}) = Δ̄_{i}(τ^{1}). The result follows via the (eq) rule. Otherwise, the last rule must have been (trans), so ℓ_{i} = ℓ′_{i}:ℓ_{j} for some ℓ′_{i} and ℓ_{j} and there exists a τ′′ such that {Δ} ⊢ Δ̄_{i}(τ^{0}) ≲_{ℓ′_{i}} τ′′ and {Δ} ⊢ τ′′ ≲_{ℓ_{j}} τ^{1}. By the inductive hypothesis, we have {Δ} ⊢ τ^{0} ≲_{ℓ′_{i}} τ′′ so by an application of the (trans) rule, the result follows.

ii If the last rule of the derivation was (eq) then ℓ_{i} = i and Δ̄_{i}(τ^{0}) = Δ̄_{i}(τ^{1}) Since rev(ℓ_{i}) = rev(i) = i, the result holds by another application of (eq). Otherwise the last rule in the derivation is (trans), in which case ℓ_{i} = ℓ′_{i}:ℓ_{j} and there exists a τ′′ such that {Δ} ⊢ τ^{0} ≲_{ℓ′_{i}} τ′′ and {Δ} ⊢ τ′′ ≲_{ℓ_{j}} τ^{1}. Two applications of the inductive hypothesis yield {Δ} ⊢ τ^{1} ≲_{rev(ℓ_{j})} τ′ and {Δ} ⊢ τ′ ≲_{rev(ℓ′_{i})} τ^{0}. Since rev(ℓ_{i}) = rev(ℓ′_{i} : ℓ_{j}) = rev(ℓ_{j}), rev(ℓ′_{i}), by the (trans) rule we have the desired result.

iii Assume {Δ} ⊢ τ^{0} → τ^{1} ≲_{ℓ_{i}} τ^{2} → τ^{3}. If the last rule used in the derivation was (eq) then ℓ_{i} = i and we have Δ̄_{i}(τ^{0} → τ^{1}) = Δ̄_{i}(τ^{2} → τ^{3}). It follows from the definition of Δ̄_{i} that Δ̄_{i}(τ^{0}) = Δ̄_{i}(τ^{2}) and Δ̄_{i}(τ^{1}) = Δ̄_{i}(τ^{3}). Thus by two applications of (eq), the result follows. Otherwise the last rule used in the derivation was (trans), in which case ℓ_{i} = ℓ′_{i} : ℓ_{j} from some ℓ′_{i} and ℓ_{j}. Also, there exists a type τ such that {Δ} ⊢ τ^{0} → τ^{1} ≲_{ℓ′_{i}} τ and {Δ} ⊢ τ ≲_{ℓ_{j}} τ^{2} → τ^{3}. There are two cases, depending on whether τ = τ′ → τ′′ or τ = t.

In the first case, the inductive hypothesis immediately yields {Δ} ⊢ τ^{0} ≲_{ℓ′_{i}} τ′ and {Δ} ⊢ τ′ ≲_{ℓ_{j}} τ^{2}, so by using the (trans) rule, we conclude {Δ} ⊢ τ^{0} ≲_{ℓ′_{i}:ℓ_{j}} τ^{2}. Similar reasoning shows that {Δ} ⊢ τ^{1} ≲_{ℓ′_{i}:ℓ_{j}} τ^{3}.

We now show that the second case need not occur. It suffices to show that if there is an i_{0}^{x_{0}}, …, i_{m}^{x_{m}}- path from τ^{0} → τ^{1} to τ^{2} → τ^{3}, then there exists an i_{0}^{x_{0}}, …, i_{m}^{x_{m}}-path from τ^{0} → τ^{1} to τ^{2} → τ^{3} that has no variable nodes. This is sufficient: If the new “no-variable” path has no nodes other than τ^{0} → τ^{1} and τ^{2} → τ^{3} then there is a one-edge path and we can just use (eq). Else there is an intermediate node τ^{4} → τ^{5} and we split the path into “before” and “after” the first time this node is reached. By Relations are Paths, we are now in the first case.

Now suppose t is the first variable encountered on the original path. We know that the node in the path before the first t occurrence is some τ^{6} → τ^{7}. Also, we know the path must eventually reach another arrow type node (since it ends at one). We show that the next arrow type node reached must be τ^{6} → τ^{7}. Assume for contradiction the next arrow type node reached is different. Then there is a variable-only path in G({Δ}) from t to some other arrow type node. Then there is a cycle-free path to the other node. This path must have interior nodes which are distinct variables t_{1}, …, t_{n}. But the definition of G({Δ}) and consistency demand that Φ(t_{1}) = t since Φ(t) = τ^{6} → τ^{7}. Similarly, it must be that Φ(t_{2}) = t_{1} and so on inductively. But then Φ(t_{n}) = t_{n−1}. This means an edge from t_{n} to an arrow node must violate consistency. Contradiction.

Since the path must cycle from τ^{6} → τ^{7}, we can eliminate all edges in-between (and just take the selfloop instead). Hence we can remove the first occurrence of a variable node from the path. Inductively, we can remove all variables.

□

3.4.2 Preservation and Progress

Lemma 3.8 (Canonical Forms) If {Δ}; ∅ ⊢_{i} v_{i} : τ then:

• If τ = b, then v_{i} = c.

• If τ = τ^{1} → τ^{2}, then v_{i} = λx_{i}:τ^{1}. e_{i} for some x_{i} and e_{i}.

• If τ = t, then t ∉ Δ_{i} and v_{i} = ⌜⌞v̂_{j}⌝⌟_{ℓ_{j}}^{t} for some v̂_{j} and ℓ_{j}.

Proof: By inspection of the static semantics, the form of values, and Lemma 3.2. □

Lemma 3.9 (Concreteness of Types) For any i, if {Δ}; Γ ⊢_{i} e_{i} : τ then τ = Δ_{i}(τ).

Proof: Easily shown induction on the derivation that {Δ}; Γ ⊢_{i} e_{i} : τ, using Lemma 3.2 as necessary. □

Lemma 3.10 (Substitution) For all agents i and j, if {Δ}; Γ[x_{j} : τ′] ⊢_{i} e_{i} : τ and {Δ}; Γ ⊢_{j} e_{j} : τ′, then {Δ}; Γ ⊢_{i} {e_{j}/x_{j}}e_{i} : τ.

Proof: By induction on the typing derivation for {Δ}; Γ[x_{j} : τ′] ⊢_{i} e_{i} : τ. There are several cases, depending on the last rule applied in the derivation:

(const) Immediate since substitution has no effect and x_{j} ∉ F V (c).

(var) Then e_{i} = x_{i} for some x_{i} and there are two possibilities:

x_{i} ≠ x_{j} Then {e_{j}/x_{j}}x_{i} = x_{i} and by strengthening (since x_{j} ∉ F V (x_{i})) and the assumptions,

{Δ}; Γ ⊢_{i} x_{i} : τ. x_{i} = x_{j} Then i = j and {e_{j}/x_{j}}x_{j} = e_{j}. By (var), τ′ = τ. The result follows.

(app) Then e_{i} = e′_{i} e′′_{i} for some e′_{i} and e′′_{i} and {Δ}; Γ[x_{j} : τ′] ⊢_{i} e′_{i} : τ′′ → τ and {Δ}; Γ[x_{j} : τ′] ⊢_{i} e′′_{i} : τ′. By two applications of the inductive hypothesis, we also have {Δ}; Γ ⊢_{i} {e_{j}/x_{j}}e′_{i} : τ′′ → τ and {Δ}; Γ ⊢_{i} {e_{j}/x_{j}}e′′_{i} : τ′′. The result follows by (app) and the definition of substitution.

(abs) Then it must be that e_{i} = λx_{i}:τ^{2}. e′_{i} and τ = τ^{2} → τ^{3}, for some x_{i}, e′_{i}, τ^{2}, and τ^{3}. Furthermore, it must be the case that {Δ}; Γ[x_{j} : τ′][x_{i} : τ^{2}] ⊢_{i} e′_{i} : τ^{3}. By the bound variable convention, x_{j} ≠ x_{i}, so {e_{j}/x_{j}}λx_{i}:τ^{2}. e′_{i} = λx_{i}:τ^{2}. {e_{j}/x_{j}}e′_{i}. The inductive hypothesis yields {Δ}; Γ[x_{i} : τ^{2}] ⊢_{i} {e_{j}/x_{j}}e′_{i} : τ^{3}, and we conclude via the (abs) rule that {Δ}; Γ ⊢_{i} λx_{i}:τ^{2}. {e_{j}/x_{j}}e′_{i} : τ^{2} → τ^{3}. The result follows from the definition of substitution.

(fix) Argument is completely analogous to previous case.

(embed) Then e_{i} = ⌜⌞e_{k}⌝⌟_{ℓ_{k}}^{τ^{2}} for some k, e_{k}, ℓ_{k} and τ^{2}. Furthermore, it must be the case that {Δ}; Γ[x_{j} : τ′] ⊢_{k} e_{k} : τ^{3}, {Δ} ⊢ τ^{3} ≲_{ℓ_{k}:i} τ^{2}, and τ = Δ̄_{i}(τ^{2}) for some τ^{3}. By the inductive hypothesis, {Δ}; Γ ⊢_{k} {e_{j}/x_{j}}e_{k} : τ^{3}, so by the (embed) rule we conclude that {Δ}; Γ ⊢_{i} ⌜⌞{e_{j}/x_{j}}e_{k}⌝⌟_{ℓ_{k}}^{τ^{2}} : τ. The result follows from the definition of substitution.

□

Lemma 3.11 (Preservation) For all agents i, if {Δ}; ∅ ⊢_{i} e_{i} : τ and e_{i} ⟼^{i} e′_{i} then {Δ}; ∅ ⊢_{i} e′_{i} : τ.

Proof: By induction on the derivation that e_{i} ⟼^{i} e′_{i}. The interesting cases are (7), (8), and (9). Rules (1), (2), (3) follow directly from the inductive hypothesis and the static semantics. Rules (4) and (5) follow from the Substitution Lemma (which applies because of Concreteness of Types) along with the (abs) and (fix) rules. Rule (6) follows directly from the static semantics. We consider the other cases separately:

(7) Since e_{i} typechecks, we must have a derivation as follows:

(embed) \frac{\{Δ\}; ∅ ⊢_{j} v̂_{j} : τ^{0} \{Δ\} ⊢ τ^{0} ≲_{ℓ_{j}:i} u}{\{Δ\}; ∅ ⊢_{i} ⌜⌞v̂_{j}⌝⌟_{ℓ_{j}}^{u} : Δ̄_{i}(u)}

Since Δ̄_{i}(u) equals Δ̄_{i}(Δ_{i}(u)), we have via the (eq) rule that {Δ} ⊢ u ≲_{i} Δ̄_{i}(u). Thus by (trans) it follows that {Δ} ⊢ τ^{0} ≲_{ℓ_{j}:i:i} Δ̄_{i}(u) and we can remove the second i by idempotency. We can now derive:

(embed) \frac{\{Δ\}; ∅ ⊢_{j} v̂_{j} : τ^{0} \{Δ\} ⊢ τ^{0} ≲_{ℓ_{j}:i} Δ̄_{i}(u)}{\{Δ\}; ∅ ⊢_{i} ⌜⌞v̂_{j}⌝⌟_{ℓ_{j}}^{Δ̄_{i}(u)} : Δ̄_{i}(u)}

The conclusion is the desired result.

(8) Since e_{i} typechecks, we must have a derivation as follows:

(embed) \frac{(embed) \frac{\{Δ\}; ∅ ⊢_{j} v̂_{j} : τ^{0} \{Δ\} ⊢ τ^{0} ≲_{ℓ_{j},k} u}{\{Δ\}; ∅ ⊢_{k} ⌜⌞v̂_{j}⌝⌟_{ℓ_{j}}^{u} : Δ̄_{k}(u)}  \{Δ\} ⊢ Δ̄_{k}(u) ≲_{ℓ_{k},i} τ}{\{Δ\}; ∅ ⊢_{i} ⌜⌞⌜⌞v̂_{j}⌝⌟_{ℓ_{j}}^{u}⌝⌟_{ℓ_{k}}^{τ} : Δ̄_{i}(τ)}

Furthermore, u ∉ Δ_{k}, so Δ̄_{k}(u) = u. Thus by using the (trans) rule, we have {Δ} ⊢ τ^{0} ≲_{ℓ_{j}:k:ℓ_{k}:i} τ. And since ℓ_{k} begins with agent k, idempotency proves that {Δ} ⊢ τ^{0} ≲_{ℓ_{j}:ℓ_{k}:i} τ, which yields the following derivation:

(embed) \frac{\{Δ\}; ∅ ⊢_{j} v̂_{j} : τ^{0} \{Δ\} ⊢ τ^{0} ≲_{ℓ_{j}:ℓ_{k}:i} τ}{\{Δ\}; ∅ ⊢_{i} ⌜⌞v̂_{j}⌝⌟_{ℓ_{j}:ℓ_{k}}^{τ} : Δ̄_{i}(τ)}

The conclusion is the desired result.

(9) Since e_{i} typechecks, we must have a derivation as follows:

(embed) \frac{(abs) \frac{\{Δ\}; [x_{j} : τ^{0}] ⊢_{j} e_{j} : τ^{3} Δ_{j}(τ^{0}) = τ^{0}}{\{Δ\}; ∅ ⊢_{j} λx_{j}:τ^{0}. e_{j} : τ^{0} → τ^{3}}  \{Δ\} ⊢ τ^{0} → τ^{3} ≲_{ℓ_{j}:i} τ^{1} → τ^{2}}{\{Δ\}; ∅ ⊢_{i} ⌜⌞λx_{j}:τ^{0}. e_{j}⌝⌟_{ℓ_{j}}^{τ^{1}→τ^{2}} : Δ̄_{i}(τ^{1} → τ^{2})}

Since the side condition gives us that, Δ_{i}(τ^{1} → τ^{2}) = τ^{1} → τ^{2}, we know from the definition of Δ_{i} that Δ̄_{i}(τ^{1}) = Δ_{i}(τ^{1}) = τ^{1} and similarly for τ^{2}. From the Type Relations Lemma and the right hand premise of the (embed) step, we conclude that {Δ} ⊢ τ^{0} ≲_{ℓ_{j}:i} τ^{1} and {Δ} ⊢ τ^{3} ≲_{ℓ_{j}:i} τ^{2}. Now notice that the reverse of ℓ_{j} : i is i :reverse(tail(ℓ_{j})):j which we shall write ℓ′ : j. So by the Type Relations Lemma, {Δ} ⊢ τ^{1} ≲_{ℓ′:j} τ^{0}. Thus we can derive:

(embed) \frac{(var) \{Δ\}; [x_{i} : τ^{1}] ⊢_{i} x_{i} : τ^{1}  \{Δ\} ⊢ τ^{1} ≲_{ℓ′:j} τ^{0}}{\{Δ\}; [x_{i} : τ^{1}] ⊢_{j} ⌜⌞x_{i}⌝⌟_{ℓ′}^{τ^{0}} : Δ̄_{j}(τ^{0})}

In fact, {Δ}; [x_{i} : τ^{1}] ⊢_{j} ⌜⌞x_{i}⌝⌟_{ℓ′}^{τ^{0}} : τ^{0} since the original derivation above provides Δ_{j}(τ^{0}) = τ^{0}. It also provides {Δ}; [x_{j} : τ^{0}] ⊢_{j} e_{j} : τ^{3}. Since x_{i} is fresh, we may conclude {Δ}; [x_{i} : τ^{1}][x_{j} : τ^{0}] ⊢_{j} e_{j} : τ^{3}. So by the substitution lemma, {Δ}; [x_{i} : τ^{1}] ⊢_{j} {⌜⌞x_{i}⌝⌟_{ℓ′}^{τ^{0}}/x_{j}}e_{j} : τ_{3}. Thus we can derive:

(abs) \frac{(embed) \frac{\{Δ\}; [x_{i} : τ^{1}] ⊢_{j} \{⌜⌞x_{i}⌝⌟_{ℓ′}^{τ^{0}}/x_{j}\}e_{j} : τ_{3} \{Δ\} ⊢ τ^{3} ≲_{ℓ_{j}:i} τ^{2}}{\{Δ\}; [x_{i} : τ^{1}] ⊢_{i} ⌜⌞\{⌜⌞x_{i}⌝⌟_{ℓ′}^{τ^{0}}/x_{j}\}e_{j}⌝⌟_{ℓ_{j}}^{τ^{2}} : Δ̄_{i}(τ^{2})}  Δ_{i}(τ^{1}) = τ^{1}}{\{Δ\}; ∅ ⊢_{i} λx_{i}:τ^{1}. ⌜⌞\{⌜⌞x_{i}⌝⌟_{ℓ′}^{τ^{0}}/x_{j}\}e_{j}⌝⌟_{ℓ_{j}}^{τ^{2}} : τ^{1} → Δ̄_{i}(τ^{2})}

Since Δ̄_{i}(τ^{2}) = τ^{2}, the conclusion is the desired result.

□

Lemma 3.12 (Progress) For all i, if {Δ}; ∅ ⊢_{i} e_{i} : τ then either e_{i} is some value, v_{i}, or there exists an e′_{i} such that e_{i} ⟼^{i} e′_{i}.

Proof: By induction on the structure of e_{i}. There are several cases:

e_{i} = x_{i} This case is impossible since {Δ}; ∅ ⊬_{i} x_{i} : τ for any τ.

e_{i} = c Since c is a value, we are done.

e_{i} = λx_{i}:τ^{0}. e′_{i} Again, e_{i} is a value, so the lemma holds.

e_{i} = fix f_{i}(x_{i}:τ^{0}). e′_{i} Rule (4) applies, so we can take a step.

e_{i} = e_{i}^{0}e_{i}^{2} By the inductive hypothesis, e_{i}^{0} is either a value or there exists some e_{i}^{1} such that e_{i}^{0} ⟼^{i} e_{i}^{1}. If the latter holds, then by operational semantics rule (1) we have e_{i} ⟼^{i} e_{i}^{1} e_{i}^{2}. Otherwise, e_{i}^{0} is a value, v_{i}, and another application of the inductive hypothesis gives us that e_{i}^{2} is either a value or there exists e_{i}^{1} such that e_{i}^{2} ⟼^{i} e_{i}^{1}. In the second case, rule (2) applies so e_{i} takes a step. The remaining case is when e_{i}^{0} = v_{i} and e_{i}^{2} = v′_{i} for some values v_{i} and v′_{i}. Because e_{i} is well typed, Canonical Forms guarantees that v_{i} = λx_{i}:τ′. e′_{i} for some e′_{i}. Thus rule (5) of the operational semantics applies, and e_{i} takes a step.

e_{i} = ⌜⌞e_{j}⌝⌟_{ℓ_{j}}^{τ^{1}} By the well typing of e_{i}, the last rule used in the typing derivation must have been (embed). Thus we have {Δ}; ∅ ⊢_{j} e_{j} : τ^{0} and {Δ} ⊢ τ^{0} ≲_{ℓ_{j}:i} τ^{1}. Then by the inductive hypothesis, e_{j} is either a value or there is some e′_{j} such that e_{j} ⟼^{i} e′_{j}. In the latter case, rule (3) of the operational semantics applies, and we conclude that e_{i} takes a step. The other possibility is that e_{j} = v_{j} for some value v_{j}. By the Canonical Forms lemma, there are three cases based on τ^{0}.

\underline{x_{i}} = x
\underline{c} = c
\underline{λx_{i}:τ. e_{i}} = λx:\overline{Φ}(τ). \underline{e_{i}}
\underline{fix f_{i}(x_{i}:τ). e_{i}} = fix f(x:\overline{Φ}(τ)). \underline{e_{i}}
\underline{e_{i}^{1} e_{i}^{2}} = \underline{e_{i}^{1}} \underline{e_{i}^{2}}
\underline{⌜⌞e_{j}⌝⌟_{ℓ_{j}}^{τ}} = \underline{e_{j}}

Figure 9: Definition of Erasure \underline{e_{i}}

τ^{0} = t Then v_{j} = ⌜⌞v̂_{k}⌝⌟_{ℓ_{k}}^{t} and t ∉ Δ_{j} for some v̂_{k} and ℓ_{k}, so by rule (8), e_{i} takes a step to ⌜⌞v̂_{k}⌝⌟_{ℓ_{k}:ℓ_{j}}^{τ^{1}}.

τ^{0} = b Then v_{j} = c. If τ^{1} = b then e_{i} ⟼^{i} c by rule (6) of the operational semantics. The only other possibility is that τ^{1} = t for some type variable t (otherwise e_{i} wouldn’t typecheck). If t ∈ Δ_{i} then rule (7) applies and e_{i} ⟼^{i} ⌜⌞v̂_{j}⌝⌟_{ℓ_{j}}^{Δ̄_{i}(t)}, otherwise e_{i} is the value ⌜⌞c⌝⌟_{ℓ_{j}}^{t}.

τ^{0} = τ^{2} → τ^{3} Then v_{j} = λx_{j}:τ^{2}. e′_{j}. If Δ_{i}(τ^{1}) ≠ τ^{1}, then rule (7) applies. Else if τ^{1} = t then e_{i} is a value. Else τ^{1} is a most-concrete arrow type, so rule (9) applies.

□

Definition 3.13 (Stuck Term) A term e_{i} is stuck if there does not exist a term e′_{i} such that e_{i} ⟼^{i} e′_{i}.

Theorem 3.14 (Type Safety) If {Δ}; ∅ ⊢_{i} e_{i} : τ then there is no stuck e′_{i} such that e_{i} ⟼^{i}^{∗} e′_{i}.

Proof: Follows directly from the Preservation and Progress Lemmas. □

3.4.3 Erasure

We use embeddings to prove safety properties such as those in the next section, but the cost seems to be dynamic rules (3), (6), (7), (8), and (9). Worse yet, in a language with recursion, agent lists might grow arbitrarily large. This section essentially shows that embeddings are only a proof technique. If a program evaluates to a constant, we can simply erase all embeddings and the program will still evaluate to the same constant.

More formally, we establish equivalence with the simply-typed λ-calculus by showing that embeddingerasure commutes with evaluation and constants correspond to constants. The target language has no embeddings and its semantics includes exactly those rules of the source language which do not explicitly mention embeddings, namely (1), (2), (4), and (5). Let \underline{e_{i}} mean the erasure of e_{i}. Let ⟼^{−} mean one step in the target language. Assume that if x_{i} and y_{j} are variables in a term then x ≠ y (α-convert as necessary). The definition of erasure is given in Figure 9. Notice that the definition depends on the implicit omniscient map Φ; we must know all type information to erase properly. If we erased to an untyped language, this would not be necessary.

Lemma 3.15 (Source and Target Evaluation Correspondence) If e_{i} ⟼^{i} e′_{i} then either \underline{e_{i}} = \underline{e′_{i}} or

\underline{e_{i}} ⟼^{−} \underline{e′_{i}}.

Proof: By induction on the source derivation. Proceeding by cases on the last rule of the derivation:

(1) Then \underline{e_{i}} = \underline{e_{i}^{0}} \underline{e_{i}^{2}} and e_{i}^{0} ⟼^{i} e_{i}^{1}. By induction, either \underline{e_{i}^{0}} = \underline{e_{i}^{1}} (in which case \underline{e′_{i}} = \underline{e_{i}^{1}} \underline{e_{i}^{2}} = \underline{e_{i}}) or

\underline{e_{i}^{0}} ⟼^{−} \underline{e_{i}^{1}} (in which case \underline{e_{i}} ⟼^{−} \underline{e_{i}^{1}} \underline{e_{i}^{2}} = \underline{e′_{i}}).

(2) Similar to argument for (1).

(3) Then e_{i} = ⌜⌞e_{j}⌝⌟_{ℓ_{j}}^{τ} and e_{j} ⟼^{j} e′_{j}. By induction, either \underline{e_{j}} = \underline{e′_{j}} (in which case \underline{e_{i}} = \underline{e_{j}} = \underline{e′_{j}} = \underline{⌜⌞e′_{j}⌝⌟_{ℓ_{j}}^{τ}} = \underline{e′_{i}})

or \underline{e_{j}} ⟼^{−} \underline{e′_{j}} (in which case \underline{e_{i}} = \underline{e_{j}} ⟼^{−} \underline{e′_{j}} = \underline{⌜⌞e′_{j}⌝⌟_{ℓ_{j}}^{τ}} = \underline{e′_{i}}).

(4) We use the following substitution lemma:

Lemma 3.16 Substitution commutes with erasure, i.e.\underline{\{v_{i}/x_{i}\}e_{i}} = \{\underline{v_{i}}/\underline{x_{i}}\}\underline{e_{i}}.

Proof: By structural induction on e_{i}:

x_{i} Immediately reduces to \underline{v_{i}} = \underline{v_{i}}.

y_{i} Immediately reduces to y = y.

e_{i}^{1} e_{i}^{2} Immediate from the inductive hypothesis since both substitution and erasure distribute across application.

⌜⌞e_{j}⌝⌟_{ℓ_{j}}^{τ} Immediate from the inductive hypothesis since both substitution and erasure cross agent boundaries.

λy_{i}:τ. e′_{i} If x_{i} = y_{i}, then substitution has no effect and the result is immediate. Else by the inductive hypothesis, \underline{\{v_{i}/x_{i}\}e′_{i}} = \{\underline{v_{i}}/\underline{x_{i}}\}\underline{e′_{i}}. So λy:\overline{Φ}(τ). \underline{\{v_{i}/x_{i}\}e′_{i}} = λy:\overline{Φ}(τ). \{\underline{v_{i}}/\underline{x_{i}}\}\underline{e′_{i}}. Finally, since

x_{i} ≠ y_{i}, this means \underline{\{v_{i}/x_{i}\}λy_{i}:τ. e′_{i}} = \{\underline{v_{i}}/\underline{x_{i}}\}\underline{λy_{i}:τ. e′_{i}}.

fix f_{i}(y_{i}:τ). e′_{i} Argument is completely analogous to previous case.

□

The result is immediate since \underline{e′_{i}} = \underline{\{v_{i}/x_{i}\}e′′_{i}} and \underline{e_{i}} ⟼^{−} \{\underline{v_{i}}/x\}\underline{e′′_{i}} where e′′_{i} is the body of the source function.

(5) Follows from the substitution lemma proved in the previous case.

(6),(7),(8) In all three cases, it is immediate from the definition of erasure that \underline{e_{i}} = \underline{e′_{i}}.

(9) Here e_{i} = ⌜⌞λx_{j}:τ^{0}. e_{j}⌝⌟_{ℓ_{j}}^{τ^{1}→τ^{2}} and e′_{i} = λx_{i}:τ^{1}. ⌜⌞\{⌜⌞x_{i}⌝⌟_{l′}^{τ^{0}}/x_{j}\}e_{j}⌝⌟_{ℓ_{j}}^{τ^{2}}. By the definition of erasure, \underline{e_{i}} =

λx:\overline{Φ}(τ^{0}). \underline{e_{j}} and \underline{e′_{i}} = λx′:\overline{Φ}(τ^{1}). \underline{⌜⌞\{⌜⌞x_{i}⌝⌟_{l′}^{τ^{0}}/x_{j}\}e_{j}⌝⌟_{ℓ_{j}}^{τ^{2}}}. By the substitution lemma proved in case (4),

and the definition of erasure, \underline{e′_{i}} = λx′:\overline{Φ}(τ^{1}). \{x′/x\}\underline{e_{j}}. That is, \underline{e_{i}} is α-equivalent to \underline{e′_{i}} so long as \overline{Φ}(τ^{0}) = \overline{Φ}(τ^{1}). We prove this type equivalence using the machinery of the previous section. Augment G({Δ}) with edges for Φ, an omniscient agent. By the definition of Φ, if (τ, τ′)_{i} is an edge, then there is now a (τ, τ′)_{Φ} edge. Since we assume e_{i} is well-formed, the static semantics guarantees τ^{0} ≲_{ℓ} τ^{1} for some ℓ (using the Type Relations Lemma to relate parts of related arrow types). So by Relations are Paths, there is some path from τ^{0} to τ^{1}. So there is a simple Φ path. So τ^{0} ≲_{Φ} τ^{1}. This can only be derived by (eq), the premise of which is the desired result: \overline{Φ}(τ^{0}) = \overline{Φ}(τ^{1}).

□

Lemma 3.17 (Type Refinement Terminates) If e_{i} = ⌜⌞e_{j}⌝⌟_{ℓ_{j}}^{τ} and evaluation of e_{j} terminates (there

exists v_{j} such that e_{j} ⟼^{j}^{∗} v_{j}), then evaluation of e_{i} terminates.

Proof: Consider the evaluation of e_{i}. By the dynamic semantics, rule (3) will first be applied until we have the term ⌜⌞v_{j}⌝⌟_{ℓ_{j}}^{τ}. At this point, by Progress, one of rules (6), (7), (8), or (9) must apply. For rules (6) or (9), we reach a value in one step. For rule (8), in one step one of rules (7), (8), or (9) will apply. For rule (7), in one step one of rules (8), or (9) will apply. Rule (7) applies at most once because Δ̄_{i}(τ) = Δ_{i}(Δ̄_{i}(τ)). Finally rule (8) cannot apply forever because it makes a smaller inside term. □

Lemma 3.18 (Correspondence of Divergence) If e_{i} diverges (has an infinite evaluation sequence), then \underline{e_{i}} diverges.

Proof: We prove the contrapositive: if evaluation of \underline{e_{i}} terminates, then evaluation of e_{i} terminates. By Lemma 3.15 and induction on the number of evaluation steps, if \underline{e_{i}} ⟼^{−}^{∗} v then e_{i} ⟼^{i}^{∗} e′_{i} such that \underline{e′_{i}} = v. Now by definition of erasure, e′_{i} must be a v_{j} enclosed in some finite number of embeddings. (This is because if e_{i} contains an application or fix expression, it cannot erase to a value.) Now by induction on the number of embeddings, using Lemma 3.17 at each step, we conclude that evaluation of e′_{i} terminates. Therefore, evaluation of e_{i} terminates. □

Theorem 3.19 If e_{i} ⟼^{i}^{∗} v_{i}, then \underline{e_{i}} ⟼^{−}^{∗} \underline{v_{i}}. If e_{i} diverges (has an infinite length evaluation sequence), then \underline{e_{i}} diverges.

Proof: The first part follows from Lemma 3.15 and induction on the number of source evaluation steps. The second part is Lemma 3.18. □

Corollary 3.20 If \{Δ\}; ∅ ⊢_{i} e_{i} : b and e_{i} ⟼^{i}^{∗} v_{i}, then \underline{e_{i}} ⟼^{−}^{∗} v_{i}.

Proof: By type soundness, canonical forms, the preceding theorem, and the definition of erasure. □

3.5 Safety Theorems

Definition 3.21 (Agents(e_{i})) Let Agents(e_{i}) be the agent names that appear anywhere in e_{i} (including i itself).

Definition 3.22 (j-free) A term e_{i} is said to be j-free if j ∉ Agents(e_{i}).

Definition 3.23 (Nearly j-free) A term e_{i} is said to be nearly j-free if the only subterms of e_{i} labeled with agent j are variables.

Note that if follows from the definition that if e_{i} is nearly j-free, and it does contain j-variables, then those variables are free. In particular, in order for e_{i} to typecheck, all j-variables occurring in e_{i} must be bound in the context.

Definition 3.24 (Oblivious to a Type) A set of agents A is \underline{oblivious} to t if ∀i ∈ A. Δ_{i}(t) = t and ∀i ∈ A. ∀s ≠ t. Δ_{i}(s) ≠ t.

Theorem 3.25 (Value Abstraction) Let j be any agent. For agent i ≠ j, let φ(e_{i}) mean:

1 {Δ}; [x_{j} : Δ̄_{j}(t)] ⊢_{i} e_{i} : τ for some τ

2 e_{i} is nearly j-free

3 Agents(e_{i}) \ {j} are oblivious to t

4 If ⌜⌞x_{j}⌝⌟_{ℓ_{j}}^{τ} is a subterm of e_{i} then τ = t.

Let i ≠ j be any agent. Let e_{i} be a term such that φ(e_{i}), and let v̂_{j} and v̂′_{j} be j-primvals such that

{Δ}; ∅ ⊢_{i} ⌜⌞v̂_{j}⌝⌟t_{j} : t and {Δ}; ∅ ⊢_{i} ⌜⌞v̂′_{j}⌝⌟t_{j} : t. Then

{v̂_{j}/x_{j}}e_{i} ⟼^{i} e_{i}^{1} = {v̂_{j}/x_{j}}e′_{i}

iff

{v̂′_{j}/x_{j}}e_{i} ⟼^{i} e_{i}^{2} = {v̂′_{j}/x_{j}}e′_{i}

Furthermore, φ(e′_{i}).

Proof: First note that by the static semantics and the concreteness of types lemma, it must be the case that {Δ}; ∅ ⊢_{j} v̂_{j} : Δ̄_{j}(t) and {Δ}; ∅ ⊢_{j} v̂′_{j} : Δ̄_{j}(t).

Suppose {v̂_{j}/x_{j}}e_{i} ⟼^{i} e_{i}^{1} = {v̂_{j}/x_{j}}e′_{i}. By the soundness of the operational semantics, and the observation above, it follows that part 1 of property φ holds for e′_{i}.

Let σ be the substitution {v̂_{j}/x_{j}} and σ′ be the substitution {v̂′_{j}/x_{j}}. Note that since e_{i} is nearly j-free, every subterm of e_{i} is also nearly j-free. Similarly, since Agents(e_{i}) \ {j} is oblivious to t, for any subterm e′′_{i} of e_{i} Agents(e′′_{i}) \ {j} is also oblivious to t. Similarly, property 4 holds for all subterms of e_{i}. We use these facts in the inductive cases below.

We now show by induction on the structure of e_{i} that σ′e_{i} ⟼^{i} e_{i}^{2} = σ′e′_{i} and φ(e_{i}). (The other direction of the implication is exactly symmetric.)

e_{i} = c This case is impossible, since there is no transition step.

e_{i} = λy_{i}:τ′. e′′_{i} This case is also impossible.

e_{i} = fix f_{i}(y_{i}:τ′). e′′_{i} Since e_{i} is nearly j-free, i ≠ j and it follows that x_{j} ≠ f_{i} and x_{j} ≠ y_{i}, so the definition of substitution yields σe_{i} = σ(fix f_{i}(y_{i}:τ′). e′′_{i}) = fix f_{i}(y_{i}:τ′). σe′′_{i}. The only transition rule applicable is rule (5), which yields fix f_{i}(y_{i}:τ′). σe′′_{i} ⟼^{i} λy_{i}:τ′. {fix f_{i}(y_{i}:τ′). σe′′_{i}/f_{i}}σe′′_{i}. We can pull the substitution out front (again since the variables aren’t equal) to obtain σ(λy_{i}:τ′. {fix f_{i}(y_{i}:τ′). e′′_{i}/f_{i}}e′′_{i}). So taking e′_{i} = λy_{i}:τ′. {fix f_{i}(y_{i}:τ′). e′′i/f_{i}}e′′_{i}, we obtain σe_{i} ⟼^{i} σe′_{i}. A similar derivation using σ′ in place of σ above also yields σ′e_{i} ⟼^{i} σ′e′_{i}.

Notice that Agents(e′_{i}) = Agents(e_{i}), so the oblivious condition still holds. Similarly, since e′′_{i} is nearly j-free, so is e′_{i}. Since the subterms of e′′_{i} satisfy item 4 of φ, so must e′_{i}.

e_{i} = e_{i}^{a} e_{i}^{b} There are three possible transitions steps taken by terms of this form, corresponding to rules (1), (2), and (4). Note that it follows immediately from (app) that {Δ}; [x_{j} : Δ̄_{j}(t)] ⊢_{i} e_{i}^{a} : τ′′ → τ and {Δ}; [x_{j} : Δ̄(t)] ⊢_{i} e_{i}^{b} : τ′′ for some τ′′. We consider each case separately.

(1) σe_{i} = σ(e_{i}^{a} e_{i}^{b}) = σe_{i}^{a} σe_{i}^{b}. Similarly, σ′e_{i} = σ′(e_{i}^{a} e_{i}^{b}) = σ′e_{i}^{a} σ′e_{i}^{b}. Since (1) was used, we have σe_{i}^{a} ⟼^{i} e_{i}^{a′}. The inductive hypothesis applies, so e_{i}^{a′} = σe_{i}^{A} and σ′e_{i}^{a} ⟼^{i} σ′e_{i}^{A}. Using rule (1) again, we have σe_{i} ⟼^{i} σe_{i}^{A} σe_{i}^{b},but σe_{i}^{A} σe_{i}^{b} = σ(e_{i}^{A} e_{i}^{b}) by the definition of substitution. Similarly, σ′e_{i} ⟼^{i} σ′(e_{i}^{A} e_{i}^{b}), so the first result holds. Furthermore, by induction, we have φ(e_{i}^{A}), it was already observed that φ(e_{i}^{b}), so we conclude φ(e′_{i}) also holds. Likewise, Agents(e′_{i}) \ {j} are oblivious to t.

(2) This follows analogously to the previous subcase.

(4) Then e_{i} = λy_{i}:τ′. e′′_{i} v_{i} and, as before, i ≠ j so we have y_{i} ≠ x_{j}. Calculating, we have σe_{i} = σ(λy_{i}:τ′. e′′_{i} v_{i}) = λy_{i}:τ′. σe′′_{i} (σv_{i}) = λy_{i}:τ′. (σe′′_{i}) v_{i} which transitions via rule (4) to

{v_{i}/y_{i}}(σe′′_{i}) = σ({v_{i}/y_{i}}e′′_{i}). Thus we have σe_{i} ⟼^{i} σ({v_{i}/y_{i}}e′′_{i}). A similar calculation using σ′

in place of σ shows that σ′e_{i} ⟼^{i} σ′({v_{i}/y_{i}}e′′_{i}), which is the desired result. Taking e′_{i} = {v_{i}/y_{i}}e′′_{i}, conditions 2 through 4 hold since v_{i} and e′′_{i} are subterms of e_{i}.

e_{i} = ⌜⌞e_{k}⌝⌟_{ℓ_{k}}^{τ′} In this case, the transition rule applied must be one of (3), (6) through (9). In case (6) the expression is closed, so substitution has no effect and the result holds trivially. We consider each of the remaining cases separately.

(3) In this case, k ≠ j since the only occurrences of j subterms in e_{i} must be the variable x_{j}, which has been replaced by a value. From the definition of substitution, σe_{i} = σ⌜⌞e_{k}⌝⌟_{ℓ_{k}}^{τ′} = ⌜⌞σe_{k}⌝⌟_{ℓ_{k}}^{τ′}. Since σe_{k} takes a step to e_{k}^{1} = σe′_{k}, the inductive hypothesis applies and we conclude that σ′e_{k} ⟼^{k} σ′e′_{k}.

Applying rule (3), we obtain σ′⌜⌞e_{k}⌝⌟_{ℓ_{k}}^{τ′} = ⌜⌞σ′e_{k}⌝⌟_{ℓ_{k}}^{τ′} ⟼^{i} ⌜⌞σ′e′_{k}⌝⌟_{ℓ_{k}}^{τ′} = σ′⌜⌞e′_{k}⌝⌟_{ℓ_{k}}^{τ′}. By induction, φ(e′_{k})

holds, so it follows immediately that φ(e′_{i}) = φ(⌜⌞e′_{k}⌝⌟_{ℓ_{k}}^{τ′}) holds too.

(7) Calculating, we have: σ⌜⌞e_{k}⌝⌟_{ℓ_{k}}^{τ′} = ⌜⌞σe_{k}⌝⌟_{ℓ_{k}}^{τ′} = ⌜⌞v̂_{k}⌝⌟_{ℓ_{k}}^{τ′} which steps via rule (7) to ⌜⌞v̂_{k}⌝⌟_{ℓ_{k}}^{Δ̄_{i}(τ′)} =

⌜⌞σe_{k}⌝⌟_{ℓ_{k}}^{Δ̄_{i}(τ′)} = σ⌜⌞e_{k}⌝⌟_{ℓ_{k}}^{Δ̄_{i}(τ′)}. Thus τ′ ≠ Δ̄_{i}(τ′), and hence τ′ ≠ t. By assumption, this implies that k ≠ j, so property 4 is preserved. Note that since σe_{k} is a value, so is σ′e_{k}. This allows us to calculate similarly that σ′⌜⌞e_{k}⌝⌟_{ℓ_{k}}^{τ′} ⟼^{i} σ′⌜⌞e_{k}⌝⌟_{ℓ_{k}}^{Δ̄_{i}(τ′)}. Since near j-freeness and oblivious to t don’t depend on the typing annotation we’re done.

(8) Since v̂_{j} is a j-primval, e_{i} must be of the form ⌜⌞⌜⌞e_{h}⌝⌟u_{ℓ_{h}}⌝⌟_{ℓ_{k}}^{τ} such that σe_{h} is a h-primval. It follows that σ′e_{h} is also a h-primval. We use the fact that substitutions commute with embeddings to cal-

culate: σ⌜⌞⌜⌞e_{h}⌝⌟u_{ℓ_{h}}⌝⌟_{ℓ_{k}}^{τ} = ⌜⌞σ⌜⌞e_{h}⌝⌟u_{ℓ_{h}}⌝⌟_{ℓ_{k}}^{τ} = ⌜⌞⌜⌞σe_{h}⌝⌟u_{ℓ_{h}}⌝⌟_{ℓ_{k}}^{τ} which transitions to ⌜⌞σe_{h}⌝⌟_{ℓ_{h}:ℓ_{k}}^{τ} = σ⌜⌞e_{h}⌝⌟_{ℓ_{h}:ℓ_{k}}^{τ}.

Under the assumption that u ∉ Dom(Δ_{k}). We can then do the similar calculation for σ′ to obtain σ′⌜⌞⌜⌞e_{h}⌝⌟u_{ℓ_{h}}⌝⌟_{ℓ_{k}}^{τ} ⟼^{i} σ′⌜⌞e_{h}⌝⌟_{ℓ_{h}:ℓ_{k}}^{τ}. As above, since near j-freeness and oblivious to t don’t depend on the typing annotation on embeddings, conditions 2 and 3 hold. To show condition 4, note that k can’t equal j, and so it remains to check two cases: h = j and h ≠ j. In the first case, by assumption, u = t and since k ≠ j it follows that τ = t, so property 4 is preserved across the step. In the second case, h ≠ j and the fact that e_{h} is a primval, imply that e_{i} contains no embeddings labeled by ℓ_{j} and neither does e′_{i}. Property 4 holds vacuously.

(9) In this case, τ′ = τ^{1} → τ^{2} and e_{k} = λx_{k}:τ^{0}. e′_{k}. Since τ^{1} → τ^{2} ≠ t it must be the case that j ≠ k and hence x_{j} ≠ x_{k}. We calculate: σ⌜⌞λx_{k}:τ^{0}. e′_{k}⌝⌟_{ℓ_{k}}^{τ^{1}→τ^{2}} = ⌜⌞σ(λx_{k}:τ^{0}. e′_{k})⌝⌟_{ℓ_{k}}^{τ^{1}→τ^{2}} = ⌜⌞λx_{k}:τ^{0}. σe′_{k}⌝⌟_{ℓ_{k}}^{τ^{1}→τ^{2}} which steps via (9) to

λx_{i}:τ^{1}. ⌜⌞{⌜⌞x_{i}⌝⌟_{ℓ′}^{τ^{0}}/x_{k}}σe′_{k}⌝⌟_{ℓ_{k}}^{τ^{2}} = λx_{i}:τ^{1}. σ⌜⌞{⌜⌞x_{i}⌝⌟_{ℓ′}^{τ^{0}}/x_{k}}e′_{k}⌝⌟_{ℓ_{k}}^{τ^{2}} = σ(λx_{i}:τ^{1}. ⌜⌞{⌜⌞x_{i}⌝⌟_{ℓ′}^{τ^{0}}/x_{k}}e′_{k}⌝⌟_{ℓ_{k}}^{τ^{2}})

A similar calculation shows that σ′⌜⌞λx_{k}:τ^{0}. e′_{k}⌝⌟_{ℓ_{k}}^{τ^{1}→τ^{2}} ⟼^{i} σ′(λx_{i}:τ^{1}. ⌜⌞{⌜⌞x_{i}⌝⌟_{ℓ′}^{τ^{0}}/x_{k}}e′_{k}⌝⌟_{ℓ_{k}}^{τ^{2}}). Since

i ≠ j, near j-freeness is preserved. The agents of e′_{i} = λx_{i}:τ^{1}. ⌜⌞{⌜⌞x_{i}⌝⌟_{ℓ′}^{τ^{0}}/x_{k}}e′_{k}⌝⌟_{ℓ_{k}}^{τ^{2}} are the same as for e_{i}, so they are oblivious as well. The embedding subterms of e′_{i} are either subterms of e_{i}, in which case they obey property 4, or labeled by either k or i, neither of which equal j, thus property 4 of φ holds for e′_{i}, and we’re done.

□

Corollary 3.26 (Independence of Evaluation) If

1 {Δ}; ∅ ⊢_{i} λx_{i}:t. e_{i} : t → b
2 {Δ}; ∅ ⊢_{i} ⌜⌞v̂_{j}⌝⌟t_{j} : t
3 {Δ}; ∅ ⊢_{i} ⌜⌞v̂′_{j}⌝⌟t_{j} : t

and e_{i} is j-free and Agents(e_{i}) are oblivious to t then: (λx_{i}:t. e_{i}) ⌜⌞v̂_{j}⌝⌟t_{j} ⟼^{∗} c iff (λx_{i}:t. e_{i}) ⌜⌞v̂′_{j}⌝⌟t_{j} ⟼^{∗} c

Proof (sketch): By induction on the length of the evaluation sequence using the Value Abstraction theorem. □

Definition 3.27 (h-terms) • Let e_{j} be an \underline{h-term} if j = h or e_{j} = ⌜⌞e_{k}⌝⌟_{ℓ_{k}}^{τ} and h ∈ ℓ_{k}.

• Let e_{j} be a \underline{non-h-term} if j ≠ h or e_{j} = ⌜⌞e_{k}⌝⌟_{ℓ_{k}}^{τ} and ∃i. i ∈ ℓ_{k} and i ≠ h.

• Let e_{j} be a \underline{both-term} if it is an h-term and a non-h-term.

• Let e_{j} be an \underline{h-embedding} if it is an h-term embedded in a non-h-term.

• Let e_{j} be a \underline{non-h-embedding} if it is a non-h-term embedded in an h-term.

• For ⌜⌞e_{k}⌝⌟_{ℓ_{k}}^{τ} let τ be the \underline{outside type} and let the type of e_{k} in some static derivation be the \underline{inside type}.

Theorem 3.28 (Host Provided Values) Let h be a distinguished agent, the host, and let i ≠ h be any other agent. Let e_{i}^{0} be an i-term. Let τ_{i} be any base type (the input type, provided by agent i) and let τ_{h} be any other type (the implementation type, known only to the host). Assume the following:

• Δ_{h}(t) = τ_{h} = Δ_{h}(τ_{h}).

• Agents(e_{i}^{0}) \ {h} are oblivious to t and for all s ≠ t, Δ_{h}(s) ≠ t.

• {Δ}; ∅ ⊢_{i} λp_{i}:τ_{i} → t. e_{i}^{0} : τ

• For all subterms e′ of e_{i}^{0}, if e′ is an h-embedding or a both-term, then t does not occur positively in its outside type; if e′ is a non-h-embedding or a both-term, then t does not occur negatively in its inside type.

• f_{h} = λx_{h}:τ_{i}. e_{h} be a pure h term such that {Δ}; ∅ ⊢_{h} f_{h} : τ_{i} → τ_{h}. It is the h-value implementing the function p_{i} provided to i. Note that {Δ}; ∅ ⊢_{i} ⌜⌞f_{h}⌝⌟_{h}^{τ_{i}→t} : τ_{i} → t. It follows by rule

(9) that ⌜⌞f_{h}⌝⌟_{h}^{τ_{i}→t} ⟼^{i} λx_{i}:τ_{i}. ⌜⌞{⌜⌞x_{i}⌝⌟_{i}^{τ_{i}}/x_{h}}e_{h}⌝⌟t_{h}. Let f_{i} = λx_{i}:τ_{i}. ⌜⌞{⌜⌞x_{i}⌝⌟_{i}^{τ_{i}}/x_{h}}e_{h}⌝⌟t_{h} and let e′_{h} =

{⌜⌞x_{i}⌝⌟_{i}^{τ_{i}}/x_{h}}e_{h}.

• {f_{i}/p_{i}}e_{i}^{0} = e^{i} ⟼^{i}^{∗} e′_{i}

Then if v is a value of type t which is a subterm of e′_{i}, v is of the form ⌜⌞v̂_{h}⌝⌟t_{ℓ} for a value v̂_{h} obtained by applying f_{h} to a suitable argument.

The next two lemmas provide what we need to prove the theorem. Lemma 3.29 (Preservation of Host Provided Terms) Let φ(e) mean that for all subterms e′ of e:

1 If e′ is an h-embedding or a both-term, then one of the following is true:

(a) t does not occur positively in the outside type of e′.

(b) The embedding is ⌜⌞e′_{h}⌝⌟t_{h}.

(c) e′ = ⌜⌞e′′_{h}⌝⌟t_{ℓ_{h}} and ∃v_{i} : τ_{i}. f_{i} v_{i} ⟼^{i}^{∗} ⌜⌞e′′_{h}⌝⌟t_{ℓ′}.

2 If e′ is a non-h-embedding or a both-term, then the typing derivation of e assigns an inside type to e′

in which t does not occur negatively. Assume the same system that is assumed for the theorem. For all i, if φ(e_{i}) and e_{i} ⟼^{i} e′_{i}, then φ(e′_{i}).

Proof: By induction on the dynamic derivation. Last rule is:

(1) By induction.

(2) By induction.

(3) Let e_{i} = ⌜⌞e_{k}⌝⌟_{ℓ_{k}}^{τ} ⟼^{i} ⌜⌞e′_{k}⌝⌟_{ℓ_{k}}^{τ}. By induction, φ(e′_{k}). It remains to verify the term ⌜⌞e′_{k}⌝⌟_{ℓ_{k}}^{τ} itself. Since the inside type and outside type do not change, every case is immediate except the possibility that e_{i} is an h-embedding or both-term and t appears positively in τ. Since e_{k} is closed, ∃v_{i} : τ_{i} such that

f_{i} v_{i} ⟼^{i}^{∗} ⌜⌞e_{k}⌝⌟_{h}^{t}. (So k = h.) Since e_{k} ⟼^{k} e′_{k}, we conclude via rule (3) that f_{i} v_{i} ⟼^{i}^{∗} ⌜⌞e′_{k}⌝⌟_{h}^{t}.

(4) Follows from the following substitution lemma: If φ(e_{i}) and φ(v_{i}) for some value v_{i}, then φ({v_{i}/y_{i}}e_{i}). Let σ = {v_{i}/y_{i}} be the substitution. Proof by structural induction on e_{i}: e_{i} = c Substitution has no effect, so the result is immediate. e_{i} = y_{i} Then σ(e_{i}) = v_{i}, and the result holds by assumption. e_{i} = y′_{i} ≠ y_{i} Then Substitution has no effect, trivial. e_{i} = λy′_{i}:τ. e′_{i} By BVC, y_{i} ≠ y′_{i}, so σ(e_{i}) = σ(λy′_{i}:τ. e′_{i}) = λy′_{i}:τ. σ(e′_{i}) Since φ(e_{i}) implies φ(e′_{i}), we

conclude by induction that φ(σ(e′_{i})). The outermost term satisfies φ vacuously, since it’s not an embedding, therefore we conclude φ(λy′_{i}:τ. σ(e′_{i})).

e_{i} = fix f_{i}(y′_{i}:τ). e′_{i} This follows analogously to the previous case. e_{i} = e_{i}^{0} e_{i}^{1} This follows immediately from two applications of the inductive hypothesis and the fact

that the outermost term of the resulting substitution is not an embedding.

e_{i} = ⌜⌞e_{k}⌝⌟_{ℓ_{k}}^{τ} Then σ(e_{i}) = σ(⌜⌞e_{k}⌝⌟_{ℓ_{k}}^{τ}) = ⌜⌞σ(e_{k})⌝⌟_{ℓ_{k}}^{τ}. Since φ(e_{i}) implies φ(e_{k}), it follows by induction that φ(σ(e_{k})). Thus the only subterm that needs to be checked is ⌜⌞σ(e_{k})⌝⌟_{ℓ_{k}}^{τ} itself. Since substitution doesn’t change types, conditions 1(a) and 2 follow immediately. The remaining case occurs when t occurs positively in τ. Since φ(e_{i}), we have τ = t. In the case that e_{k} = e′_{h}, its only free variable is x_{i}. If y_{i} = x_{i}, then σ(e_{k}) = σ(e′_{h}) = σ({⌜⌞x_{i}⌝⌟_{i}^{τ_{i}}/x_{h}}e_{h}) = {⌜⌞v_{i}⌝⌟_{i}^{τ_{i}}/x_{h}}e_{h}. Notice that f_{i} v_{i} transitions in one step by (4) to {⌜⌞v_{i}⌝⌟_{i}^{τ_{i}}/x_{h}}e_{h}, so 1(c) is satisfied. If y_{i} ≠ x_{i} then the substitution has no effect and 1(b) is still satisfied. The only other possibility is that e_{i} satisfied 1(c), in which case e_{k} is closed and hence substitution has no effect. Thus in all cases, we conclude φ(σ(e_{i})).

(5) All of the subterms of e′_{i} are subterms of e_{i} with the exception of e_{i} itself. Since e′_{i} is not an embedding, the conditions hold trivially for it and we’re done.

(6) Let e_{i} = ⌜⌞⌜⌞v̂_{h}⌝⌟u_{ℓ_{h}}⌝⌟_{ℓ_{k}}^{τ} ⟼^{i} ⌜⌞v̂_{h}⌝⌟_{ℓ_{h}:ℓ_{k}}^{τ} By the constraints on the system, if τ contains t, then u = τ = t. (Otherwise some Δ(u) contains t.) The result is immediate if τ does not contain t, so assume it does. By the system, static semantics, and canonical forms, v̂_{h} must be of type τ_{i}, which is devoid of t’s. So the inside type cannot have a negative occurrence of t. If h ∉ ℓ_{k}, then we’re done because appending non-h agents cannot violate φ(e′_{i}) since the inside type has no negative occurrence of t. To see that h cannot occur in ℓ_{k}, note that e_{k} ≠ e′_{h}. Furthermore, since f_{h} accepts only base values, any term stepped to by f_{h} v must be a pure h term. This rules out the possibility that e_{i} satisfies 1(c), and so the only possibility is that h does not occur in ℓ_{k}.

(7) Immediate because for all s and k, Δ_{k}(s) ≠ t.

(8) Immediate.

(9) Let e_{i} = ⌜⌞λx_{j}:τ^{0}. e_{j}⌝⌟_{ℓ_{j}}^{τ^{1}→τ^{2}} ⟼^{i} λx_{i}:τ^{1}. ⌜⌞{⌜⌞x_{i}⌝⌟_{i:rev(tl(ℓ_{j}))}^{τ^{0}}/x_{j}}e_{j}⌝⌟_{ℓ_{j}}^{τ^{2}} = e′_{i}

If e_{i} is a both term, then t does not occur positively in τ^{1} → τ^{2} and t does not occur positively in τ^{0} (since the inside type must be τ^{0} → τ^{3} for some τ^{3}). The t doesn’t occur positively in τ^{2} or negatively in τ^{1}. This immediately verifies e′_{i} and the body of the function, so long as the embedded term is verified. We know φ(e_{j}). We need a substitution lemma analogous to the one above but tailored to substitutions of the form ⌜⌞x_{i}⌝⌟_{ℓ_{i}}^{τ^{0}}. The key observation is that the types prohibit {⌜⌞x_{i}⌝⌟_{i:rev(tl(ℓ_{j}))}^{τ^{0}}/x_{j}}e_{j}

from being e′_{h}, or the result of f_{i} v_{i} for any v_{i}. Thus it is sufficient to show φ(⌜⌞x_{i}⌝⌟_{i:rev(tl(ℓ_{k}))}^{τ^{0}}). Since t does not occur positively in τ^{0}, it suffices to show that t does not occur negatively in the type of x_{i}. That type is τ^{1}, so we are done.

If e_{i} is an h-embedding and not a both-term, then t does not occur positively in τ^{1} → τ^{2} (see that the other cases are not possible) and τ^{0} does not contain t at all (since k = h). This is stronger than what we assumed in the previous case, so apply that argument.

If e_{i} is a non-h-embedding and not a both-term, then t does not occur at all in τ^{1} → τ^{2} (by the side-condition for rule 5 which gives rule 7 precedence) and does not occur positively in τ^{0}. Again, this is stronger than what we assumed in the both-term case.

□

Lemma 3.30 (t values are h-embeddings) Assume the system of the theorem. If v is a value of type t and a subterm of e_{i}, then v is h-term embedded in a non-h-term with a τ_{i} for the embedded term.

Proof: Follows directly from the system and the static semantics. □

The theorem follows from the lemmas and claiming that if a value is produced by check, then it is permissible (applying f to it produces true).

4 Future Work

4.1 Polymorphism

Type abstraction and polymorphism are closely related. Indeed, the example encoding of an agent in the introduction used polymorphism to achieve type abstraction. However, the two are different. The key distinction seems to be one of scope. Our type abstractions are globally scoped and statically known. Polymorphism allows locally scoped type abstractions which can be instantiated many times at run-time.

There are several approaches to adding polymorphism to the multiagent calculus, none of which we have fully explored. One is to simply add polymorphism, keeping the type variables for polymorphism and agents disjoint. The necessary additions seem to be straightforward.

A different avenue is to encode polymorphism using the embeddings of the multiagent calculus. The idea is to represent the body of a polymorphic function, Λα. e_{i} as an agent with no information about the type variable α. When such a function is applied to a type τ, a new agent, j, that knows α = τ is “spawned” with the body e_{i} embedded inside it. The type system prevents the body of the function from breaking the type abstraction, while the “wrapper” agent, j, provides a way to recover the type information when the function returns.

4.2 Beyond Type Abstraction

Type abstraction is one application of formalizing the notion of principal. The difference between agents in this calculus is what type-information is available to them. There are many other dimensions along which this idea can be extended. We can use essentially the same mechanism to formalize foreign function calls, where each agent uses a different set of operational rules. For example, we could give some agents a call-by-name semantics, allowing a mixture of eager and lazy evaluation. For less similar languages, the embeddings express exactly where foreign data conversions and calling conventions need to occur.

The Δ_{i}’s capture an agent’s view of its environment. In this paper we restricted our attention to type information, but this too can potentially be extended. The Δ_{i}’s could represent arbitrary capabilities, controlling access to resources in the environment. Suitable rules in the operational semantics would propagate which capabilities are available. The ability to update the Δ_{i}’s could be reflected into the language itself, yielding a dynamic system in which a principal could grant or revoke capabilities to other agents at run-time.

5 Related Work

Perhaps the closest work to ours is Leroy and Rouaix’s investigation into the safety properties of typed applets [9]. They use a λ-calculus augmented with state in order to prove theorems similar to Theorem 2.16. They too distinguish between the execution environment code and applet code, similar to our use of principals, but they consider only the two-agent case and take a less syntactic approach.

There has been much work on representation independence and parametric polymorphism, as pioneered by Strachey [18] and Reynolds [17]. Such notions have been incorporated into programming languages such as SML and Haskell [10, 14] and studied extensively in Girard’s system F [5].

Abadi, Cardelli, and Curien have taken a syntactic approach to parametricity by formalizing the logical relations arguments used in such proofs [1]. More recently, Crary has proposed the use of singleton types as a means of proving parametricity results without resorting to the construction of models [4]. Pierce and Sangiorgi [15] have studied parametricity in a polymorphic variant of the π-calculus; they too are concerned with multiple views of the same value and point out some interesting interactions between abstraction and aliasing.

None of the above work (except Leroy and Rouaix’s) explicitly involves the notion of principal. Our syntactic separation of agents is similar to Nielson and Nielson’s Two-Level λ-calculus [13]. There they are concerned with binding time analysis, so the two principals’ code is inherently not mixed during evaluation. A notion of principal also arises in the study of language based security, where privileged agents may not leak information to unprivileged ones. See, for example, Heinze and Reicke’s work on the SLam calculus [8], Volpano and Smith’s work on type-based security [19], or Myers’ JFlow system [12].

6 Conclusion

We have created a multiagent calculus in which the notion of principal is made explicit in the language. This syntactic distinction allows us to track agent code during evaluation, giving syntactic proofs of interesting type abstraction properties. Our hope is that these techniques will scale to realistic, hard to model languages.

References

[1] Martín Abadi, Luca Cardelli, and Pierre-Louis Curien. Formal parametric polymorphism. In Principles of Programming Languages, volume 20, pages 157–167, January 1993.

[2] Godmar Back, Patrick Tullmann, Leigh Stoller, Wilson C. Hseih, and Jay Lepreau. Java operating systems: Design and implementation. Technical Report UUCS-98-015, University of Utah, August 1998.

[3] Brian N. Bershad, Stefan Savage, Przemyslaw Pardyak, Emin Gün Sirer, Marc Fiuczynski, David Becker, Susan Eggers, and Craig Chambers. Extensibility, safety and performance in the SPIN operating system. In Proceedings of the Fifteenth ACM Symposium on Operating Systems Principles, Copper Mountain, CO, December 1995.

[4] Karl Crary. A simple proof technique for certain parametricity results. Technical Report CMU-CS-98-185, Carnegie Mellon University, December 1998.

[5] Jean-Yves Girard, Y. Lafont, and P. Taylor. Proofs and Types. Cambridge University Press, 1989.

[6] Michael Godfrey, Tobias Mayr, Praveen Seshadri, and Thorsten von Eicken. Secure and portable database extensibility. In Proceedings of the 1997 ACM-SIGMOD Conference on the Management of Data, pages 390– 401, Seattle, WA, June 1998.

[7] Chris Hawblitzel, Chi-Chao Chang, Grzegorz Czajkowski, Deyu Hu, and Thorston von Eiken. Implementing multiple protection domains in Java. In 1998 USENIX Annual Technical Conference, New Orleans, LA, June 1998.

[8] Nevin Heintze and Jon G. Riecke. The SLam calculus: programming with secrecy and integrity. In Conference Record of the Twenty-Fifth Annual ACM Symposium on Principles of Programming Languages, pages 365–377. ACM Press, 1998.

[9] Xavier Leroy and François Rouaix. Security properties of typed applets. In Principles of Programming Languages, January 1998.

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

[11] J.C. Mitchell. On the equivalence of data representations. In V. Lifschitz, editor, Artificial Intelligence and Mathematical Theory of Computation: Papers in Honor of John McCarthy, pages 305–330. Academic Press, 1991.

[12] Andrew C. Myers. JFlow: Practical mostly-static information flow control. In Proceedings of the 26th ACM Symposium on Principles of Programming Languages, pages 228–241, San Antonio, TX, January 1999.

[13] Flemming Nielson and Hanne Riis Nielson. Two-Level Functional Languages. Number 34 in Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1992.

[14] John Peterson, Kevin Hammond, Lennart Augustsson, Brian Boutel, Warren Burton, Joseph Fasel, Andrew D. Gordon, John Hughes, Paul Hudak, Thomas Johnsson, Mark Jones, Erik Meijer, Simon Peyton Jones, Alastair Reid, and Philip Wadler. Report on the programming language Haskell, version 1.4. http://www.haskell.org/report.

[15] Benjamin C. Pierce and Davide Sangiorgi. Behavioral equivalence in the polymorphic pi-calculus. Technical Report MS-CIS-99-10, University of Pennsylvania, April 1999. (Summary in POPL ’97).

[16] John C. Reynolds. Towards a theory of type structure. In Programming Symposium, volume 19 of Lecture Notes in Computer Science, pages 408–425. Springer-Verlag, Paris, France, April 1974.

[17] John C. Reynolds. Types, abstraction, and parametric polymorphism. In R.E.A Mason, editor, Information Processing, pages 513–523. Elsevier Science Publishers B.V., 1983.

[18] C. Strachey. Fundamental concepts in programming languages. Unpublished Lecture Notes, Summer School in Computer Programming, August 1967.

[19] Dennis Volpano and Geoffrey Smith. A type-based approach to program security. In Proceedings of TAPSOFT ’97, Colloquium on Formal Approaches to Software Engineering, Lille, France, April 1997.

[20] Steve Zdancewic, Dan Grossman, and Greg Morrisett. Principals in programming languages: A syntactic proof technique. In Proceedings of the 4th ACM SIGPLAN International Conference on Functional Programming, Paris, France, September 1999.