Syntactic Type Abstraction

DAN GROSSMAN, GREG MORRISETT, and STEVE ZDANCEWIC Cornell University

Software developers often structure programs in such a way that different pieces of code constitute distinct principals. Types help define the protocol by which these principals interact. In particular, abstract types allow a principal to make strong assumptions about how well-typed clients use the facilities that it provides. We show how the notions of principals and type abstraction can be formalized within a language. Different principals can know the implementation of different abstract types. We use additional syntax to track the flow of values with abstract types during the evaluation of a program and demonstrate how this framework supports syntactic proofs (in the style of subject reduction) for type-abstraction properties. Such properties have traditionally required semantic arguments; using syntax avoids the need to build a model for the language. We present various typed lambda calculi with principals, including versions that have mutable state and recursive types.

Categories and Subject Descriptors: D.2.11 [Software Engineering]: Software Architectures— Information Hiding; Languages; D.3.1 [Programming Languages]: Formal Definitions and Theory—Syntax; Semantics; D.3.3 [Programming Languages]: Language Constructs and Features—Abstract data types; F.3.2 [Logics and Meanings of Programs]: Semantics of Programming Languages—Operational Semantics; F.3.3 [Logics and Meanings of Programs]: Studies of Program Constructs—Type Structure

General Terms: Languages, Security, Theory, Verification Additional Key Words and Phrases: Operational semantics, parametricity, proof techniques, syntactic proofs, type abstraction

1. INTRODUCTION

Programmers often use a notion of principal when designing the structure of a program. Examples of principals include modules of a large system, a host and its clients, and separate functions. Dividing code into such agents is useful for composing programs. Moreover, with the increasing use of extensible systems, such as Web browsers, databases, and operating systems, this notion of principal becomes critical for reasoning about untrusted clients that interact with host-provided code.

In this paper, we incorporate the idea of principal into various typed lambda calculi. Doing so allows us to formulate security policies and check that the type system enforces them. An example of a useful policy is, “clients can gain access to

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. Authors’ address: Department of Computer Science, 4130 Upson Hall, Cornell University, Ithaca, NY, 14853; email: {danieljg, jgm, zdance}@cs.cornell.edu. Permission to make digital/hard copy of all or part of this material without fee for personal or classroom use provided that the copies are not made or distributed for profit or commercial advantage, the ACM copyright/server notice, the title of the publication, and its date appear, and notice is given that copying is by permission of the ACM, Inc. To copy otherwise, to republish, to post on servers, or to redistribute to lists requires prior specific permission and/or a fee.

ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year, Pages 1–44.

2 · Dan Grossman et al.

                         (* File handle implemented as int *)
                         abstype fh

open : string → fh read : fh → char

Fig. 1. Abstract interface for file handles.

a file handle only through the open procedure.”

Consider a host-provided interface for an abstract type of file handles, fh, that includes operations to create and use them (Figure 1). 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, whereas clients do not.

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

How do we prove such properties? One way of phrasing the result is to say that the client 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 [Girard et al. 1989], the polymorphic lambda calculus [Reynolds 1974]. The type fh is held abstract by encoding the client as a polymorphic function:

Λfh.λhost : {open : string → fh, read : fh → char}.client code

We can then appeal to Reynolds’ parametricity results [Reynolds 1983] to conclude that the client respects the host’s interface.

Unfortunately, these representation-independence results are proven using semantic arguments based on a model of the language (see the work of Mitchell [1991], 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 agents with different type information. By “coloring” host code and client code differently, we can track 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 the client code when linked against a host implementation. Figure 2 shows the standard encoding of linking as application. In one step of the standard operational semantics, the host type is substituted throughout the client 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 client code, and all distinctions between principals are lost.

ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

Syntactic Type Abstraction · 3

τ = {open : string → fh, read : fh → char}
(Λfh.λhost : τ.client code) int host code
⟼ (λhost : {int/fh}τ.{int/fh}client code) host code
⟼ {host code/host}{int/fh}client code

Fig. 2. Standard encoding for “linking” client and host code.

In the next section, we describe a two-agent setting sufficient for proving interesting properties about the file-handle example. It introduces the general approach of distinguishing principals^{1} during evaluation. Section 3 introduces a multiagent calculus that provides for multiple agents, multiple abstract types, and an arbitrary assignment of what types are known to what agents. We prove several safety and abstraction theorems for this calculus; the safety properties for the two-agent calculus follow as corollaries. The next two sections sketch extensions to our system that we believe are more difficult in a less syntactic framework. Section 4 adds references and state; the presentation emphasizes the subtle ways that naive treatments of state can break type abstraction. Section 5 adds recursive types and polymorphism; here we emphasize that these features can be treated as orthogonal to principals or that these features can be encoded using principals. Section 6 surveys related work; this work includes approaches to proving type abstraction, approaches to using syntactic proof techniques, and approaches to putting a notion of principal in a programming language.

This work extends our previously published paper [Zdancewic et al. 1999] by providing a more complete presentation of the two-agent and multiagent calculi and extensions that incorporate state, recursive types, and polymorphism.

2. THE TWO-AGENT CALCULUS

2.1 Syntax

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

Figure 3 gives the syntax for the two-agent calculus. Types, τ, include a base type, b, the host’s abstract type, t, and function types. The terms of the language are client terms, C, client values, Ĉ, host terms, H, and host values, Ĥ. The metavariable x_{c} ranges over client variables, which are disjoint from host variables, ranged over by x_{h}.

The metavariables b_{c} and b_{h} range over values of base type. We assume that the host and client use the same underlying representation for values of base type. These values are thus the fundamental medium of information exchange between agents. For example, the client value 3_{c} corresponds to the host value 3_{h}. It would be possible to relax this assumption; conversion between host and client values would then require computation (for instance to change the byte-order of integer

1Throughout this paper, we use the words “principal,” “agent,” and “color” interchangeably.

ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

\begin{aligned}τ & ::= & t | b | τ → τ′ \\ C & ::= & x_{c} | b_{c} | λx_{c}:τ. C | C C′ | ⌜ ⌞H⌝ ⌟_{h}^{τ} \\ Ĉ & ::= & b_{c} | λx_{c}:τ. C | ⌜ ⌞Ĥ⌝ ⌟t_{h} \\ H & ::= & x_{h} | b_{h} | λx_{h}:τ. H | H H′ | ⌜ ⌞C⌝ ⌟_{c}^{τ} \\ Ĥ & ::= & b_{h} | λx_{h}:τ. H \\ e & ::= & C | H \\ ê & ::= & Ĉ | Ĥ \end{aligned}

Fig. 3. Two-agent syntax.

values). One of the advantages of distinguishing principals is that places where such marshalling and unmarshalling is needed are made explicit in the program.

It is helpful to think of terms generated by C and H as having different colors (indicated by the subscripts c and h respectively) that indicate to which principal each belongs. As observed in the introduction, client 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 clients.

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 a client term. If the annotation is t, then the client has no information about the form of the term inside the embedding. Thus, an embedding with annotation t and containing a host value is a client value.

A good intuition for the semantics is to imagine two copies of the simply typed lambda calculus augmented with a new type t. In the client copy, t is abstract, whereas in the host copy, t is τ_{h}. Because the host has more knowledge, there is an asymmetry in the language. In the semantics, this asymmetry manifests itself in rules in which the host refines t to τ_{h}. It also means the notion of value depends on the principal and the type information: an embedding with annotation t is a client value. An embedding is never a host value because the annotation is never a type that is abstract to the host.

2.2 Notation

Before describing the semantics, we define some convenient notions. Let e range over both client and host terms, and let ê range over both client and host values. The color of e is c if e is a C term; otherwise, e’s color is h. Note that both terms in a syntactically well-formed application are the same color. Because the host and client terms share some semantic rules, we use polychromatic rules to range over both kinds of terms. The intention is that all terms mentioned in a polychromatic rule have the same color; the rule is short-hand for two analogous rules, one for each color.

We write {e′/x}e for the capture-avoiding substitution of e′ for x in e. Terms are equal up to alpha conversion, where substituted variables are of the same color. We also define substitution on types, written {τ′/t}τ. Intuitively, we use the sub-

ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

Polychromatic Steps [P1 ]  e e′ ⟼ e′′ e′ if e ⟼ e′′
[P2 ] ê e′ ⟼ ê e′′ if e′ ⟼ e′′
[P3 ]  (λx:τ. e) ê ⟼ {ê/x}e
Client Steps [C1 ]  ⌜ ⌞H⌝ ⌟_{h}^{τ} ⟼ ⌜ ⌞H′⌝ ⌟_{h}^{τ} if H ⟼ H′
[C2 ]  ⌜ ⌞b_{h}⌝ ⌟b_{h} ⟼ b_{c}
[C3 ] ⌜ ⌞λx_{h}:τ. H⌝ ⌟_{h}^{τ′→τ′′} ⟼ λx_{c}:τ′. ⌜ ⌞{⌜ ⌞x_{c}⌝ ⌟_{c}^{τ} /x_{h}}H⌝ ⌟_{h}^{τ′′}
Host Steps [H1 ]  ⌜ ⌞C⌝ ⌟_{c}^{τ} ⟼ ⌜ ⌞C′⌝ ⌟_{c}^{τ} if C ⟼ C′
[H2 ]  ⌜ ⌞b_{c}⌝ ⌟b_{c} ⟼ b_{h}
[H3 ] ⌜ ⌞λx_{c}:τ. C⌝ ⌟_{c}^{τ′→τ′′} ⟼ λx_{h}:{τ_{h}/t}τ′. ⌜ ⌞{⌜ ⌞x_{h}⌝ ⌟_{h}^{τ}/x_{c}}C⌝ ⌟_{c}^{τ′′}
[H4 ]  ⌜ ⌞⌜ ⌞Ĥ⌝ ⌟t_{h}⌝ ⌟_{c}^{τ_{h}} ⟼ Ĥ

Fig. 4. Two-agent dynamic semantics.

stitution {τ_{h}/t}τ to produce the host’s view of τ.

We say a client term is host-free if it contains no embeddings (and similarly for client-free host terms).

2.3 Dynamic Semantics

Figure 4 describes a small-step operational semantics for the two-agent calculus. The polychromatic rules are the same as for the simply typed call-by-value lambda calculus. The other rules handle embeddings.

Rules [C1 ] and [H1 ] allow evaluation to proceed within embeddings. Inside embeddings, the rules for the other color apply. These “context switches” ensure that terms evaluate with the appropriate rules 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 (see rules [C2 ] and [H2 ]). It is at this point that conversion between data representations would take place.

Rules [C3 ] and [H3 ] maintain the distinction between client and host code. For example, suppose the client contains a host function that is being exported at type τ′ → τ′′. In this case, the client does know that the embedding contains a function, so the client can apply it to an argument of a suitable type. If instead the function had been exported at type t, the client would not have been able to apply it. The subtlety is that the host type of the function may be more specific than the client type, such as when τ′ = t.

Thus, [C3 ] converts an embedded host function to a client function with an argument of type τ′. The body of the client version of the function is an embedding of the host code, except that, as the argument now comes from the client, every occurrence of the original argument variable, x_{h}, is replaced by an embedding of the client’s argument variable, ⌜⌞x_{c}⌝⌟_{c}^{τ}. This embedding is exported to the host at type τ, the type the host originally expected for the function argument. The rule for hosts, [H3 ], is symmetric, except that, because the host may use t as τ_{h}, occurrences of t in the host function’s type annotation are replaced by τ_{h}.

The final rule, [H4 ], allows the host to “open up” a client value that is an embedded host value. This rule allows the host to recover a value that has been

ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

(λopen_{c}:string → fh. open_{c} “myfile”_{c}) ⌜ ⌞λs_{h}:string. ho s_{h}⌝ ⌟_{h}^{string→fh}
(1) (λopen_{c}:string → fh. open_{c} “myfile”_{c}) (λs_{c}:string. ⌜ ⌞ho ⌜ ⌞s_{c}⌝ ⌟_{c}^{string}⌝ ⌟fh_{h})
(2) (λs_{c}:string. ⌜ ⌞ho ⌜ ⌞s_{c}⌝ ⌟_{c}^{string}⌝ ⌟fh_{h}) “myfile”_{c}
(3) ⌜ ⌞ho ⌜ ⌞“myfile”_{c}⌝ ⌟_{c}^{string}⌝ ⌟fh_{h}
(4) ⌜ ⌞ho “myfile”_{h}⌝ ⌟fh_{h}
⋮
(n) ⌜ ⌞3_{h}⌝ ⌟fh_{h}

Fig. 5. Client calling open.

embedded abstractly in the client. The restricted form of this rule ensures that the term inside the embedding is a value and is itself an embedding. (Specifically, if the annotation is not t, then the term is not a value.) Therefore, no other rule applies. This restriction keeps our system deterministic, a property that we find convenient, but that is probably not necessary.

The crucial point is that any attempt by the client to treat a value of type t as a function leads to a stuck configuration (no rule applies). 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 lambda calculus, allows us to prove the safety properties of Section 2.6.

2.4 Examples

We now give two examples of program evaluation in the two-agent calculus. Returning to our example of file handles, let t = fh and τ_{h} = int.

Figure 5 shows the client obtaining a file handle through a host interface. For simplicity, only the host’s open function is provided to the client. The host implementation, ho, takes in a string and produces an integer representing a file handle. This code is embedded inside the client at the more abstract type string → fh.

Step (1) uses [C3 ] to convert the embedded host function to a client function. Note that the new variable, s_{c}, is embedded in the host as a client term. Step (2) is a standard β-reduction. Together, these two reduction steps correspond to the linking of host and client code, but, unlike the example in Figure 2, there is no type information about fh given to the client code. Step (3) is another β-reduction, passing in the client string “myfile.” Step (4) uses [H2 ] to extract the string from the embedding. At this point, the host function ho is applied to a host value. Repeated use of [C1 ] allows the host function to proceed. We assume that ho returns 3 when applied to “myfile.” This result, embedded within the client code at type fh, is a client value.

The second example (Figure 6) illustrates the client calling the host’s read function, passing in the file handle ⌜⌞3_{h}⌝⌟fh_{h}. We assume the host code for read is already embedded in the client and exported at the type fh → char. The body of the host function is hr, a host term taking an integer representing a file handle and returning a character read from that file.

In step (1), the client extracts the host function via rule [C3 ]. The type of the argument handle_{c} is abstract in the client, so the type annotation is changed to

ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

⌜ ⌞λhandle_{h}:int. hr handle_{h}⌝ ⌟_{h}^{fh→char} ⌜ ⌞3_{h}⌝ ⌟fh_{h}

(1)  (λhandle_{c}:fh. ⌜ ⌞hr ⌜ ⌞handle_{c}⌝ ⌟_{c}^{int}⌝ ⌟_{h}^{char}) ⌜ ⌞3_{h}⌝ ⌟fh_{h}
(2)  ⌜ ⌞hr ⌜ ⌞⌜ ⌞3_{h}⌝ ⌟fh_{h}⌝ ⌟_{c}^{int}⌝ ⌟_{h}^{char}
(3)  ⌜ ⌞hr 3_{h}⌝ ⌟_{h}^{char}

⋮

(n)  ⌜ ⌞′A′_{h}⌝ ⌟_{h}^{char}
(n + 1) ′A′_{c}

Fig. 6. Client calling read.

Polychromatic Rules

[var] Γ ⊢ x : Γ(x)  [const] Γ ⊢ b : b  [app] \begin{matrix}Γ ⊢ e : τ′ → τ & Γ ⊢ e′ : τ′ \\ Γ ⊢ e e′ : τ \end{matrix}

Client Rules

[Cfn] {Γ[x_{c} : τ′] ⊢ C : τ \atop Γ ⊢ λx_{c}:τ′. C : τ′ → τ}  [HinC ] {Γ ⊢ H : \{τ_{h}/t\}τ \atop Γ ⊢ ⌜ ⌞H⌝ ⌟_{h}^{τ} : τ}

Host Rules

[Hfn] {Γ[x_{h} : τ′] ⊢ H : τ \atop Γ ⊢ λx_{h}:τ′. H : τ′ → τ} t ∉ τ′  [CinH ] {Γ ⊢ C : τ \atop Γ ⊢ ⌜ ⌞C⌝ ⌟_{c}^{τ} : \{τ_{h}/t\}τ}

Fig. 7. Two-agent static semantics.

fh. The second step is a β-reduction. At this point, evaluation continues via [H4 ], which in step (3) allows the embedded host code to extract the integer 3, held abstract by the client, as a host value. The application (hr 3_{h}) proceeds as usual until the host computes the character read from the file. At last, because this embedded character is exported to the client at type char, rule [C2 ] produces the value ′A′_{c}.

2.5 Static Semantics

Figure 7 describes the static semantics for the two-agent calculus. The typing context, Γ, maps variables (of either color) to types. The polychromatic rules are standard, as is the introduction rule for client functions. For host functions, the only difference is that t is not allowed to appear in the annotation for the argument to a function. Because the host knows that t = τ_{h}, this restriction does not limit expressiveness. The convenient effect of this side condition and rule [CinH ] is that types of host terms never contain t. The presence of t in host-function types would complicate other rules, such as [var] and [app], because we would often need to refine a type τ to {τ_{h}/t}τ in order for types to be preserved under evaluation.

The interesting typing rules are those for embeddings. Rule [HinC ] says that an embedded host term, H, exported to the client 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}/t}τ. In other words, the host may hide type information from the client by replacing some occurrences of τ_{h} with t in the exported type. The rule for clients embedded inside of host terms, [CinH ], is dual in that the host refines the types

ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

\begin{aligned}erase(x_{i}) & = & x \\ erase(b) & = & b \\ erase(λx:τ. e) & = & λx:\{τ_{h}/t\}τ. erase(e) \\ erase(e e′) & = & erase(e) erase(e′) \\ erase(⌜ ⌞e⌝ ⌟_{i}^{τ}) & = & erase(e) \end{aligned}

Fig. 8. Two-agent erase translation.

provided by the client.

2.6 Safety Properties

In this section, we explore properties of the two-agent calculus including soundness and some type-abstraction theorems. We defer the proofs because they are corollaries to the corresponding theorems in Sections 3.7 and 3.8. These properties are not intended to be as general as possible. Rather, they convey the flavor of some statements that are provable using syntactic arguments.

The following lemmas establish type soundness:

Lemma 2.1 (Canonical Forms). Assuming ∅ ⊢ ê: τ,

— if τ = b, then ê = b for some b.

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

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

Lemma 2.2 (Preservation). If ∅ ⊢ e : τ and e ⟼ e′ then ∅ ⊢ e′ : τ.

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

Definition 2.4. A term e is \underline{stuck} if it is not a value and there is no e′ such that e ⟼ e′.

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

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

Lemma 2.6 (Erasure). Let e be any two-agent term such that ∅ ⊢ e : τ. Then e ⟼^{∗} ê if and only if erase(e) ⟼^{∗} erase(ê).

The interesting fact is that the erasure of rule [C3 ] is basically λx : τ. e ⟼ λx′:τ. {x′/x}e; the substitution of τ_{h} for t in the erasure process ensures that the types of the bound variables on either side of the transition are the same. Because λx: τ. e is alpha equivalent to λx′: τ. {x′/x}e, the transition [C3 ] corresponds to the identity transition (zero steps) in the erased language.

With soundness and erasure established, we reexamine the abstraction properties of the introduction. Because the host is always capable of providing information to the client, we are particularly interested in evaluations where we assume the host

ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

does not do so. Recall that we say host-free to describe a client term that has no host terms embedded in it.

One desirable property of the file handle interface is that the client never breaks the type abstraction for file handles. For example, if C is host-free, ∅ ⊢ handle : fh, and ∅ ⊢ λf_{c} :fh. C : τ, then (λf_{c} :fh. C) handle never evaluates to a term in which handle is treated as an integer. This property is a corollary of type soundness because within the client code the type fh is not equal to int (and hence, for example, the expression f_{c} + 3 is not well-typed).

A stronger property is that the client is oblivious to the particular choice of integer that the host uses to represent a given file handle. More formally:

Theorem 2.7 (Independence of Evaluation). If ⌜⌞Ĥ⌝⌟fh_{h} and ⌜⌞Ĥ′⌝⌟fh_{h} are well-typed, C is host-free, and ∅ ⊢ λf_{c}:fh. C : fh → b, then (λf_{c}:fh. C) ⌜⌞Ĥ⌝⌟fh_{h} ⟼^{∗} b_{c} if and only if (λf_{c}:fh. C) ⌜⌞Ĥ′⌝⌟fh_{h} ⟼^{∗} b_{c}.

The proof strengthens the claim to a step-by-step evaluation correspondence when using Ĥ and Ĥ′:

Lemma 2.8 (Value Abstraction). Let Ĥ and Ĥ′ be host values of type τ_{h}. If C is host-free, [x_{c} : fh] ⊢ C : τ, and {⌜⌞Ĥ⌝⌟fh_{h}/x_{c}}C is not a value, then there exists a host-free term C′ such that:

— [x_{c} : fh] ⊢ C′ : τ
— {⌜⌞Ĥ⌝⌟fh_{h}/x_{c}}C ⟼ {⌜⌞Ĥ⌝⌟fh_{h}/x_{c}}C′
— {⌜⌞Ĥ′⌝⌟fh_{h}/x_{c}}C ⟼ {⌜⌞Ĥ′⌝⌟fh_{h}/x_{c}}C′

The embeddings also enable us to track expressions of the abstract type during evaluation, thus allowing us to formalize a third property: The client must have called open to obtain a file handle.

Theorem 2.9 (File Handles Come from open). Suppose C is host-free, ho is client-free, and λopen_{c}:string → fh. C is well-typed. If (λopen_{c}:string → fh. C) applied to ⌜⌞λs_{h}:string. ho s_{h}⌝⌟_{h}^{string→fh} steps to some term C′ containing ⌜⌞Ĥ⌝⌟fh_{h} as a subterm, then Ĥ was derived from a sequence of the form (ho Ĥ′) ⟼^{∗} Ĥ.

The proof shows that (after one step) every host embedding has as its embedded term either an application of ho or an intermediate result of such an application.

3. THE MULTIAGENT CALCULUS

So far, we have described a simple two-agent setting in which the host has strictly more information than the client. We can model many interesting cases in this fashion, but there are times when both principals wish to hide information or in which there are more than two agents involved. For example, we need a multiagent setting to prove safety properties about nested abstract data types.

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

ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

(agents) i, j ∈ {1, …, n}
(lists) ℓ ::= i | iℓ
(types) τ ::= t | b | τ → τ′
(i-terms) e_{i} ::= x_{i} | b_{i} | λx_{i}:τ. e_{i} | e_{i} e′_{i} | fix f_{i}(x_{i}:τ).e_{i} | ⌜ ⌞e_{j}⌝ ⌟_{ℓ}^{τ}
(i-primvals) v̂_{i} ::= b_{i} | λx_{i}:τ. e_{i}
(i-values) v_{i} ::= v̂_{i} | ⌜ ⌞v̂_{j}⌝ ⌟_{ℓ}^{t} (t ∉ Dom(δ_{i}))

Fig. 9. Multiagent syntax.

3.1 Syntax

Figure 9 shows the syntax for the multiagent language. The types include a base type, b, function types, and type variables ranged over by t. In what follows, we also use u and s to range over type variables.

Rather than just two colors of terms, we now assume that there are n agents, where n is fixed. We use the metavariables i, j, and k to range over the set of agents {1, …, n}.

Every nonembedding term has exactly one color, as indicated by the subscript. Embeddings also have a color that is determined by context—the grammar allows e_{i} and e_{j} to produce syntactically identical embedding terms. We explicitly state the color of the term when it is ambiguous or particularly relevant to the discussion. Functions and applications are always constructed from subterms of the same color.

The terms for agent i include variables, x_{i}, constants, b_{i}, nonrecursive functions, λx_{i}: τ. e_{i}, recursive functions, fix f_{i}(x_{i}:τ).e_{i}, function applications, e_{i} e′_{i}, and embeddings, ⌜⌞e_{j}⌝⌟_{ℓ}^{τ}. We include both recursive and nonrecursive functions to simplify the dynamic semantics (see rule [4 ] in Figure 10).

An embedding containing a j-term is labeled with a list of agents, ℓ, for reasons explained in Section 3.3. We write simply j for the singleton list containing the agent j, and we use juxtaposition to denote appending two lists (ℓℓ′ is the concatenation of lists ℓ and ℓ′). The static semantics requires that the list for an embedded j-term begins with j, so in fact ℓ = jℓ′ for the term ⌜⌞e_{j}⌝⌟_{ℓ}^{τ}; but we write just ℓ when the j is unimportant. We use rev(ℓ) to mean the list-reversal of ℓ.

3.2 Type Information

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. 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 should not be the case that j thinks fh = string.)

To capture this information, we assume each agent i has a finite partial map from type variables to types called δ_{i}. To maintain consistency of knowledge among agents, we require that all agents that know the implementation of an abstract type t know the same implementation. We further restrict the δ_{i} maps so that for each

ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

type variable, t, there is a unique, most concrete interpretation of t. For example, we do not allow δ_{i}(t) = t → t, or the more subtle δ_{i}(t) = s → s, δ_{j}(s) = t, because these examples do not admit a well-defined notion of most-concrete type for t.

The need for consistency among agents motivates the first part of the following definition; the need for most concrete interpretations of a type motivates the second part.

Definition 3.1. A set {δ_{1}, …, δ_{n}} of finite partial maps from type variables to types is \underline{compatible} if:

—For every i, j ∈ {1, …, n} if t ∈ Dom(δ_{i}) ∩ Dom(δ_{j}), then δ_{i}(t) = δ_{j}(t). —The collection of type variables can be totally ordered such that for every agent,

i, and type variable, t, all variables in δ_{i}(t) precede t.

Each δ_{i} extends naturally to a total function, Δ_{i} from types to types:

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

Applying Δ_{i} to a type τ either yields τ (if i has no information about the type variables appearing in τ) or a more concrete version of τ. For example, Δ_{h}(fh → fh) = int → int. We say that Δ_{i}(τ) refines τ, and we write ⊑_{i} for the reflexive, transitive closure of Δ_{i} viewed as a relation on types. Thus, fh → fh ⊑_{h} int → int.

The second condition in the definition of compatibility, and the fact that each agent has a finite amount of type information, guarantees that the process of an agent refining a type halts. That is, the sequence τ ⊑_{i} Δ_{i}(τ) ⊑_{i} Δ_{i}(Δ_{i}(τ)) ⊑_{i} … reaches a fixpoint, which we write Δ̄_{i}(τ). This fixpoint is the most concrete view of τ that agent i is able to determine from its knowledge.

Even if all of the agents pool their information about type variables, the notion of a most concrete view of τ is still valid. We write Φ for the union of the compatible Δ_{i} maps. It contains the composite knowledge of every agent in the system. Let ⊑ be the reflexive, transitive closure of the relation Φ. As above, the process of refining τ using Φ also terminates: τ ⊑ Φ(τ) ⊑ Φ(Φ(τ)) ⊑ … reaches a fixpoint. The notation Φ̄(τ) indicates this fixpoint, which is the most concrete type compatible with τ.

In practice, the compatibility constraints guarantee two things. First, no set of agents can conspire to show that incompatible types are equal (and thus effectively cast an integer to a function, for example). Second, there is a well-defined notion of most concrete type for each agent. The first criterion is clearly necessary for soundness of the system. The second criterion greatly simplifies the static semantics. There may be other notions of compatibility that relax one or both of these conditions while still admitting a sound type system and a well behaved semantics.

3.3 Embeddings

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. That is, ⌜⌞v̂_{j}⌝⌟_{ℓ}^{t} is an i-value if t ∉ Dom(δ_{i}).

ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

Because an embedding is not an i-primval, a nested embedding (for example, ⌜⌞⌜⌞λx_{j}: τ. x_{j}⌝⌟_{j}^{t}⌝⌟_{i}^{s}) is never an i-value. We could have made such terms values, but the result would significantly complicate the dynamic semantics: if our example nested embedding were passed to an agent that was able to refine s to an arrow type, then we would need to cross two embedding boundaries to find the function that the agent expects. Instead, our dynamic semantics collapses the two embeddings into one, in this case ⌜⌞λx_{j}: τ. x_{j}⌝⌟_{ji}^{s}. As a result, values never cross more than one embedding at a time, but the embeddings are now annotated with a list of agents.

Why is this somewhat complicated mechanism necessary? There must be some way of relating the type of a term inside an embedding to the type annotation on the embedding; otherwise, an agent could export an integer as a function. The list of agents allows us to maintain exactly the information needed to establish the connection between the type of the term inside an embedding and the type annotating the embedding. If we forget any agents, inconsistencies may arise. For example, consider three agents, i, j, and k, such that δ_{i}(t) = int, δ_{j}(s) = t, and δ_{k} = ∅. Then collapsing the k-term ⌜⌞⌜⌞3_{i}⌝⌟_{i}^{t}⌝⌟_{j}^{s} to either ⌜⌞3_{i}⌝⌟_{i}^{s} or ⌜⌞3_{j}⌝⌟_{j}^{s} violates the type-abstraction properties because neither i nor j knows that s abstracts an int. If we use sets of agents instead of (ordered) lists, the reasonable rules become too permissive because we lose the information that agent i must have exported the integer at type t before j could export it at type s. As we explain in Section 3.6, the type system admits the nested-embedding term and the collapsed version, ⌜⌞3_{i}⌝⌟_{ij}^{s}, but not the others.

In summary, the lists of agents on embeddings let us remember a particular order of principals, which is necessary for type checking, without treating nested embeddings as values.

3.4 Dynamic Semantics

Figure 10 shows the operational semantics for agent i in the multiagent language. That is, several of the rules depend on the color of the term being reduced, and the rules use i to denote this color.

Rules [1 ], [2 ], [4 ], and [5 ] establish a typical call-by-value semantics.^{2} Rule [3 ] allows evaluation inside embeddings. Rule [6 ] lets agent i pull a constant out of an embedding, provided that the constant is exported at type b. This rule corresponds to rules [C2 ] and [H2 ] of the two-agent scenario.

As in the two-agent case, in which the host had more type information than the client, 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. The side condition on this rule (in conjunction with the conditions on [8 ] and [9 ]) ensures that evaluation is deterministic. This determinism of the type-refinement rules is not critical to the system, but it makes many of the proofs easier because there is only one applicable rule for each evaluation step. The choice of when the operational semantics refines type information interacts with where we must apply the Δ_{i} maps in the static semantics; we chose to maintain the invariants that the static semantics always derives

2We believe the language can easily be adapted to a call-by-name setting.

ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

[1 ] {e_{i} ⟼ e′′_{i} \atop e_{i} e′_{i} ⟼ e′′_{i} e′_{i}}  [2 ] {e′_{i} ⟼ e′′_{i} \atop v_{i} e′_{i} ⟼ v_{i} e′′_{i}}  [3 ] {e_{j} ⟼ e′_{j} \atop ⌜ ⌞e_{j}⌝ ⌟_{ℓ}^{τ} ⟼ ⌜ ⌞e′_{j}⌝ ⌟_{ℓ}^{τ}}
[4 ]  fix f_{i}(x_{i}:τ).e_{i} ⟼ λx_{i}:τ. {fix f_{i}(x_{i}:τ).e_{i}/f_{i}}e_{i}
[5 ]  (λx_{i}:τ. e_{i}) v_{i} ⟼ {v_{i}/x_{i}}e_{i}
[6 ]  ⌜ ⌞b_{j}⌝ ⌟b_{ℓ} ⟼ b_{i}
[7 ]  ⌜ ⌞v̂_{j}⌝ ⌟_{ℓ}^{τ} ⟼ ⌜ ⌞v̂_{j}⌝ ⌟_{ℓ}^{Δ̄_{i}(τ)} (τ ≠ Δ̄_{i}(τ))
[8 ]  ⌜ ⌞⌜ ⌞v̂_{j}⌝ ⌟_{ℓ}^{u}⌝ ⌟_{kℓ′}^{τ} ⟼ ⌜ ⌞v̂_{j}⌝ ⌟_{ℓkℓ′}^{τ} (u ∉ Dom(δ_{k}), τ = Δ̄_{i}(τ))
[9 ] ⌜ ⌞λx_{j}:τ. e_{j}⌝ ⌟_{jℓ}^{τ′→τ′′} ⟼ λx_{i}:τ′. ⌜ ⌞{⌜ ⌞x_{i}⌝ ⌟_{irev(ℓ)}^{τ}/x_{j}}e_{j}⌝ ⌟_{jℓ}^{τ′′} (x_{i} fresh, τ′ → τ′′ = Δ̄_{i}(τ′ → τ′′))

Fig. 10. Multiagent dynamic semantics: e ⟼ e′ where color(e) = i.

the most concrete type for any term, and that types explicitly mentioned in the lambda-abstraction syntax are most concrete. It would be possible to reformulate the calculus so that these conditions are relaxed (by allowing a nondeterministic type-refinement rule in the static semantics), but doing so would require additional proof-normalization arguments.

Rule [8 ] is the multiagent generalization of rule [H4 ]. Both rules allow progress when we have nested embeddings, and the inner embedding cannot be reduced because the inner agent considers it a value. In the two-agent case, this situation can occur only when the outer agent is the host. Because we are not concerned with tracking what values the host manipulates, rule [H4 ] strips away both embeddings. However, in the more symmetric multiagent setting, naively stripping away embeddings loses information about which agents could have contributed information about the type of a term.

Rule [8 ] says that if there are nested embeddings, ⌜⌞⌜⌞v̂_{j}⌝⌟_{ℓ}^{u}⌝⌟_{kℓ′}^{τ}, and the inner embedding, ⌜⌞v̂_{j}⌝⌟_{ℓ}^{u}, is a k-value (that is, u ∉ Dom(δ_{k})), then the two embeddings can be collapsed into one, ⌜⌞v̂_{j}⌝⌟_{ℓkℓ′}^{τ}. Because we append the two lists, we lose no information about which agents have participated in the evaluation of the term.

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 that 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. Because the “inside type” and “outside type” have reversed roles, the list must be in reverse order. Intuitively, the agents that successively provided the function-argument type to i must undo their work in the body of the function. The side condition ensuring that the embedding’s type is most concrete with respect to the outer agent preserves the determinism of the semantics and ensures that the

ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

Assume δ_{h}(fh) = int and fh ∉ Dom(δ_{c})

(λy_{h}:int → int. y_{h} 3_{h}) ⌜ ⌞λx_{c}:fh. x_{c}⌝ ⌟_{c}^{fh→fh}

[7 ] (λy_{h}:int → int. y_{h} 3_{h}) ⌜ ⌞λx_{c}:fh. x_{c}⌝ ⌟_{c}^{int→int}
[9 ] (λy_{h}:int → int. y_{h} 3_{h}) (λx′_{h}:int. ⌜ ⌞⌜ ⌞x′_{h}⌝ ⌟fh_{h}⌝ ⌟_{c}^{int})
[5 ] (λx′_{h}:int. ⌜ ⌞⌜ ⌞x′_{h}⌝ ⌟fh_{h}⌝ ⌟_{c}^{int}) 3_{h}
[5 ] ⌜ ⌞⌜ ⌞3_{h}⌝ ⌟fh_{h}⌝ ⌟_{c}^{int}
[8 ] ⌜ ⌞3_{h}⌝ ⌟_{hc}^{int}
[6 ] 3_{h}

Fig. 11. Multiagent evaluation example.

explicit type for x_{i} is most concrete.

3.5 Example

As an example, we encode our two-agent calculus by letting δ_{h} map fh to int and letting δ_{c} be undefined everywhere. An evaluation that uses all of the novel rules appears in Figure 11. The host program invokes a client function defined in terms of the abstract type fh. (For simplicity, it is just the identity function.) The evaluation takes place in a host context, enabling the host to apply the function to the value 3 even though the client function expects an argument of type fh. Within the body of the client code, however, the host value 3 is wrapped in an embedding and must be treated abstractly. Even so, the host code is able to recover the value 3 returned by the client. The numbers in the figure are the reduction rules used to take the step. Note that under this simple system, rules [7 ] and [9 ] encode what was previously “hard-wired” into rule [H3 ]. Similarly, rules [8 ] and [6 ] do the work of [H4 ].

3.6 Static Semantics

Figure 12 shows the multiagent static semantics. Note that the rules depend on the color of the term and the value of the maps δ_{1}, …, δ_{n}. The rules use i to denote the color of the term. The values of the maps do not change, so we leave them implicit. Therefore, the judgment Γ ⊢ e_{i} : τ should be read as, “Under 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; they are analogous to the side condition on [Hfn] in the two-agent case. Similarly, the use of Δ̄_{i} in the conclusion of [embed] guarantees that an embedded term is viewed by agent i at the most concrete type possible. Formally, the convenient invariant we are maintaining is that Γ ⊢ e_{i} : τ implies Δ_{i}(τ) = τ.

The issue of consistency among agents arises during type checking. For instance, we do not want a principal to export an int as a function. Likewise, we do not want an agent, or collection of agents, to violate the type abstractions represented by the δ_{i} maps. Thus, we need to relate the type of the expression inside the embedding to the type annotation on the embedding.

ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

[const] Γ ⊢ b_{i} : b  [var] Γ ⊢ x_{i} : Γ(x_{i})  [app] \begin{matrix}Γ ⊢ e_{i} : τ′ → τ & Γ ⊢ e′_{i} : τ′ \\ Γ ⊢ e_{i} e′_{i} : τ \end{matrix}

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

[fix]  \begin{matrix}Γ[f_{i} : τ′ → τ][x_{i} : τ′] ⊢ e′_{i} : τ & Δ_{i}(τ′ → τ) = τ′ → τ \\ Γ ⊢ fix f_{i}(x_{i}:τ′).e′_{i} : τ′ → τ \end{matrix} (f_{i}, x_{i} ∉ Dom(Γ), f_{i} ≠ x_{i})

[embed]  \begin{matrix}Γ ⊢ e_{j} : τ′ & ⊢ τ′ ≲_{jℓi} τ \\ Γ ⊢ ⌜ ⌞e_{j}⌝ ⌟_{jℓ}^{τ} : Δ̄_{i}(τ) \end{matrix}

Fig. 12. Multiagent static semantics: Γ ⊢ e_{i} : τ.

[eq] {Δ̄_{i}(τ) = Δ̄_{i}(τ′) \atop ⊢ τ ≲_{i} τ′}  [trans] \begin{matrix}⊢ τ ≲_{ℓ} τ′′ & ⊢ τ′′ ≲_{ℓ′} τ′ \\ ⊢ τ ≲_{ℓℓ′} τ′ \end{matrix}
Fig. 13. Type relations: ⊢ τ ≲_{ℓ} τ′.

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

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.

3.7 Safety Properties

This section illustrates some of the standard safety theorems of typed programming languages and then presents an embedding-erasure transformation that commutes with evaluation.

The following standard lemmas help establish type soundness. The proofs are straightforward.

Lemma 3.2 (Canonical Forms). Assuming ∅ ⊢ v_{i} : τ,

— if τ = b, then v_{i} = b_{i} for some b.

— if τ = τ′ → τ′′, then v_{i} = λx_{i}:τ′. e′_{i} for some x_{i} and e′_{i}.

— if τ = t, then t ∉ Dom(δ_{i}) and v_{i} = ⌜⌞v̂_{j}⌝⌟_{jℓ}^{t} for some v̂_{j} and ℓ.

3We give a nondeterministic rule for [trans] because we are not concerned with an algorithmic presentation of type checking. This formulation lets us slightly simplify the proofs of the Type-Relations Properties, but is not essential to their correctness.

ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

Lemma 3.3 (Substitution). Suppose Γ[x_{j} : τ′] ⊢ e_{i} : τ and Γ ⊢ e_{j} : τ′. Then Γ ⊢ {e_{j}/x_{j}}e_{i} : τ.

We also need several properties about the ≲ relations.

Lemma 3.4 (Type-Relation Properties).

Idempotence: ⊢ τ ≲_{ℓiiℓ′} τ′ if and only if ⊢ τ ≲_{ℓiℓ′} τ′.

Reversal: If ⊢ τ ≲_{ℓ} τ′, then ⊢ τ′ ≲_{rev(ℓ)} τ.

Arrow: If ⊢ τ^{1} → τ^{2} ≲_{ℓ} τ^{3} → τ^{4}, then ⊢ τ^{1} ≲_{ℓ} τ^{3} and ⊢ τ^{2} ≲_{ℓ} τ^{4}.

Proofs of the first two properties are simple arguments by induction on the derivation of the type relation. Our proof of the last property requires a tedious normalization argument showing that if ⊢ τ^{1} → τ^{2} ≲_{ℓ} τ^{3} → τ^{4}, then there is a derivation that relates only types whose top-level constructors are arrows. We give a brief sketch of the argument: the proof is by induction on the length of the list ℓ. The base case, when ℓ is of length one, follows from the compatibility of the δ_{i} relations. The inductive case is straightforward if the types in the chain are all arrows, so we suppose that in a chain of types showing ⊢ τ^{1} → τ^{2} ≲_{ℓ} τ^{3} → τ^{4} the first type variable encountered is t. Then the type before t must be some τ^{5} → τ^{6}. After some number of type variables in the chain, we must again have some arrow type. From the consistency conditions on the δ_{i} maps, this next arrow type must be τ^{5} → τ^{6}. Hence we did not need the occurrence of t in the chain, and can simply replace it with τ^{5} → τ^{6}. In other words, any occurrences of type variables provide no additional information, so we can remove them, reducing the problem to a chain consisting only of arrow types.

We now have the results we need to prove the two main lemmas.

Lemma 3.5 (Preservation). If ∅ ⊢ e_{i} : τ and e_{i} ⟼ e′_{i}, then ∅ ⊢ e′_{i} : τ.

Proof. By induction on the derivation that e_{i} ⟼ e′_{i}. We proceed by cases on the last step of the derivation. Cases [1 ], [2 ], and [3 ] follow from induction. Cases [4 ] and [5 ] follow immediately from the Substitution Lemma. Case [6 ] is trivial to prove. We consider the remaining cases individually:

[7 ] We have a typing derivation as follows:

\begin{matrix}∅ ⊢ v̂_{j} : τ′′ & ⊢ τ′′ ≲_{jℓi} τ′ \\ ∅ ⊢ ⌜⌞v̂_{j}⌝⌟_{jℓ}^{τ′} : Δ̄_{i}(τ′) \end{matrix}

Because Δ̄_{i}(τ′) equals Δ̄_{i}(Δ̄_{i}(τ′)), by [eq] we have that ⊢ τ′ ≲_{i} Δ̄_{i}(τ′). Thus by [trans] we have that ⊢ τ′′ ≲_{jℓii} Δ̄_{i}(τ′), and we can remove the second i by Idempotence. We can now derive:

\begin{matrix}∅ ⊢ v̂_{j} : τ′′ & ⊢ τ′′ ≲_{jℓi} Δ̄_{i}(τ′) \\ ∅ ⊢ ⌜⌞v̂_{j}⌝⌟_{jℓ}^{Δ̄_{i}(τ′)} : Δ̄_{i}(τ′) \end{matrix}

The conclusion is the desired result.

ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

[8 ] We have a typing derivation as follows:

\begin{matrix}\begin{matrix}∅ ⊢ v̂_{j} : τ′′ & ⊢ τ′′ ≲_{jℓk} u \\ ∅ ⊢ ⌜⌞v̂_{j}⌝⌟_{jℓ}^{u} : Δ̄_{k}(u) \end{matrix} & ⊢ Δ̄_{k}(u) ≲_{kℓ′i} τ′ \\ ∅ ⊢ ⌜⌞⌜⌞v̂_{j}⌝⌟_{jℓ}^{u}⌝⌟_{kℓ′}^{τ′} : Δ̄_{i}(τ′) \end{matrix}

The fact that the inner embedding is labeled with a list starting with j follows from the Canonical Forms Lemma. Furthermore, u ∉ Δ_{k}, so Δ̄_{k}(u) = u. Thus by [trans] and the premises, we have ⊢ τ′′ ≲_{jℓkkℓ′i} τ′. So Idempotence proves that ⊢ τ′′ ≲_{jℓkℓ′i} τ′. We can now derive:

\begin{matrix}∅ ⊢ v̂_{j} : τ′′ & ⊢ τ′′ ≲_{jℓkℓ′i} τ′ \\ ∅ ⊢ ⌜⌞v̂_{j}⌝⌟_{jℓkℓ′}^{τ′} : Δ̄_{i}(τ′) \end{matrix}

The conclusion is the desired result.

[9 ] We have a typing derivation as follows:

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

Furthermore, the concreteness side condition on rule [9 ] implies that Δ_{i}(τ^{1} → τ^{2}) = τ^{1} → τ^{2}. So by the definition of Δ_{i}, we know that Δ_{i}(τ^{1}) = τ^{1} and Δ_{i}(τ^{2}) = τ^{2}. From the Arrow Lemma and the right-hand premise of the bottom step, we conclude that ⊢ τ^{0} ≲_{jℓi} τ^{1} and ⊢ τ^{3} ≲_{jℓi} τ^{2}. The reverse of jℓi is irev(ℓ)j, so by the Reversal Lemma, ⊢ τ^{1} ≲_{irev(ℓ)j} τ^{0}. Thus we can derive:

\begin{matrix}[x_{i} : τ^{1}] ⊢ x_{i} : τ^{1} & ⊢ τ^{1} ≲_{irev(ℓ)j} τ^{0} \\ [x_{i} : τ^{1}] ⊢ ⌜⌞x_{i}⌝⌟_{irev(ℓ)}^{τ^{0}} : Δ̄_{j}(τ^{0}) \end{matrix}

Because the original derivation provides Δ_{j}(τ^{0}) = τ^{0}, we conclude [x_{i} : τ^{1}] ⊢ ⌜⌞x_{i}⌝⌟_{irev(ℓ)}^{τ^{0}} : τ^{0}. It also provides [x_{j} : τ^{0}] ⊢ e_{j} : τ^{3}. Because x_{i} is fresh, we may weaken this claim to [x_{i} : τ^{1}][x_{j} : τ^{0}] ⊢ e_{j} : τ^{3}. Hence by Substitution, [x_{i} : τ^{1}] ⊢ {⌜⌞x_{i}⌝⌟_{irev(ℓ)}^{τ^{0}}/x_{j}}e_{j} : τ^{3}. So we can derive:

\begin{matrix}[x_{i} : τ^{1}] ⊢ \{⌜⌞x_{i}⌝⌟_{irev(ℓ)}^{τ^{0}}/x_{j}\}e_{j} : τ^{3} & ⊢ τ^{3} ≲_{jℓi} τ^{2} \\ [x_{i} : τ^{1}] ⊢ ⌜⌞\{⌜⌞x_{i}⌝⌟_{irev(ℓ)}^{τ^{0}}/x_{j}\}e_{j}⌝⌟_{jℓ}^{τ^{2}} : Δ̄_{i}(τ^{2}) \end{matrix} Δ_{i}(τ^{1}) = τ^{1}
∅ ⊢ λx_{i}:τ^{1}. ⌜⌞{⌜⌞x_{i}⌝⌟_{irev(ℓ)}^{τ^{0}}/x_{j}}e_{j}⌝⌟_{jℓ}^{τ^{2}} : τ^{1} → Δ̄_{i}(τ^{2})

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

Lemma 3.6 (Progress). If e is well-typed, then either e is a value or there exists an e′ such that e ⟼ e′.

Proof Sketch. The proof is a straightforward inductive argument on the structure of e. The interesting case is when e = e_{i} = ⌜⌞v_{j}⌝⌟_{ℓ}^{τ}. If Δ_{i}(τ) ≠ τ, then rule [7 ] applies. Else, if v_{j} is an embedding, then rule [8 ] applies. Otherwise, we proceed

ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

\begin{aligned}erase(x_{i}) & = & x \\ erase(b_{i}) & = & b \\ erase(λx_{i}:τ. e_{i}) & = & λx:Φ̄(τ). erase(e_{i}) \\ erase(fix f_{i}(x_{i}:τ).e_{i}) & = & fix f(x:Φ̄(τ)).erase(e_{i}) \\ erase(e_{i} e′_{i}) & = & erase(e_{i}) erase(e′_{i}) \\ erase(⌜ ⌞e_{j}⌝ ⌟_{ℓ}^{τ}) & = & erase(e_{j}) \end{aligned}

where Φ = ⋃_{i} Δ_{i}

Fig. 14. Multiagent erase translation.

by cases on the form of τ. If τ = b, rule [6 ] applies. If τ = τ′ → τ′′, rule [9 ] applies. Else e_{i} is a value.

Given the previous two lemmas, we conclude type safety:

Theorem 3.7 (Type Safety). If ∅ ⊢ e : τ, then there is no stuck e′ such that e ⟼^{∗} e′.

The cost of including embeddings is the addition of several dynamic rules. Worse yet, with recursion and multiple agents, the lists annotating embeddings might grow arbitrarily large. The erasure property stated below essentially shows that these syntactic tricks are only a proof technique.

For erasure to a typed language, it is necessary to combine the type information of all the agents. The multiagent definition of erase is given in Figure 14, where we recall that Φ is the map obtained by taking the union of the compatible Δ_{i} maps. Φ̄(τ) is the most concrete type for τ that can be found using all n agents’ knowledge.

The target language has one agent and no embeddings.

Lemma 3.8 (Erasure). If e_{i} is well-typed then either both e_{i} and erase(e_{i}) diverge or e_{i} ⟼^{∗} v_{i} and erase(e_{i}) ⟼^{∗} erase(v_{i}).

Proof Sketch. By induction on the number of steps in the source derivation. For one step, show that if e_{i} ⟼ e′_{i}, then either erase(e_{i}) = erase(e′_{i}) or erase(e_{i}) ⟼ erase(e′_{i}). That is, the erased version takes either zero steps (if the source step uses one of rules [6 ] through [9 ]) or one step (if the source step uses rule [4 ] or [5 ]). For divergence, show the contrapositive—any term erasing to a nondiverging term is nondiverging. The essence of the argument is that the source derivation can take only a finite number of steps before using rules [4 ] or [5 ].

3.8 Type-Abstraction Properties

In this section, we use subject-reduction arguments to prove type-abstraction properties that generalize those of the two-agent case.

Definition 3.9. Let \underline{Agents(e_{i})} be the set of colors appearing in e_{i}. (The set necessarily includes i as well as any agents appearing in lists annotating embedding subterms of e_{i}.)

Definition 3.10. A set of agents, S, is \underline{oblivious} to type t if for all i ∈ S, t ∉ Dom(δ_{i}).

ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

Theorem 3.11 (Independence of Evaluation). Let e_{i} be a term such that Agents(e_{i}) are oblivious to t and ∅ ⊢ λx_{i}:t. e_{i} : t → b. Let v̂_{j} and v̂′_{j} be closed, well-typed terms with type Δ̄_{j}(t). Then (λx_{i}:t. e_{i}) ⌜⌞v̂_{j}⌝⌟_{j}^{t} ⟼^{∗} b_{i} if and only if (λx_{i}:t. e_{i}) ⌜⌞v̂′_{j}⌝⌟_{j}^{t} ⟼^{∗} b_{i}.

First note that v̂_{j} and v̂′_{j} are primitive values. Hence ⌜⌞v̂_{j}⌝⌟_{j}^{t} and ⌜⌞v̂′_{j}⌝⌟_{j}^{t} are values. Also, we know j ∉ Agents(e_{i}): because v̂_{j} is a constant or a function and ⌜⌞v̂_{j}⌝⌟_{j}^{t} is well-typed, [embed] ensures that t ∈ Dom(δ_{j}). Agents(e_{i}) are oblivious to t, so j ∉ Agents(e_{i}).

The proof of the theorem strengthens the claim to a step-by-step evaluation correspondence when using v̂_{j} and v̂′_{j}. We give the intuition before presenting the formal lemma: we maintain that the intermediate terms in the two evaluation sequences are always exactly the same except that every occurrence of v̂_{j} in one is replaced with v̂′_{j} in the other. To ensure this correspondence, we show that every occurrence of v̂_{j} is safely within an embedding with a type that agents other than j can relate to t. These agents are oblivious to t, so the embedding’s type must be at least as abstract as t. We also maintain that there are no j-terms other than the ones we are abstracting and that j appears nowhere in an embedding list except as the first element. These conditions suffice to argue that j never helps the other agents break the type abstraction.

More specifically, properties (1) and (2) of φ (defined in the lemma) suffice to show that Agents(e_{i}) \ {j} cannot distinguish values of type t without the help of agent j; properties (3), (4), and (5) suffice to show that j does not provide such help.

Lemma 3.12 (Value Abstraction). Let v̂_{j} and v̂′_{j} have type Δ̄_{j}(t). Let φ(e_{i}) mean:

(1 ) [x_{j} : Δ̄_{j}(t)] ⊢ e_{i} : τ for some τ. (2 ) Agents(e_{i}) \ {j} are oblivious to t. (3 ) The only j-term in e_{i} is x_{j}. (It may appear zero, one, or more times.) (4 ) If ⌜⌞x_{j}⌝⌟_{jℓ}^{τ} is a k-term in e_{i}, then ⊢ t ≲_{ℓk} τ. (5 ) j never appears in an embedding list within e_{i} except as the first element.

Then if φ(e_{i}) and {v̂_{j}/x_{j}}e_{i} ⟼ e_{i}^{1}, then there exists an e_{i}^{2} such that:

(a) φ(e_{i}^{2})

(b) {v̂_{j}/x_{j}}e_{i}^{2} =_{α} e_{i}^{1}

(c) {v̂′_{j}/x_{j}}e_{i} ⟼ {v̂′_{j}/x_{j}}e_{i}^{2}

Proof Sketch. By induction on the derivation of {v̂_{j}/x_{j}}e_{i} ⟼ e_{i}^{1}, proceeding by cases on the last rule used in the derivation.

Rules [1 ], [2 ], and [3 ] essentially follow from induction and the definition of substitution. Note that for [3 ], the embedded term is not a j-term because the only j-term, v̂_{j}, is a value.

Rules [4 ] and [5 ] follow from the definition of substitution and the fact that the variable for which we substitute a term must be distinct from x_{j} because the term and x_{j} are different colors. Furthermore, v̂_{j} is closed, so the substitution has no effect on it.

ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

Rule [6 ] is trivial except that we must prove the term inside the embedding is not v̂_{j} (otherwise e_{i}^{1} = v̂_{i}, so property (c) will not hold). Assume for contradiction the term inside is v̂_{j}. Then by property (3), before the substitution this term was x_{j}. Then by properties (4) and (5), a j-free list of agents, ℓ, can show ⊢ t ≲_{ℓ} b. A simple proof by induction on the rules for ≲_{ℓ} shows that this conclusion contradicts property (2).

Rules [7 ] and [8 ] are straightforward to verify. Note that in [8 ] the outer agent list cannot contain j because of properties (3) and (5).

Rule [9 ] requires an analogous argument to the one we used in [6 ] to show that the term inside the embedding cannot be x_{j}. Hence the agent list on the embedding does not contain j, so property (5) is preserved even though the agent list is reversed. The substitution in the body of the function is unproblematic because v̂_{j} is closed and therefore unaffected.

This lemma suffices to prove Independence of Evaluation because, given the assumptions of the theorem, φ((λx_{i}:t. e_{i}) ⌜⌞x_{j}⌝⌟_{j}^{t}). By induction on the length of the evaluation, property (b) holds for b_{i}, where b_{i} is the result of the evaluation with v̂_{j}. This implies that the same b_{i} must be the result of the evaluation with v̂′_{j} because the two results are alpha equivalent.

The generalization of Theorem 2.9 is the following theorem. It effectively says that a client containing a value of abstract type fh must have obtained that value via a host-provided function.

Theorem 3.13 (Host-Provided Values). Suppose prog is a closed and welltyped term of the form (λopen_{i} : b → fh. client)⌜⌞λx_{h} : b. ho⌝⌟_{h}^{b→fh}. Further suppose Agents(client) are oblivious to fh, h knows fh, ho is embedding-free, and prog ⟼^{∗} e_{i}. Then any subterm of e_{i} that is a closed value of type fh has the form ⌜⌞v̂_{h}⌝⌟fh_{hℓ}, and there exists an e_{h} such that {e_{h}/x_{h}}ho ⟼^{∗} v̂_{h} and erase(e_{h}) = b for some base value b.

Note that it is not necessarily the case that {b_{h}/x_{h}}ho ⟼^{∗} v̂_{h} because Δ̄_{h}(fh) could be a function type and because the dynamic semantics does not evaluate under functions. Also note that we make no restrictions on the agents in client and their type abstractions except that none of them know the implementation of fh. For example, one agent could export fh more abstractly to another agent.

The proof consists of an intricate subject-reduction argument, so we first present the general idea. Intuitively, the only h terms are ho and the result of applying ho to an argument. Because only h knows fh, all values of type fh come from applying ho. The main complication is tracking all the functions that are essentially λx_{h}: b. ho except that they differ in color and embeddings: The first step of prog uses [9 ] to convert ⌜⌞λx_{h} : b. ho⌝⌟_{h}^{b→fh} to λx_{i} : b. ⌜⌞{⌜⌞x_{i}⌝⌟b_{i}/x_{h}}ho⌝⌟fh_{h}, so we must consider the latter term a legitimate producer of file handles. Agent i could pass this term to another agent using [9 ] again, and that result must also be legitimate.

Due to these complications, we carefully state a property that evaluation of a well-typed term preserves: Figure 15 presents two relations, φ(e) and ψ(e), where as usual, we mean the least relations closed under the appropriate inference rules. In the rules, we assume the color of e does not know fh; we use colors j and k to

ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

[A] φ(b)  [B] φ(x)

[C ] \begin{matrix}φ(e) & φ(e′) \\ φ(e e′) \end{matrix} [D] {φ(e) \atop φ(λx:τ. e)} [E] {φ(e) \atop φ(fix f(x:τ).e)} [F] \begin{matrix}φ(e) & h ∉ ℓ \\ φ(⌜ ⌞e⌝ ⌟_{ℓ}^{τ}) \end{matrix}

[G] \begin{aligned}\{e_{h}/x_{h}\}ho ⟼^{∗} e′_{h} & erase(e_{h}) = b & ∅ ⊢ e_{h} : b & ⊢ fh ≲_{ℓ′} τ & h ∉ ℓℓ′ \\ & φ(⌜ ⌞e′_{h}⌝ ⌟_{hℓ}^{τ}) \end{aligned}

[H ] {ψ(e) \atop φ(e)} [I ] ψ(λx_{j}:b. ⌜ ⌞\{⌜ ⌞x_{j}⌝ ⌟b_{j}/x_{h}\}ho⌝ ⌟fh_{h})

[J ] \begin{matrix}ψ(λy_{k}:τ^{1}. ⌜ ⌞e⌝ ⌟_{ℓ}^{τ^{2}}) & ⊢ τ^{3} ≲_{jrev(ℓ′)} τ^{1} & h ∉ ℓ′ \\ ψ(λx_{j}:τ^{3}. ⌜ ⌞⌜ ⌞\{⌜ ⌞x_{j}⌝ ⌟_{jrev(ℓ′)}^{τ^{1}}/y_{k}\}e⌝ ⌟_{ℓ}^{τ^{2}}⌝ ⌟_{kℓ′}^{τ^{4}}) \end{matrix}
[K ] ψ(⌜ ⌞λx_{h}:b. ho⌝ ⌟_{h}^{b→fh})

Fig. 15. Host-Provided Values preservation property.

range over any such color. We implicitly assume the context of the Host-Provided Values Theorem, so λx_{h}:b. ho is closed, well-typed, and embedding-free.

Rules [A] through [F ] are just structural rules; we use them to “find the important terms,” namely the functions that are essentially λx_{h} : b. ho and the results of applying such functions. No other h-terms are allowed.

Rule [G] accepts terms that are the (intermediate) results of applying such functions. Because such functions differ from ho in terms of embeddings, [G] does not require that e = ⌜⌞e′_{h}⌝⌟_{hl}^{τ} where there exists a v_{h} such that {v_{h}/x_{h}}ho ⟼^{∗} e′_{h}. Rather, v_{h} may be a nonvalue e_{h} so long as its erasure is a value.

Rule [H ] accepts the terms that are essentially λx_{h}:b. ho by using the auxiliary relation ψ. Rule [I ] accepts the function we have after one step of prog. For each time that the function is passed to another agent via rule [9 ], we use the rule [J ] to conclude that the resulting function is still acceptable. We include rule [K ] so that φ(prog) holds. It is easy to show that ψ(e) implies e is closed and well-typed.

It is straightforward to prove that if φ(e) is preserved under evaluation then the Host-Provided Values Theorem is true: first verify that φ(prog). Therefore, φ(e_{i}) for any e_{i} such that prog ⟼^{∗} e_{i}. A simple induction on the derivation of φ(e_{i}), appealing to the canonical forms of values as necessary, suffices to prove that for any subterm v that is a closed value of type fh, it must be that φ(v). Rule [G] is necessary to derive φ(v), and the antecedents of this rule are strong enough to prove the theorem. (A separate inductive argument shows that if ψ(e), then no subterm of e is a closed value of type fh.)

We now proceed with the rigorous proof that φ is preserved. As usual, the subject-reduction argument relies on a substitution lemma that we prove before presenting the main lemma.

Lemma 3.14 (Host-Provided Substitution). If φ(e), φ(e′) and color(e′) = color(x), then φ({e′/x}e).

Proof. The proof is by induction on the derivation of φ(e), proceeding by cases

ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

on the last rule in the derivation. Cases [A] and [B] are trivial. Cases [C ], [D], [E], [F ] follow from straightforward inductive arguments. Case [G] follows because {e_{h}/x_{h}}ho is closed and evaluation preserves this property. Case [H ] follows because ψ(e) implies that e is closed (as shown by induction on the derivation of ψ(e)).

Lemma 3.15 (Host-Provided Preservation). If φ(e), ∅ ⊢ e : τ, and e ⟼ e′, then φ(e′).

Proof. The proof is by induction on the derivation of e ⟼ e′, proceeding by cases on the last rule in the derivation.

[1 ] Follows from the induction hypothesis and [C ].

[2 ] Follows from the induction hypothesis and [C ].

[3 ] The derivation of φ(e) ends with [F ] or [G]. (Note that [H ] is impossible because ψ(e) holds only for values or embeddings of values, which do not fit the conditions of [3 ].) If [F ], then the result follows from the induction hypothesis and [F ]. If [G], then we know e = ⌜⌞e′_{h}⌝⌟_{hℓ}^{τ} and {e_{h}/x_{h}}ho ⟼^{n} e′_{h} for some n and appropriate e_{h}. Therefore, we know that {e_{h}/x_{h}}ho ⟼^{n+1} e′′_{h} and e′ = ⌜⌞e′′_{h}⌝⌟_{hℓ}^{τ}. So we can use [G] to derive φ(e′).

[4 ] Follows from the induction hypothesis, [E], Host-Provided Substitution, and [D].

[5 ] Then e = (λx_{j}: τ′. e′′) v_{j}, v_{j} has type τ′, and the derivation ends with [C ]. Therefore, φ(v_{j}) and φ(λx_{j} : τ′. e′′); the derivation of the latter ends in [D] or [H ]. If [D], then the result follows from the induction hypothesis, [D], and Host-Provided Substitution. If [H ], then ψ(λx_{j} : τ′. e′′), the derivation ending in [I ] or [J ]. Therefore, e′′ has the form ⌜⌞e′′′⌝⌟_{ℓ}^{τ′′}. It suffices to show that φ({v_{j}/x_{j}}⌜⌞e′′′⌝⌟_{ℓ}^{τ′′}). To prove this fact, we prove that ψ(λx_{j} : τ′. ⌜⌞e′′′⌝⌟_{ℓ}^{τ′′}), φ(v_{j}), and v_{j} has type τ′ implies two stronger facts:

—erase(v_{j}) = b for some b —For any e_{j} of type τ′, if there is a b such that φ(e_{j}) and erase(e_{j}) = b, then

φ({e_{j}/x_{j}}⌜⌞e′′′⌝⌟_{ℓ}^{τ′′}).

It is clear that this strengthened claim suffices. We prove it by induction on the derivation of ψ(λx:τ′. ⌜⌞e′′′⌝⌟_{ℓ}^{τ′′}), proceeding by cases on the last rule used.

For case [I ], τ′ = b, so the first fact follows from the Canonical Forms Lemma and the well-typedness of e. For the second fact, {e_{j}/x_{j}}⌜⌞e′′′⌝⌟_{ℓ}^{τ′′} = ⌜⌞{⌜⌞e_{j}⌝⌟b_{j}/x_{h}}ho⌝⌟fh_{h}. So [G] applies by letting e_{h} = ⌜⌞e_{j}⌝⌟b_{j} and e′_{h} = {e_{h}/x_{h}}ho.

For case [J ], we have λx_{j} : τ′. ⌜⌞e′′′⌝⌟_{ℓ}^{τ′′} = λx_{j} : τ^{3}. ⌜⌞⌜⌞{⌜⌞x_{j}⌝⌟_{jrev(ℓ′)}^{τ^{1}}/y_{k}}e^{1}⌝⌟_{ℓ}^{τ^{2}}⌝⌟_{jℓ′}^{τ^{4}}.

Furthermore, we have from the derivation that ψ(λy_{k}:τ^{1}. ⌜⌞e^{1}⌝⌟_{ℓ}^{τ^{2}}) and ⊢ τ^{3} ≲_{jrev(ℓ′)} τ^{1}. From the induction hypothesis, we conclude that if some v_{k} has type τ^{1} and φ(v_{k}), then erase(v_{k}) = b for some b. Because ⊢ τ^{3} ≲_{jrev(ℓ′)} τ^{1}, we can use the Canonical Forms Lemma to conclude that if v_{j} has type τ^{3}, then erase(v_{j}) = b, which is our first obligation. From the induction hypothesis, we know that for any e_{k} of type τ^{1} such that φ(e_{k}) and erase(e_{k}) = b, we know φ({e_{k}/y_{k}}⌜⌞e^{1}⌝⌟_{ℓ}^{τ^{2}}). So for arbitrary e_{j} such that φ(e_{j}) and erase(e_{j}) = b, we let e_{k} = ⌜⌞e_{j}⌝⌟_{jrev(ℓ′)}^{τ^{1}} to conclude

ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

that φ({⌜⌞e_{j}⌝⌟_{jrev(ℓ′)}^{τ^{1}}/y_{k}}⌜⌞e^{1}⌝⌟_{ℓ}^{τ^{2}}). Therefore, from the definition of substitution, we

have φ(⌜⌞{e_{j}/x_{j}}{⌜⌞x_{j}⌝⌟_{jrev(ℓ′)}^{τ^{1}}/y_{k}}e^{1}⌝⌟_{ℓ}^{τ^{2}}). Finally, because h ∉ ℓ′, we can use rule [F ]

and the definition of substitution to derive φ({e_{j}/x_{j}}⌜⌞⌜⌞{⌜⌞x_{j}⌝⌟_{jrev(ℓ′)}^{τ^{1}}/y_{k}}e^{1}⌝⌟_{ℓ}^{τ^{2}}⌝⌟_{jℓ′}^{τ^{4}}, which is our second obligation.

[6 ] Immediate because φ(b).

[7 ] Then the derivation of φ(e) ends with [F ] or [G]. (Note that [H ] is impossible because that derivation would have to end with [K ], but no nonhost agent can refine b → fh.) For either [F ] or [G], inspection of the antecedents reveals that the same rule applies after the step.

[8 ] Then each of the last two steps of the derivation of φ(e) are [F ] or [G]. (Note that [H ] is impossible because [K ] is not a nested embedding and b → fh is not a type variable.) If both are [F ], then the induction hypothesis and one use of [F ] let us conclude φ(e′). If the last step is [F ] and the second-to-last step is [G], then the induction hypothesis and one use of [G] let us conclude φ(e′). Note that the welltypedness of e suffices to satisfy the requirement that the type on the annotation be more abstract than fh. The remaining cases have [G] as the last step; we show by contradiction this situation is impossible. Suppose the derivation of φ(e) ends in [G]. Then the e′_{h} in the consequent of the rule is an h-value of the form ⌜⌞v̂_{j}⌝⌟_{ℓ}^{u} and u ∉ δ_{h}. But ho is embedding-free and ∅ ⊢ e_{h} : b, so it is easy to show that {e_{h}/x_{h}}ho cannot evaluate to a value that is an embedding.

[9 ] Then the derivation of φ(e) ends in [H ] or [F ]. (Note that [G] is impossible because Agents(client) are oblivious to fh, so τ must be at least as abstract as fh.) If the derivation ends in [H ], we know e = ⌜⌞λx_{h} : b. ho⌝⌟_{h}^{b→fh} and therefore e′ = λx_{i} : b. ⌜⌞{⌜⌞x_{i}⌝⌟b_{i}/x_{h}}ho⌝⌟fh_{h}, so [I ] lets us conclude φ(e′). If the derivation ends with [F ], we know the second-to-last step is [D] or [H ]. If [D], then the result follows from Host-Provided Substitution, [F ], and [D]. If [H ], then we know ψ(λy:τ^{1}. ⌜⌞e′′⌝⌟_{ℓ′}^{τ^{2}}) where e = ⌜⌞λy:τ^{1}. ⌜⌞e′′⌝⌟_{ℓ′}^{τ^{2}}⌝⌟_{ℓ}^{τ^{3}→τ^{4}}. (Either [I ] or [J ] could be the last rule used to derive this result; e has this form in both cases.) Therefore, we can use [J ] and [H ] to derive φ(e′). Note that the well-typedness of e and the fact that h ∉ ℓ suffice to satisfy the antecedents of [J ].

It is worth considering how we could generalize this proof and proof technique. Generalizing the means by which clients obtain file handles is straightforward. The function ho is just an example of a constructor; it is an expression that is exported at a type in which fh appears in a positive position. By tracking these constructors, we can show that all abstract values originate from them. More generally, using syntax and subject reduction to track the flow of values requires that we can always “find” the interesting terms, which is the purpose of rules [A] through [F ]. Rule [G] describes the property of interest (in this case that the term came from an invocation of the host implementation of open). The auxiliary predicate ψ describes how the host term can appear after being exported to any number of agents—embeddings can pile up, but only in a uniform way which does not change the underlying code, only the interface at which the code is available.

ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

4. REFERENCES AND STATE

In this section, we augment the program states of the preceding development with a mutable store and appropriate expressions for manipulating the store. The goal is to extend our type-abstraction results to a stateful setting without being unduly restrictive.

The next section is a brief overview of our formalization of state, ignoring issues regarding agents and type abstraction. The point is simply to establish basic notation for the discussion that follows. Our work follows closely the standard treatment of references in a subject-reduction setting, e.g., see the work of Wright and Felleisen [1994] or Harper [1994]. We then give an informal description of the issues that make the store a particularly interesting addition to our framework. Then we formally augment our calculus with state and discuss the reasons for particular design decisions. Finally, we augment the proofs of type soundness and safety properties appropriately.

4.1 Notation

Ignoring types and agents, a store, M, is a partial map from labels to values. The collection of labels is an infinite set; we use l to range over its members. A program state is a pair of a store and a closed expression, and the dynamic semantics operates on program states. Three new expression forms allow a program to manipulate the store. Reference creation, ref v, evaluates to a fresh label, l, and extends the store to map l to v. Dereference, !l evaluates to M(l) where M is the current store. Update, l := v, evaluates to v and changes the current store to map l to v.

So that we may give appropriate types to labels, we add a unary type constructor ref. Under store M, the values of type ref τ are those l such that M(l) has type τ. The static semantics ensures that well-formed program states refer only to labels defined in the store. This restriction applies to the store itself, not just to the closed expression. Hence, stores and expressions are well-formed relative what labels are in the store and what types these labels have. Store types, ranged over by Ψ, formalize these assumptions as a partial map from labels to types.

Figure 16 summarizes the preceding considerations by presenting the syntax and semantics for a lambda calculus with state. Note that the rule for store wellformedness permits the store to contain cycles.

4.2 Problems with State

Although the semantics associated with our stateful calculus is well understood, discussing type abstraction between principals in such a setting is considerably more complicated. Here we present examples of the difficulties.

The first difficulty is that the expressions that a program may use in its evaluation are not syntactically captured by the subterms of an expression. That is, we previously described some client expression, C, as host-free, but now we must account for C obtaining host code from the store. For example, in the expression (!l ⌜⌞v⌝⌟t_{h}), whether or not the evaluation is independent of the value of v depends on the value of M(l) where M is the current store. An obvious solution is to define “host-free” over the entire program state (M, C), but this solution is unnecessarily restrictive. Instead, our safety theorems use a notion of expressions reachable from C in (M, C).

ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

Syntax

τ ::= b | τ → τ′ | ref τ
e ::= v | x | e e′ | fix f(x:τ).e | ref e | e := e′ | !e
v ::= b | l | λx:τ. e

Dynamic Semantics

{(M, e_{1}) ⟼ (M′, e′_{1}) \atop (M, e_{1} e_{2}) ⟼ (M′, e′_{1} e_{2})}  {(M, e_{2}) ⟼ (M′, e′_{2}) \atop (M, v_{1} e_{2}) ⟼ (M′, v_{1} e′_{2})}

{(M, e_{1}) ⟼ (M′, e′_{1}) \atop (M, e_{1} := e_{2}) ⟼ (M′, e′_{1} := e_{2})} {(M, e_{2}) ⟼ (M′, e′_{2}) \atop (M, v_{1} := e_{2}) ⟼ (M′, v_{1} := e′_{2})}

{(M, e) ⟼ (M′, e′) \atop (M,!e) ⟼ (M′,!e′)}  {(M, e) ⟼ (M′, e′) \atop (M, ref e) ⟼ (M′, ref e′)}
(M, (λx:τ. e) v) ⟼ (M, {v/x}e)  (M,!l) ⟼ (M, M(l))
(M, ref v) ⟼ (M[l ↦ v], l) l fresh (M, l := v) ⟼ (M[l ↦ v], v)
(M, fix f(x:τ).e) ⟼ (M, λx:τ. {fix f(x:τ).e/f}e)

Static Semantics

\begin{matrix}⊢ M : Ψ & Ψ; ∅ ⊢ e : τ \\ ⊢ (M, e) : τ \end{matrix} Dom(M) = Dom(Ψ) ∀l ∈ Dom(M). Ψ; ∅ ⊢ M(l) : Ψ(l)

⊢ M : Ψ
Ψ; Γ ⊢ x : Γ(x)  Ψ; Γ ⊢ b : b  Ψ; Γ ⊢ l : ref Ψ(l)

\begin{matrix}Ψ; Γ ⊢ e : τ′ → τ & Ψ; Γ ⊢ e′ : τ′ \\ Ψ; Γ ⊢ e e′ : τ \end{matrix}  {Ψ; Γ[x : τ′] ⊢ e : τ \atop Ψ; Γ ⊢ λx:τ′. e : τ′ → τ} x ∉ Dom(Γ)

{Ψ; Γ[f : τ′ → τ][x : τ′] ⊢ e : τ \atop Ψ; Γ ⊢ fix f(x:τ′).e : τ′ → τ} f, x ∉ Dom(Γ), f ≠ x  {Ψ; Γ ⊢ e : ref τ \atop Ψ; Γ ⊢! e : τ}
Ψ; Γ ⊢ e : ref τ Ψ; Γ ⊢ e′ : τ
Ψ; Γ ⊢ e := e′ : τ

Ψ; Γ ⊢ e : τ

Ψ; Γ ⊢ ref e : ref τ

Fig. 16. Lambda calculus with state.

The second difficulty is that the store provides a new medium for interagent communication. For example, the client could assign to a shared reference that the host then dereferences. Suppose that l is a shared reference and that the program evaluates the client program state (M, l := ⌜⌞v⌝⌟t_{h}). If we interpret this program to mean that M(l) is now ⌜⌞v⌝⌟t_{h}, then, from the host’s perspective, the store now contains a client term. If we mean M(l) is now ⌜⌞⌜⌞v⌝⌟t_{h}⌝⌟_{c}^{τ_{h}}, then the store now contains a nonvalue. The dual case is also a potential problem: if the host assigns v of type τ_{h} to l and then the client dereferences l, the result must be a client expression that preserves the type abstraction.

In general, when a reference is assigned, we do not know which agents will dereference the value. Despite this lack of knowledge, the semantics must create the

ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

correct embeddings to allow a syntactic account of type abstraction. Fortunately, because all expressions are colored, we do know which agent last assigned to a reference.

The third difficulty is that the host should not provide the client the same reference as a ref t and a ref τ_{h}. Using a let notation as syntactic sugar for function application, an expression that violates this requirement could have the form

let r_{h} = ref v
let client = ⌜⌞λx_{c}:ref t. λy_{c}:ref τ_{h}. e⌝⌟_{c}^{ref τ_{h}→ref τ_{h}→τ}
client r_{h} r_{h}

To see the problem, consider what the values of !x_{c} and !y_{c} should be in the body of the client function, e, after the application client r_{h} r_{h}. An answer that preserves the types of the expressions is !x_{c} = ⌜⌞v⌝⌟t_{h} and !y_{c} = ⌜⌞v⌝⌟_{h}^{τ_{h}} respectively, but this answer requires that the dynamic semantics depends on the types of x_{c} and y_{c}. This dependence is undesirable in the substitution-based semantics we use. This approach is even less sensible if we consider a code fragment within e such as:

\begin{matrix}let = y_{c} := (v′ : τ_{h}) \\ !x_{c} \end{matrix}

Because the agent knows τ_{h}, it can construct a value v′ of this type and assign it to the shared reference. The ensuing dereference cannot preserve the type of !x_{c} unless it is something like ⌜⌞v′⌝⌟t_{h}, but v′ is not a host-provided term.

Even if we could somehow resolve the subject-reduction issues exemplified above, the resulting system can still break type abstraction. The example we give below is well-known in the context of the ML programming language; the same device works in that setting [Pierce and Sangiorgi 1999]. If the client term e can determine that values of types ref t and ref τ_{h} are the same value, then it can correctly conclude that t = τ_{h}. The following client fragment makes such a determination using aliasing information. We assume only that the client can distinguish two values of type τ_{h}, call them v_{1} and v_{2}.

let = y_{c} := v_{1}
let abs_{1} =!x_{c}
let = y_{c} := v_{2}
let = x_{c} := abs_{1}
if !y_{c} == v_{1}
then“aha, t = τ_{h}”

Given these problems, the challenge is to prohibit an agent from viewing the contents of the same reference at two different levels of abstraction. In so doing, we should not otherwise restrict the language’s expressiveness.

4.3 The Revised Calculus

Before presenting the formal calculus, we summarize how we solve the problems just outlined.

ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

The definition of host-free is straightforward: an expression e′ is reachable from (M, e) if e′ is a subterm of e or l is a subterm of e and e′ is reachable from (M, M(l)).^{4} (M, e) is host-free if all terms reachable from (M, e) are client terms.

To correctly handle interagent communication through the store, we make the semantics of the dereference operator depend on the color of the expression currently stored in the reference. For example, if M(l) = v_{c}, then (M,!l_{h}) ⟼ (M, ⌜⌞v_{c}⌝⌟_{c}^{τ}) because l_{h} and v_{c} are different colors. (To know what type τ to put on the embedding, we annotate labels with types—see below.) Conversely, (M,!l_{c}) ⟼ (M, v_{c}). This technique requires only that every expression (even an embedding) has one color and that we can determine this color at run time. Intuitively, a value is embedded precisely when it is received by a different agent.

Alternatively, we could have made all dereference operations return embeddings. Allowing i-embeddings in i code is perfectly reasonable—in fact, our multiagent calculus does not prevent it. We choose not to take this approach because we prefer to introduce embeddings precisely when interagent communication occurs. Although our theorems do not rely on the fact that intraagent evaluation does not introduce embeddings, we find this fact aesthetically pleasing. (If crossing an embedding boundary requires computation to change data representation, avoiding these redundant embeddings reduces computational overhead.)

Finally, we prevent an agent from exporting a reference at different levels of abstraction. To enforce this restriction syntactically, we associate a type expression with each label, l_{i}^{τ}, and reference creation expression, ref_{τ} e. Such expressions have type ref τ and must be exported at precisely ref τ, or at a fully abstract type, such as t. So the host must decide when creating a reference at what level of abstraction it will expose the contents of the reference. To prevent exposing a reference at a different level of abstraction, the rules for relating the type on an embedding annotation to the type of the embedded value do not substitute for any types under the ref constructor.

Of course, the host could allow the client to access a reference of type ref t by also providing functions get = ⌜⌞λx_{h}: ref t. !x_{h}⌝⌟_{h}^{ref t→τ_{h}} and set = ⌜⌞λx_{h}: τ_{h}. λy_{h}: ref t. y_{h} := x_{h}⌝⌟_{h}^{t→ref t→t}. It might appear, then, that the client could use get and set to encode the aliasing example above that breaks type abstraction. However, because we assume that the client does not know the function bodies associated with get and set, the client cannot ever conclude for sure that two references of different types are aliases. After all, get could perform other computation that happened to evaluate to the contents of the supposedly aliased value. In other words, the correctness of the aliasing device relies on the atomic, completely specified behavior of the assignment and dereference operators.

Having given some intuition for our design decisions, we now present the augmented calculus. We extend the multiagent calculus because the symmetry of this calculus actually simplifies much of the presentation, but we explain the system in terms of the familiar host and client example.

First, recall that δ_{i} is a finite partial map from type variables to types; it encodes what type variables agent i knows. (So in the two-agent case, δ_{h} maps t to τ_{h} and

4Because we are generally concerned with stores of finite size, we interpret this definition inductively; otherwise, a coinductive interpretation is warranted.

ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

[!1 ] (M, ref_{τ} v_{i}) ⟼ (M[l^{τ} ↦ v_{i}], l_{i}^{τ}) l^{τ} fresh [!2 ] (M, l_{i}^{τ} := v_{i}) ⟼ (M[l^{τ} ↦ v_{i}], v_{i})

[!3 ]  {color(M(l^{τ})) = i \atop (M,!l_{i}^{τ}) ⟼ (M, M(l^{τ}))}  [!4 ]  {color(M(l^{τ})) = j ≠ i \atop (M,!l_{i}^{τ}) ⟼ (M, ⌜ ⌞M(l^{τ})⌝ ⌟_{j}^{τ} )}

[!5 ]  {(M, e_{j}) ⟼ (M, e′_{j}) \atop (M, ⌜ ⌞e_{j}⌝ ⌟_{ℓ}^{τ} ) ⟼ (M, ⌜ ⌞e′_{j}⌝ ⌟_{ℓ}^{τ} )}  [!6 ]  (M, ⌜ ⌞l_{j}^{τ} ⌝ ⌟_{ℓ}^{ref τ} ) ⟼ (M, l_{i}^{τ})

Fig. 17. Dynamic semantics with state (partial): (M, e) ⟼ (M′, e′) where color(e) = i.

δ_{c} is the empty map.) We extend δ_{i} to a function Δ_{i} on types that does not operate under the ref constructor:

Δ_{i}(b) = b
Δ_{i}(t) = \{ \begin{matrix}t & t ∉ Dom(δ_{i}) \\ δ_{i}(t) & t ∈ Dom(δ_{i}) \end{matrix}
Δ_{i}(τ → τ′) = Δ_{i}(τ) → Δ_{i}(τ′)
Δ_{i}(ref τ) = ref τ

Hence a value of type ref τ is exported either abstractly or as ref τ, but not at ref τ′ for τ′ ≠ τ.

In the two-agent case, we previously wrote Δ_{h} as {τ_{h}/t}τ and Δ_{c} as the identity function. Using syntax that suggests substitution is now misleading because substitution does not occur under ref. As before, Δ̄_{i}(τ) = ⨆_{n≥0} Δ_{i}^{n}(τ), which in the one-abstract-type case is just Δ_{i}.

The dynamic semantics is a straightforward combination of the multiagent semantics presented in Figure 10 and the stateful semantics presented in Figure 16. Specifically, the system is defined by

—Rules [4 ]–[9 ] in Figure 10, suitably extended so that they operate on program

states and do not modify the store. —The top six rules in Figure 16, which allow evaluation to proceed in subexpres-

sions of applications and state operations. —Rules for evaluating the state operations and allowing evaluation within an em-

bedding, as shown in Figure 17.

Rules [!3 ] and [!4 ] enforce our decision to introduce embeddings when the heap facilitates interagent communication. Rule [!6 ] allows an agent to extract a label from an embedding when the agent has sufficient type information to know that the embedding contains a label. Note that the type on the label is τ, and the type on the embedding is ref τ; this equality is consistent with our definition of Δ_{i}.

The interesting additions to the static semantics appear in Figure 18. To obtain the full semantics, include the rules presented in Figures 12 and 13 with the modification that all typing judgments include the store type Ψ in the context.

Store contents are typechecked according to their color. Hence a reference may hold a value of any color. In the two-agent setting, this policy means that if lt contains a host value, then that value must have type τ_{h} under the host’s static semantics; but if the reference contains an agent value, then the value must have

ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

[heap1 ]  \begin{matrix}⊢ M : Ψ & Ψ; ∅ ⊢ e_{i} : τ \\ ⊢ (M, e) : τ \end{matrix}

[heap2 ]

Dom(M) = Dom(Ψ)
∀l^{τ} ∈ Dom(M). (Ψ; ∅ ⊢ M(l^{τ}) : τ′ Δ̄_{i}(τ) = τ′ color(M(l^{τ})) = i)
⊢ M : Ψ

[label]

l^{τ} ∈ Dom(Ψ)
Ψ; Γ ⊢ l_{i}^{τ} : ref τ [ref ]

Ψ; Γ ⊢ e_{i} : τ′ Δ̄_{i}(τ) = τ′
Ψ; Γ ⊢ ref_{τ} e_{i} : ref τ

[assign]

Ψ; Γ ⊢ e_{i} : ref τ Ψ; Γ ⊢ e′_{i} : τ′ Δ̄_{i}(τ) = τ′

Ψ; Γ ⊢ e_{i} := e′_{i} : τ′ [deref ]

Ψ; Γ ⊢ e_{i} : ref τ
Ψ; Γ ⊢!e_{i} : Δ̄_{i}(τ)

Fig. 18. Static semantics with state (partial).

type t under the agent’s static semantics. Note this treatment requires that we can determine the color of M(l^{τ}).

We maintain the convenient invariant that Ψ; Γ ⊢ v_{i} : τ implies τ = Δ_{i}(τ). Because references have the type with which they are annotated, this invariant means the type of the dereference operation must explicitly be Δ̄_{i}(τ) where the reference has type ref τ. The rules for reference creation and assignment require the subexpression that evaluates to the reference’s eventual contents to have type Δ̄_{i}(τ). In other words, i must know that τ is a legitimate abstraction of τ′, which by our invariant is most concrete.^{5} For example, in our two-agent system, consider reft v where v has type τ_{h}. This expression is well-formed if it is a host term, but not if it is an agent term.

The rule for relating the type on an embedding to the type of the embedded expression prevents a ref τ from being exported at any reference type other than ref τ even if ref τ is a constituent of another type. This important fact follows from the definition of the ≲_{ℓ} relation, which is defined in terms of the Δ_{i} maps. In the two-agent case, the right antecedent of rule [embed] is simply Δ_{h}(τ) = τ′ for host terms and τ = τ′ for agent terms.

4.4 Safety Properties

The type soundness and erasure results that we established for the calculi without state extend naturally to the stateful calculus. Therefore, we only present the aspects of the theorems and proofs that pertain to the additional rules.

The Canonical Forms Lemma now describes the form of v_{i} based on τ, assuming that Ψ; ∅ ⊢ v_{i} : τ. The addition is that if τ = ref τ′, then v_{i} has the form l_{i}^{τ′}.

For the sake of type soundness, the Substitution Lemma still need describe only substitution over expressions, as opposed to program states. This simplicity is because the dynamic semantics substitutes through only expressions. As we will see, however, the Independence of Evaluation Lemma needs definitions for substitution through program states and well-formedness of open stores (that is, stores that may contain values with free variables).

5An equivalent antecedent is ⊢ τ ≲_{i} τ′; it is equivalent because τ′ = Δ_{i}(τ′).

ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

The Preservation Lemma now expresses that evaluation extends the store consistently. Together with a Store Weakening Lemma, stating that store extensions cannot change the type of an expression, the induction hypothesis is strong enough.

Lemma 4.1 (Store Weakening). If Ψ′ is an extension of Ψ and Ψ; Γ ⊢ e : τ, then Ψ′; Γ ⊢ e : τ.

Lemma 4.2 (Preservation). If ⊢ M : Ψ, Ψ; ∅ ⊢ e : τ, and (M, e) ⟼ (M′, e′), then there exists a Ψ′ such that Ψ′ extends Ψ, ⊢ M′ : Ψ′, and Ψ′; ∅ ⊢ e′ : τ.

Note that this strengthening of Preservation is precisely what is needed to extend the lambda calculus with state; principals add no complications. As for the proof, the careful use of Δ̄_{i} in the static semantics makes it routine. Recall that the proof is by induction on the derivation that (M, e) ⟼ (M′, e′). We show only the cases for the rules in Figure 17. The other cases are either simple restatements of the analogous cases from the proof without state or trivial inductive arguments using the Store Weakening Lemma.

Proof.

[!1 ] By assumption, there must be a derivation of the form

Ψ; ∅ ⊢ v_{i} : τ′ Δ̄_{i}(τ) = τ′ Ψ; ∅ ⊢ ref_{τ} v_{i} : ref τ.

Letting M′ = M[l^{τ} ↦ v_{i}] and Ψ′ = Ψ[l^{τ} ↦ τ], we have Ψ′ extends Ψ. Because we know ⊢ M : Ψ, to prove ⊢ M′ : Ψ′, it suffices to prove Ψ′; ∅ ⊢ v_{i} : τ′ and Δ̄_{i}(τ) = τ′. These facts follow from the antecedents of the static derivation and the Store Weakening Lemma. Our final obligation, Ψ′; ∅ ⊢ l_{i}^{τ} : ref τ, follows from the definition of Ψ′ and the static semantics.

[!2 ] By assumption, there must be a derivation of the form

\begin{matrix}Ψ; ∅ ⊢ l_{i}^{τ} : ref τ & Ψ; ∅ ⊢ v_{i} : τ′ & Δ̄_{i}(τ) = τ′ \\ Ψ; ∅ ⊢ l_{i}^{τ} := v_{i} : τ \end{matrix}.

Letting M′ = M[l^{τ} ↦ v_{i}] and Ψ′ = Ψ we have that M′ and Ψ′ are extensions of M and Ψ respectively. We have from the hypothesis of the derivation that Ψ; ∅ ⊢ v_{i} : τ′, so we have to show only that ⊢ M′ : Ψ. Because we already know ⊢ M : Ψ, this conclusion follows from Ψ; ∅ ⊢ v_{i} : τ′ and Δ̄_{i}(τ) = τ′.

[!3 ] and [!4 ] By assumption, there must be a derivation of the form

{Ψ; ∅ ⊢ l_{i}^{τ} : ref τ \atop Ψ; ∅ ⊢!l_{i}^{τ} : Δ̄_{i}(τ)}.

Letting M′ = M and Ψ′ = Ψ, we need to show only that Ψ; ∅ ⊢ v_{i} : Δ̄_{i}(τ). There are two cases: color(M(l^{τ})) = i or not. First assume color(M(l^{τ})) = i. Then v_{i} = M(l^{τ}). It follows from the hypotheses needed to prove ⊢ M : Ψ that Ψ; ∅ ⊢ v_{i} : τ′ and Δ̄_{i}(τ) = τ′ from which the conclusion is immediate. Now assume M(l^{τ}) is a different color. Then v_{i} = ⌜⌞M(l^{τ})⌝⌟_{j}^{τ}. By the argument given for the other case, we know Ψ; ∅ ⊢ M(l^{τ}) : τ′ and Δ̄_{j}(τ) = τ′. Hence by [eq] we conclude τ′ ≲_{j} τ. Hence [embed] applies, and its conclusion is the desired result.

[!5 ] By induction.

ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

[!6 ] By assumption, there must be a derivation of the form

l^{τ} ∈ Dom(Ψ) Ψ; ∅ ⊢ l_{j}^{τ} : ref τ ⊢ ref τ ≲_{ℓi} ref τ Ψ; ∅ ⊢ ⌜⌞l_{j}^{τ} ⌝⌟_{ℓ}^{ref τ} : Δ̄_{i}(ref τ).

Because Δ̄_{i}(ref τ) = ref τ and from hypothesis we have l^{τ} ∈ Dom(Ψ), we can derive Ψ; ∅ ⊢ l_{i}^{τ} : ref τ using [label]. Letting M′ = M and Ψ′ = Ψ, we are done.

The statement of the Progress Lemma remains unchanged other than to use program states instead of expressions. The additions to the proof are entirely straightforward. In the case of (M, ⌜⌞v̂_{j}⌝⌟_{ℓ}^{τ}), there is one additional case because τ could have the form ref τ′. In this case, Canonical Forms guarantees that v̂_{j} has the form l_{j}^{τ′}, so we can take a step using [!6 ].

Defining erasure from this stateful language with embeddings to the calculus in Figure 16 such that erasure commutes with evaluation is straightforward, so we omit the details. Note that the target of this transformation does not include explicit types on labels; these explicit types have no real dynamic effect.

Extending the Value Abstraction Lemma (to which the Independence of Evaluation Theorem is a corollary) to our stateful calculus is straightforward except for some technical distractions. First, we must use the notion of reachable expressions, which includes expressions in the store, instead of the simpler notion of subterms. Second, the Value Abstraction Lemma uses substitution (such as {v̂_{j}/x_{j}}e_{i}) to establish a correspondence between two evaluations. To use this technique, we extend the definition of substitution to work on stores in a pointwise fashion. Otherwise the Lemma would not apply if an agent stored ⌜⌞v̂_{j}⌝⌟_{jℓ}^{τ} in the store and, hence, would not be strong enough to prove the Independence of Evaluation Theorem. Substituting through a store requires that we define a well-formed open store with respect to a context Γ, so that Γ ⊢ M : Ψ makes sense. The correct definition is the obvious generalization: Γ ⊢ M : Ψ if for all l^{τ} ∈ Dom(M), Ψ; Γ ⊢ M(l^{τ}) : τ′ and Δ̄_{i}(τ) = τ′, where M(l^{τ}) is a possibly-open i-value.

Extending the Host-Provided Values Theorem to our stateful calculus is also straightforward. Essentially, the preservation property needs to be inductively defined to include all terms that are reachable from the current program state without considering the trusted ho term. That is, ho can maintain private state without invalidating the theorem.

5. POLYMORPHISM AND RECURSIVE TYPES

In this section, we explore the extension of the multiagent language of Section 3 to include recursive types and polymorphism. Both of these mechanisms define type variables: the type μα.τ(α) establishes the equation α = τ(α). Instantiation of a polymorphic value, e:∀α.τ, at type τ′ establishes a context in which α = τ′ and e has type τ (that is, {τ′/α}τ).

Because the δ_{i} maps of the multiagent calculus already provide a way of expressing equalities of the form α = τ, we may try to encode recursive or polymorphic types using them. The current multiagent language is not sufficient to encode either of them. The following sections discuss the consequences of adding the necessary mechanisms.

ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

(types) τ ::= … | α | μα.τ
(i-terms) e_{i} ::= … | roll_{μα.τ} e_{i} | unroll e_{i}
(i-primvals) v̂_{i} ::= … | roll_{μα.τ} v_{i}

[μ1 ]

e_{i} ⟼ e′_{i}
roll_{μα.τ} e_{i} ⟼ roll_{μα.τ} e′_{i} [μ2 ]

e_{i} ⟼ e′_{i}
unroll e_{i} ⟼ unroll e′_{i}
[μ3 ] unroll roll_{μα.τ} v_{i} ⟼ v_{i}
[μ4 ] ⌜ ⌞roll_{μα.τ} v̂_{j}⌝ ⌟_{jℓ}^{μα.τ′} ⟼ roll_{μα.τ′} ⌜ ⌞v̂_{j}⌝ ⌟_{jℓ}^{{μα.τ′/α}τ′} (μα.τ′ = Δ̄_{i}(μα.τ′))

[roll]

{Γ ⊢ e_{i} : \{μα.τ/α\}τ \atop Γ ⊢ roll_{μα.τ} e_{i} : μα.τ}

[unroll]

Γ ⊢ e_{i} : μα.τ

Γ ⊢ unroll e_{i} : {μα.τ/α}τ

Fig. 19. Recursive types as an orthogonal extension.

5.1 Recursive Types

There are two general approaches for adding recursive types to the multiagent language. The first way is straightforward, and it interacts well with the previous results about the language. The idea is to treat μ-bound type variables as separate entities from the type variables that are used for abstraction (they could be drawn from the same syntactic class, but separating them makes for cleaner presentation). Figure 19 contains the necessary additions to the language.

The new types include recursive type variables, ranged over by α, and the recursive types themselves, μα.τ. Terms roll and unroll mediate the isomorphism between μα.τ and {μα.τ/α}τ. If v_{i} is an i-value, then roll_{μα.τ} v_{i} is an i-primval. The typing judgments for the new forms are standard.^{6} The operational rules [μ1 ], [μ2 ], and [μ3 ] are also standard—they allow progress under a roll or unroll and establish that composing unroll with roll is the identity.

The new rule, [μ4 ], propagates the embedding on a roll expression that is exported at a concrete type. It is similar to rule [9 ] used for embedded functions in that the outer agent may have different information about the nature of the recursive type. For instance, the outer agent may know that the value is of type μα.1+t×α, the type of t-lists, whereas the inner agent, for whom δ_{j}(t) = int views the value as an int-list.^{7} The side condition on [μ4 ] ensures that the dynamic semantics are deterministic—rule [7 ] applies to a disjoint collection of terms.

The only remaining change needed to establish the soundness of this system is to extend the definition of Δ_{i} in terms of δ_{i}.

\begin{aligned}Δ_{i}(μα.τ) & = & μα.Δ_{i}(τ) \\ Δ_{i}(α) & = & α \end{aligned}

6As in the case for λ-abstractions, types annotating roll terms are required to be the most concrete possible, but we do not need to apply Δ_{i} because the concreteness of the type in the antecedent implies the concreteness of the type on the roll. 7We did not formally add product and sum types to our framework, but doing so is straightforward. For example, ⌜ ⌞inleft_{τ^{0}+τ^{1}}e_{j}⌝ ⌟_{ℓ}^{τ^{2}+τ^{3}} ⟼ inleft_{τ^{2}+τ^{3}}⌜ ⌞e_{j}⌝ ⌟_{ℓ}^{τ^{2}} when τ^{2} and τ^{3} are most concrete.

ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

Because the μ-bound type variables are syntactically distinct from the abstraction type variables, it makes no sense for α to be in the domain of δ_{i}. To avoid problems with capture, we prohibit free occurrences of α in the range of δ_{i}.

Having made these additions to the language, it is straightforward to establish type soundness. To establish Preservation for the case of [μ4 ], we need a typerelations lemma that is analogous to the Arrow Lemma used in the case of [9 ]:

Lemma 5.1 (μ Type Relations). If ⊢ μα.τ ≲_{ℓ} μα.τ′, then ⊢ {μα.τ/α}τ ≲_{ℓ} {μα.τ′/α}τ′

The most interesting case of the proof of preservation is when the last rule of the dynamic derivation is [μ4 ]:

Proof. By assumption, we have a derivation of the form

{∅ ⊢ e_{j} : \{μα.τ/α\}τ \atop ∅ ⊢ roll_{μα.τ} e_{j} : μα.τ} ⊢ μα.τ ≲_{jℓi} μα.τ′ ∅ ⊢ ⌜⌞roll_{μα.τ} e_{j}⌝⌟_{jℓ}^{μα.τ′} : Δ̄_{i}(μα.τ′).

Using the right antecedent and Lemma 5.1, we conclude that ⊢ {μα.τ/α}τ ≲_{jℓi} {μα.τ′/α}τ′. So using the top antecedent, we can derive

\begin{matrix}∅ ⊢ e_{j} : \{μα.τ/α\}τ & ⊢ \{μα.τ/α\}τ ≲_{jℓi} \{μα.τ′/α\}τ′ \\ ∅ ⊢ ⌜⌞e_{j}⌝⌟_{jℓ}^{\{μα.τ′/α\}τ′} : Δ̄_{i}(\{μα.τ′/α\}τ′) \end{matrix}.

By assumption, we have the side condition Δ̄_{i}(μα.τ′) = μα.τ′. From this condition, it is easy to show that Δ̄_{i}({μα.τ′/α}τ′) = {Δ̄_{i}(μα.τ′)/α}Δ̄_{i}(τ′) = {μα.τ′/α}τ′. So we can derive

{∅ ⊢ ⌜⌞e_{j}⌝⌟_{jℓ}^{\{μα.τ′/α\}τ′} : \{μα.τ′/α\}τ′ \atop ∅ ⊢ roll_{μα.τ′} ⌜⌞e_{j}⌝⌟_{jℓ}^{\{μα.τ′/α\}τ′} : μα.τ′}.

The Progress Lemma is routine; it uses an extension of the Canonical Forms Lemma that asserts that i-values of type μα.τ have the form roll_{μα.τ} v_{i}.

This way of dealing with recursive types has the advantage of simplicity: because the presence of recursive types is orthogonal to the kind of type abstraction allowed by embeddings, all of the proofs of safety properties in Section 3 require minimal changes to account for the new constructs.

Another approach to incorporating recursive types into this system requires us to change the notion of compatibility of the Δ_{i} maps to account for cycles. Given a recursive type μα.τ, observe that the rolled values behave essentially abstractly. There is only one destructor for the term roll_{μα.τ} v_{i}, namely, unroll. This observation suggests that we can encode recursive types like so: Let r and u be fresh type variables. Create a special agent, r, whose sole function is to provide the roll and unroll operations for a recursive type. From the type perspective, r knows that r = {u/α}τ, i.e., δ_{r}(r) = {u/α}τ, and δ_{r} is otherwise undefined. For any client agent, i, who wishes to use values of type μα.τ, let δ_{i}(u) = r. The terms encoding roll_{μα.τ} x and unroll x are

ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

roll_{μα.τ} ≡ ⌜⌞λx_{r}:{u/α}τ. x_{r}⌝⌟_{r}^{{u/α}τ→r}
unroll ≡ ⌜⌞λx_{r}:{u/α}τ. x_{r}⌝⌟_{r}^{r→{u/α}τ}

The type variable r acts like the type μα.τ. As expected, the agent r provides identity functions that outwardly appear to clients as having the types appropriate to roll and unroll: {r/α}τ → r and r → {r/α}τ, respectively.

Although this approach is initially appealing, it requires substantial changes to the language. The essential difficulty is that there may not be a most concrete form for a given type variable, due to the possibly cyclic nature of the type information.

Two reasonable alternatives are (1) move to an operational semantics in which types are refined nondeterministically, or (2) require that each agent’s type information be acyclic, even if there are cycles globally. Neither of these options is satisfactory. The first makes reasoning about the behavior of programs unduly complicated. The second choice means that giving more type information to an agent can destroy a system’s compatibility. Both suffer from the problem that erasure (to a typed language) is harder to establish.

There may be merit in further considering this approach, particularly if the agents are module-level constructs and if the concern is mutually recursive data types that cross module boundaries. For a core language, however, the simplicity of the first approach and its compatibility with our previous proofs make it more valuable.

5.2 Polymorphism

The primary difference between polymorphism and the type abstraction already present in the multiagent calculus is one of scope: the abstract types present in the multiagent calculus are global and static, whereas a polymorphic instantiation is local to part of the program. That is, the application (Λα. e) τ introduces the type equality α = τ within the scope of the expression e. A second difference between type abstraction and polymorphism is that, in the latter, the same type variable may be instantiated at different types, for example,

λx:∀α.α → α. (… (x [int]) … (x [bool]) …).

It appears that α = int holds for part of the term whereas α = bool holds for a different part of the term.

This second difference is superficial, however. Because the α in x’s type is bound in ∀α.α → α, we are free to rename it for each occurrence of x in the body. We can think of the term (x [int]) as establishing the equation α = int whereas in the second term we choose the type of x to be (the equivalent type) ∀β.β → β, and thus (x [bool]) defines β = bool. In this way, each type application can establish the concrete form of a distinct type variable.

The true distinction, then, between our type-abstraction mechanism and polymorphism is local scoping. As with our first approach to recursive types, we could include both features separately. Instead, we investigate how to extend our framework to unify type abstraction and polymorphism via a single mechanism. Bridging the gap between the two features amounts to allowing the definitions of the δ_{i} maps to change during evaluation. We use the notation {Δ} to mean a set of type maps {Δ_{1}, …, Δ_{n}}; it captures the type knowledge each agent has at a particular point

ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

(types) τ ::= … | ∀α.τ
(i-terms) e_{i} ::= … | Λα. e_{i} | e_{i} [τ]
(i-primvals) v̂_{i} ::= … | Λα. e_{i}

Dom{Δ} = ⋃_{i} Dom(δ_{i})

\begin{matrix}[∀1 ] & ⟨\{Δ\}, (Λα. e_{i}) [τ]⟩ & ⟼ & ⟨\{Δ\} ⊎_{i} \{α = τ\}, \{τ/α\}_{i}e_{i}⟩ \\ [∀2 ] & ⟨\{Δ\}, ⌜ ⌞Λα. e_{j}⌝ ⌟_{ℓ}^{∀α.τ} ⟩ & ⟼ & ⟨\{Δ\}, Λα. ⌜ ⌞e_{j}⌝ ⌟_{ℓ}^{τ} ⟩ \end{matrix}

[∀intro] {Θ, α; \{Δ\}; Γ ⊢ e_{i} : τ \atop Θ; \{Δ\}; Γ ⊢ Λα. e_{i} : ∀α.τ} (α ∉ Θ ∪ Dom\{Δ\})

[∀elim] \begin{matrix}Θ; \{Δ\}; Γ ⊢ e_{i} : ∀α.τ & Δ_{i}(τ′) = τ′ \\ Θ; \{Δ\}; Γ ⊢ e_{i} [τ′] : \{τ′/α\}τ \end{matrix} (α ∉ Dom\{Δ\})

Fig. 20. Polymorphism.

in the program evaluation. We can then integrate traditional polymorphic terms by extending our notion of evaluation from e_{i} ⟼ e′_{i} to ⟨{Δ}, e_{i}⟩ ⟼ ⟨{Δ′}, e′_{i}⟩. This approach is similar to the allocation-based, explicit type-passing semantics for polymorphism found in the dissertation of Morrisett [1995].

Figure 20 contains the necessary adjustments to the language. Note that we have only one form of type variable. In keeping with convention with respect to polymorphism, we allow α and β to range over type variables in addition to t, s, and u. Types are extended with the form ∀α.τ. We add terms of the form Λα. e_{i}, in which α is abstract in e_{i}.

Instantiation of a type variable is represented by e_{i} [τ]. Operationally (see rule [∀1 ]), this application corresponds to extending δ_{i} to include α = τ. We use the notation Δ_{i} ⊎ {α = τ} to mean the mapping from types to types obtained from δ_{i}[α ↦ τ]. The notation {Δ} ⊎_{i} {α = τ} represents

{Δ_{1}, …, Δ_{i−1}, Δ_{i} ⊎ {α = τ}, Δ_{i+1}, …, Δ_{n}}.

This extension is valid only if it preserves the compatibility of the Δ maps. Letting Dom{Δ} mean ⋃_{i} Dom(δ_{i}), it is easy to show that if {Δ} is compatible and α ∉ Dom{Δ}, then {Δ} ⊎_{i} {α = τ} is compatible. As a notational convenience, whenever we use {Δ} ⊎_{i} {α = τ}, we implicitly assume that α ∉ Dom{Δ}.

We need to specify the behavior of Δ_{i} on types of the form ∀α.τ. Assuming α ∉ Dom(δ_{i}), which is always possible via alpha-conversion of ∀α.τ, we have

Δ_{i}(∀α.τ) = ∀α.Δ_{i}(τ).

The original multiagent calculus maintains the invariant that any types appearing as part of the syntax of an i-term are most concrete from agent i’s perspective. This invariant is enforced in the typing rules; for example, the [abs] rule requires that Δ_{i}(τ′) = τ′. Unfortunately, this invariant is harder to maintain now that an agent may “learn” information about a type variable at runtime. To do so, we introduce a special substitution operator, {τ/α}_{i}, to perform the substitution of τ for α only in terms colored i, including i-subterms of any j-colored subexpressions. We can

ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

extend the operator to contexts in a pointwise manner because variables in the context have a color.

We can now understand the operational behavior of the new constructs. Polymorphic expressions are values. Rule [∀1 ] performs type instantiation. Agent i’s type map is extended with the new binding for α, and we substitute τ for α in the i-colored terms of the body. Most importantly, no other agents knows α. That way, if the body of the polymorphic expression is a different color, then we will be able to use our techniques to argue that (under sufficient conditions) it evaluates independently of certain values it is passed. Rule [∀2 ] describes the transition step for an embedded polymorphic value being exported as such. In this case, the type maps do not change; the outer embedding is simply moved inside the Λ.

The static semantics are derived from the regular polymorphic lambda calculus with a few twists to account for our different style of tracking type information. First, because {Δ} changes during the course of evaluation, we must parameterize our typing judgments by the current definition of {Δ}. We also need to track the lexical scoping of Λ-bound type variables. We do so by adding a set, Θ, of type variables currently in scope. The new form of typing judgments is therefore Θ; {Δ}; Γ ⊢ e_{i} : τ.

With these additions, the static rules of the original multiagent calculus carry over to the new setting, with the understanding that occurrences of Δ_{i} in those judgments now refer to the Δ_{i} found in the {Δ} parameter to the rule. (Θ is unused by the new version of the old rules.) The typing rules for the new constructs are [∀intro] and [∀elim]. The former lets us conclude that a polymorphic term has type ∀α.τ if, when we add α to the variables in scope, the body has type τ. The side condition ensures that α is distinct from all other variables in scope and distinct from those variables that are defined in any δ map. (We can always satisfy this condition by suitable alpha conversion.) Note that this condition means Δ_{i}(α) = α for any agent i, and hence τ may mention α.

The rule [∀elim] shows how to type polymorphic instantiation. Because agent i is performing the instantiation, we require that the instantiation type is most concrete from the perspective of agent i. The last antecedent requires that such an update preserves compatibility.

One might expect that the static scoping of type variables regulated by Θ and the dynamic information encapsulated in {Δ} are closely related. The following lemma, which we need to prove preservation, establishes the relation.

Lemma 5.2. Suppose Θ, α; {Δ}; Γ ⊢ e_{j} : τ′ and α ∉ Dom{Δ}. Let {Δ′} = {Δ} ⊎_{i} {α = τ}. Then

(i) If i = j then Θ; {Δ′}; {τ/α}_{i}Γ ⊢ {τ/α}_{i}e_{j} : {τ/α}τ′ (ii) If i ≠ j then Θ; {Δ′}; {τ/α}_{i}Γ ⊢ {τ/α}_{i}e_{j} : τ′.

Proof Sketch. By simultaneous induction of parts (i) and (ii) on the derivation that Θ, α; {Δ}; Γ ⊢ e_{j} : τ′.

As usual, when we add a new type constructor to the language, we need a Type Relations Lemma to relate subcomponents of related types. In this case, we have the following:

Lemma 5.3 (∀ Type Relations). If {Δ} ⊢ ∀α.τ ≲_{ℓ} ∀α.τ′, then {Δ} ⊢ τ ≲_{ℓ} τ′.

We alter the statement of preservation to account for the difference in program configurations. As usual for an allocation-style semantics, we must show that the program does not lose type information during the course of evaluation. Thus, we make the following definition:

Definition 5.4. Let {Δ} ≤ {Δ′} mean {Δ′} = {Δ} ⊎_{i} {α = τ} for some agent i, type τ, and type variable α such that α ∉ Dom{Δ}. Let ≤^{∗} be the reflexive, transitive closure of ≤. We say that \{Δ′\} \underline{refines} \{Δ\} whenever \{Δ\} ≤^{∗} \{Δ′\}.

Lemma 5.5 (Preservation). If ∅; {Δ}; ∅ ⊢ e_{i} : τ and ⟨{Δ}, e_{i}⟩ ⟼ ⟨{Δ′}, e′_{i}⟩, then {Δ′}; ∅ ⊢ e′_{i} : τ. Furthermore, {Δ′} is compatible and refines {Δ}.

Proof. The cases for terms not involving the new constructs are similar to those cases presented earlier, so we omit them. The new cases are:

[∀1 ] By assumption, there is a derivation of the form

\begin{matrix}{α; \{Δ\}; ∅ ⊢ e_{i} : τ′′ \atop ∅; \{Δ\}; ∅ ⊢ Λα. e_{i} : ∀α.τ′′} & Δ_{i}(τ) = τ \\ ∅; \{Δ\}; ∅ ⊢ (Λα. e_{i}) [τ] : \{τ/α\}τ′′ \end{matrix} (α ∉ Dom\{Δ\}).

Let {Δ′} = {Δ}⊎_{i}{α = τ} and Δ′_{i} = Δ_{i}⊎_{i}{α = τ}. We can apply Lemma 5.2 to the antecedent to obtain ∅; {Δ′}; ∅ ⊢ {τ/α}_{i}e_{i} : {τ/α}τ′′. Clearly {Δ′} is compatible and refines {Δ} .

[∀2 ] By assumption, there is a derivation of the form

\begin{matrix}{α; \{Δ\}; ∅ ⊢ e_{j} : τ^{1} \atop ∅; \{Δ\}; ∅ ⊢ Λα. e_{j} : ∀α.τ^{1}} & \{Δ\} ⊢ ∀α.τ^{1} ≲_{jℓi} ∀α.τ \\ ∅; \{Δ\}; ∅ ⊢ ⌜⌞Λα. e_{j}⌝⌟_{jℓ}^{∀α.τ} : Δ̄_{i}(∀α.τ) \end{matrix}.

The side conditions ensure that α ∉ Dom{Δ}, so we are able to conclude that Δ̄_{i}(∀α.τ) = ∀α.Δ̄_{i}(τ). We need to construct a derivation for

\begin{matrix}α; \{Δ\}; ∅ ⊢ e_{j} : τ^{1} & \{Δ\} ⊢ τ^{1} ≲_{jℓi} τ \\ α; \{Δ\}; ∅ ⊢ ⌜⌞e_{j}⌝⌟_{jℓ}^{τ} : Δ̄_{i}(τ) \end{matrix} ; ∅; \{Δ\}; ∅ ⊢ Λα. ⌜⌞e_{j}⌝⌟_{jℓ}^{τ} : ∀α.Δ̄_{i}(τ).

We have the first antecedent from the original typing derivation. The Type Relations Lemma (5.3) says that {Δ} ⊢ ∀α.τ^{1} ≲_{jℓi} ∀α.τ implies {Δ} ⊢ τ^{1} ≲_{jℓi} τ. The side condition on [∀intro] has already been observed above. Because {Δ} is compatible and refines itself, we are done.

Because the {Δ} context changes during evaluation, and the definition of when ⌜⌞v̂_{j}⌝⌟_{jℓ}^{t} is an i-value depends on whether Δ_{i}(t) = t, the notion of value is also dynamic. We write {Δ} ⊢ e_{i} : Value when either e_{i} is an i-primval or e_{i} = ⌜⌞v̂_{j}⌝⌟_{ℓ}^{t} and t ∉ Dom{Δ}.

Progress, proved as usual by induction on the structure of e_{i}, then becomes:

Lemma 5.6 (Progress). If ∅; {Δ}; ∅ ⊢ e_{i} : τ then either {Δ} ⊢ e_{i} : Value or there exists an e′_{i} and {Δ′} such that ⟨{Δ}, e_{i}⟩ ⟼ ⟨{Δ′}, e′_{i}⟩

ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

\begin{aligned}τ & ::= & α | τ → τ | ∀α.τ \\ e & ::= & x | λx:τ. e | (e e) | Λα. e | (e [τ]) \end{aligned}

Γ ⊢ x : Γ(x)

{Γ[x:τ] ⊢ e : τ′ \atop Γ ⊢ λx:τ. e : τ → τ′} (x ∉ Dom(Γ))  \begin{matrix}Γ ⊢ e : τ′ → τ & Γ ⊢ e′ : τ′ \\ Γ ⊢ (e e′) : τ \end{matrix}
{Γ ⊢ e : τ \atop Γ ⊢ Λα. e : ∀α.τ} (α ∉ F T V (Γ))  {Γ ⊢ e : ∀α.τ′ \atop Γ ⊢ (e [τ]) : \{τ/α\}τ′}

Fig. 21. Polymorphic lambda calculus.

5.3 Translation from the Polymorphic Lambda Calculus

The net effect of our design decisions is that we can faithfully embed the polymorphic lambda calculus (shown in Figure 21) into this new language by simply decorating the term with a single color. In this case, the operational semantics degenerates to those of the regular polymorphic lambda calculus; in particular, type application still substitutes a type for a type variable. Using such a naive translation, our system will provide no more opportunity to use syntactic proofs of type abstraction than before.

Instead, we show that a smarter translation, which essentially colors the code in such a way as to make agents with different type information explicit, allows us to recover some type-abstraction proofs in a syntactic manner.

We formulate the translation as a type-directed transformation C[[Γ ⊢ e : τ]]. The translation takes two additional parameters: i, an agent indicating the desired color of the result term, and γ, a map from source variables to target variables (including color information). We maintain the invariant that, when compiling the judgment C[[Γ ⊢ e : τ]]iγ, we have Dom(γ) = Dom(Γ). The result of the translation is an i-term.

The translation is given in Figure 22. Most of the rules are straightforward—they recursively translate the subterms of the expression and combine the results into the corresponding construct. The two interesting cases are [Tvar] and [Ttypeabs].

The rule for translating the variable x simply looks up x in the map γ. If the resulting variable has the same color as the desired color of the term, no further action is needed. Otherwise, the translation produces an embedding of the variable to yield a term of the appropriate color. Because the type Γ(x) may mention type variables that are currently in scope, the embedding may be abstract.

The idea for translating a polymorphic term is to “spawn” a new agent with which to color the body of the type abstraction. By recursively translating the body to a term of this new color, [Ttypeabs] explicitly marks the boundaries where type information changes.

As examples, we have the following translations:

C[[∅ ⊢ Λα. λx:α. x : ∀α.α → α]]i∅ = Λα. ⌜⌞λx_{j}:α. x_{j}⌝⌟_{j}^{α→α}

C[[∅ ⊢ λx:b. Λα. x : b → ∀α.b]]i∅ = λx_{i}:b. Λα. ⌜⌞⌜⌞x_{i}⌝⌟b_{i}⌝⌟b_{j}

ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

[Tvar]  C[[Γ ⊢ x : Γ(x)]]iγ = \{ \begin{matrix}γ(x) & if color(γ(x)) = i \\ ⌜ ⌞γ(x)⌝ ⌟_{j}^{Γ(x)} & if color(γ(x)) = j ≠ i \end{matrix}

[Tabs]  {C[[Γ[x:τ] ⊢ e : τ′]]i(γ[x ↦ x_{i}]) = e_{i} \atop C[[Γ ⊢ λx:τ. e : τ → τ′]]iγ = λx_{i}:τ. e_{i}}

[Tapp]  \begin{matrix}C[[Γ ⊢ e : τ′ → τ]]iγ = e_{i} & C[[Γ ⊢ e′ : τ′]]iγ = e′_{i} \\ C[[Γ ⊢ (e e′) : τ]]iγ = (e_{i} e′_{i}) \end{matrix}

[Ttypeabs]  {C[[Γ ⊢ e : τ]]jγ = e_{j} \atop C[[Γ ⊢ Λα. e : ∀α.τ]]iγ = Λα. ⌜ ⌞e_{j}⌝ ⌟_{j}^{τ}} (j fresh)

[Ttypeapp]  {C[[Γ ⊢ e : ∀α.τ]]iγ = e_{i} \atop C[[Γ ⊢ (e [τ′]) : \{τ′/α\}τ]]iγ = (e_{i} [τ′])}

Fig. 22. Translation of the polymorphic lambda calculus.

The translation is type-preserving, as formalized in the following lemma, where γΓ is the pointwise application of γ to the variables in Γ.

Lemma 5.7. Suppose Γ ⊢ e : τ in the polymorphic lambda calculus and γ is a map from source variables to target variables where Dom(γ) = Dom(Γ). Suppose further that C[[Γ ⊢ e : τ]]iγ = e_{i}. Let {Δ} = {Δ_{k} | k ∈ Agents(e_{i}), δ_{k} = ∅}, and let Θ = F T V (Γ), the free type variables appearing in Γ. Then Θ; {Δ}; γΓ ⊢ e_{i} : τ.

Proof Sketch. By induction on the derivation that Γ ⊢ e : τ in the source language. The base case is handled by the definition of γ. It uses the fact that for any {Δ} and nonempty ℓ, {Δ} ⊢ τ ≲_{ℓ} τ. The same idea is used to show that the embedding introduced in the translation of a polymorphic term is well-typed. To show that a translated type application is well-formed, we need to show that α ∉ Dom{Δ} and that Δ_{i}(τ′) = τ′, but these follow from the fact that each δ_{k} is the empty map. The remainder of the cases follow by straightforward induction.

We can erase this extended multiagent calculus (excluding fix) to the polymorphic lambda calculus by extending our definition of erasure to include the new terms. Also, the definition of Φ (the composite type information) depends on the current {Δ}, so we treat {Δ}as an input to erase.

\begin{aligned}erase(\{Δ\}, Λα. ⌜⌞e_{j}⌝⌟_{jℓ}^{τ}) & = & Λα. erase(\{Δ\}, e_{j}) \\ erase(\{Δ\}, e_{i} [τ]) & = & erase(\{Δ\}, e_{i}) [Φ̄(τ)] \end{aligned}

Using the same techniques as before, we prove the following lemma:

Lemma 5.8 (Erasure). If e_{i} is well-typed and ⟨{Δ}, e_{i}⟩ ⟼^{∗} ⟨{Δ′}, e′_{i}⟩, then erase({Δ}, e_{i}) ⟼^{∗} erase({Δ′}, e′_{i}).

This lemma lets us establish a correspondence between the polymorphic lambda calculus and its translation into our multiagent setting.

Lemma 5.9 (Translation). If ∅ ⊢ e : τ in the polymorphic lambda calculus, then erase(C[[∅ ⊢ e : τ]]i∅) = e.

ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

Proof Sketch. By induction on the derivation that e is well-typed. The invariant must be strengthened to include open terms.

Putting the previous two lemmas together yields the following theorem, which establishes the correctness of our translation:

Theorem 5.10 (Correctness of Translation). Suppose ∅ ⊢ e : τ is a term of the polymorphic lambda calculus, e ⟼^{∗} v, and C[[∅ ⊢ e : τ]]i∅ = e_{i}. Furthermore, let {Δ} = {Δ_{k} | k ∈ Agents(e_{i}), δ_{k} = ∅}. Then there exists a v_{i} such that ⟨{Δ}, e_{i}⟩ ⟼^{∗} ⟨{Δ′}, v_{i}⟩ and erase({Δ′}, v_{i}) = v.

Finally, if we return to the file-handle example from the introduction, letting τ_{c} = string → fh, we see that

C[[(Λfh. λhost:τ_{c}. client code) int host code]]h∅

= (Λfh. ⌜⌞λhost_{c}:τ_{c}. client code_{c}⌝⌟_{c}^{τ_{c}→τ}) int host code_{h}.

If we assume that host code_{h} is a value, the Canonical Forms lemma tells us that it is a function, λx_{h}: string. host. Let τ_{h} be string → int, the host’s view of τ_{c}. Let {Δ} be {δ_{h} = ∅, δ_{c} = ∅} and {Δ′} be {δ_{h} = [fh ↦ int], δ_{c} = ∅}. Then the first several steps of the operational semantics are

⟨{Δ}, (Λfh. ⌜⌞λhost_{c}:τ_{c}. client code_{c}⌝⌟_{c}^{τ_{c}→τ}) int host code_{h}⟩
⟼ ⟨{Δ′}, ⌜⌞λhost_{c}:τ_{c}. client code_{c}⌝⌟_{c}^{τ_{h}→τ} host code_{h}⟩
⟼ ⟨{Δ′}, (λhost_{h}:τ_{h}. ⌜⌞{⌜⌞host_{h}⌝⌟_{h}^{τ_{c}}/host_{c}}client code_{c}⌝⌟_{c}^{τ}) host code_{h}⟩
⟼ ⟨{Δ′}, ⌜⌞{⌜⌞host code_{h}⌝⌟_{h}^{τ_{c}}/host_{c}}client code_{c}⌝⌟_{c}^{τ} ⟩.

The evaluation from this point on is via rule [3 ]. We can use the invariant φ presented for the Host-Provided Preservation Lemma: if we assume that client code is host-free, it is easy to establish that φ(client code). By rule [H ], we have φ(⌜⌞host code⌝⌟_{h}^{τ_{h}}). Thus, by Host-Provided Substitution we are able to conclude φ({⌜⌞host code_{h}⌝⌟_{h}^{τ_{a}}/host_{c}}client code_{c}). We conclude that any closed value of type fh appearing in the client code during evaluation was obtained through the host interface. (Technically, we should require that the bodies of the client and host do not themselves contain polymorphic terms, because the proof in Section 3 does not account for the new extensions to the language. We expect that this requirement is actually not necessary.)

6. RELATED WORK

There has been much work on representation independence and parametric polymorphism, as pioneered by Strachey [1967] and Reynolds [1983], and more recently by Ma and Reynolds [1992]. Such notions have been incorporated into programming languages such as SML [Milner et al. 1997] and Haskell [Peyton Jones et al. 1999] and studied extensively in Girard’s System F [1989]. The connection between type abstraction and existential types has been studied by Mitchell and Plotkin [1988].

Model-theoretic approaches to studying polymorphism have also enjoyed a rich history, although incorporating notions of recursion have proven to be difficult: see MacQueen et al. [1986], the work of Coquand et al. [1987; 1989], and Abadi and Plotkin [1990]. Pitts [1996] has studied relational properties on recursively defined

ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

domains and investigated parametricity in extensions of the polymorphic lambda calculus that include fixpoint recursion [Pitts 2000].

Wright and Felleisen [1994] popularized the use of syntactic techniques for proving type safety. We can view our work as extending theirs to prove stronger properties by adding innocuous syntax to a language. Given the right syntactic additions, the resulting proofs follow precisely the subject-reduction form that Wright and Felleisen advocate.

Abadi et al. [1993] have taken a syntactic approach to parametricity by formalizing the logical relations arguments used in such proofs. More recently, Crary [1999] has proposed the use of singleton types as a means of proving parametricity results without resorting to the construction of models.

None of the above work explicitly involves the notion of principal. Our syntactic separation of agents is similar to Nielson and Nielson’s two-level lambda calculus [Nielson and Nielson 1992]. 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 Riecke’s work on the SLam calculus [1998], Volpano and Smith’s work on typebased security [1997], and the language JFlow [Myers 1999].

Pierce and Sangiorgi [1999] prove parametricity results for a polymorphic pi calculus in an operational setting. Rather than add principals to the term language, they use external substitutions to reason about bisimilarity of polymorphic processes in which there are both abstract and concrete views of data values. Sewell and Vitek [1999] have also used the idea of coloring in a variant of the pi calculus to prove properties about causal relationships in a security setting.

Perhaps the closest work to ours is Leroy and Rouaix’s investigation into the safety properties of typed applets [Leroy and Rouaix 1998]. They use a lambda calculus augmented with state in order to prove theorems similar to our two-agent theorems. They too distinguish between 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.

7. SUMMARY AND CONCLUSIONS

Abstract types are an invaluable tool to software designers. They aid programmers in reasoning about interfaces between different pieces of code.

Despite this utility, it is very hard to prove that the informal reasoning about abstract types, such as, “all file handles are obtained from the open system call,” is correct. One approach is to encode different principals in the well-understood polymorphic lambda calculus and appeal to results on parametricity. This approach is not always feasible, such as when the language includes state, threads, recursive types, or other expressive features. The syntactic proofs of type-abstraction properties presented in this paper are tedious, but conceptually straightforward. In contrast, building a model is conceptually difficult but can yield elegant proofs.

We have presented a syntactic approach to proving some type-abstraction properties. The main idea is “color” the different principals in the language, each of which has access to different type information. We show how we can track these principals throughout evaluation. This extra syntactic structure gives us a frame-

ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

work in which we can prove properties about where certain values came from (the file-handle example), as well as how abstraction is preserved by evaluation. The arguments take the form of subject-reduction proofs, which show that a desired property is invariant with respect to evaluation, so the hope is that they will scale more easily than model-theoretic techniques. As evidence supporting this hope, we have shown how to extend these results to include mutable references, recursive types, and parametric polymorphism.

There are a number of open questions about our approach. Parametric polymorphism offers the strong notion of representation independence, which can be used to reason about the equivalence of abstract data types. As long as two implementations are equivalent in an appropriate sense, it does not matter which implementation a program uses—they produce equivalent results. We have avoided building such logical relations, but it remains to be seen exactly what formal connections can be drawn between those results and the ones presented here.

We also have not investigated the connections between the multiagent calculus and process-based calculi or object-oriented calculi where the notion of principal (that is, threads or objects) arises naturally. Our method of tracking principals during evaluation should adapt to these domains, but we may also learn more about the multiagent calculus by viewing each agent as a thread and the embedding annotations as points at which synchronization occurs during execution. There is also a similarity between our use (in Section 5.2) of global alpha conversion and the restriction operator, ν, of the pi calculus to generate a “fresh” type variable at runtime.

Another addition to our approach would be an integration of traditional subtyping. That is, we have not considered how we would need to adapt the framework to permit a primitive subtyping relation between (multiple) base types and its standard extension to other type constructors. Our multiagent calculus does allow a principal to reveal partial information about a type. (For example, by letting t_{1} = t_{2} → t_{3}, t_{2} = int, and t_{3} = int, an agent can export a function of type int → int at four different types.) Perhaps there is some connection between this sort of partial information and the partial information of knowing that τ is some subtype of τ′, but it seems our approach is closer to polymorphism than subtyping.

The kinds of properties we have proven in the multiagent language are limited by the granularity of types. The system does not let us prove that an agent does not misuse file handles, for instance by duplicating them or confusing two different file handles obtained from separate calls to open. The reason is that we track embeddings at the granularity of their types—the theorems do not distinguish particular instances of type fh. We could imagine tracking such fine-grained details, but the necessary invariants for subject-reduction proofs may become more complex.

Finally, the notion of principal could prove useful for results other than abstraction. For example, we could easily give different operational semantics to different principals and then reason about interlanguage interoperability. Lifting constants and values out of embeddings could require wrapper code or data conversions. Similarly, we could imagine that embeddings represent a form of remote communication. In this case, putting values in embeddings and taking values out would require marshalling and unmarshalling.

ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

REFERENCES

Abadi, M., Cardelli, L., and Curien, P.-L. 1993. Formal parametric polymorphism. In 20th ACM Symposium on Principles of Programming Languages. ACM Press, New York, NY, 157– 167.

Abadi, M. and Plotkin, G. D. 1990. A PER model of polymorphism. In 5th Annual Symposium

on Logic in Computer Science. IEEE Computer Society Press, Los Alamitos, CA, 355–365. Coquand, T., Gunter, C. A., and Winskel, G. 1987. DI-domains as a model of polymorphism.

In Mathematical Foundations of Programming Language Semantics, M. Main, A. Melton, M. Mislove, and D. A. Schmidt, Eds. Lecture Notes in Computer Science, vol. 298. Springer-Verlag, New York, NY, 344–363.

Coquand, T., Gunter, C. A., and Winskel, G. 1989. Domain theoretic models of polymorphism.

Inf. Comput. 81, 2 (May), 123–167. Crary, K. 1999. A simple proof technique for certain parametricity results. In 4th ACM Inter-

national Conference on Functional Programming. ACM Press, New York, NY, 82–89. Girard, J.-Y., Lafont, Y., and Taylor, P. 1989. Proofs and Types. Cambridge University

Press, Cambridge, UK. Harper, R. 1994. A simplified account of polymorphic references. Information Processing Let-

ters 51, 4 (August), 201–206. Heintze, N. and Riecke, J. G. 1998. The SLam calculus: programming with secrecy and integrity.

In 25th ACM Symposium on Principles of Programming Languages. ACM Press, New York, NY, 365–377.

Leroy, X. and Rouaix, F. 1998. Security properties of typed applets. In 25th ACM Symposium

on Principles of Programming Languages. ACM Press, New York, NY, 391–403. Ma, Q. and Reynolds, J. 1992. Types, abstraction, and parametric polymorphism: Part 2. In

Proceedings of the 1991 Mathematical Foundations of Programming Semantics, S. Brookes, M. Main, A. Melton, M. Mislove, and D. A. Schmidt, Eds. Number 598 in Lecture Notes in Computer Science. Springer-Verlag, New York, NY, 1–40.

MacQueen, D., Plotkin, G. D., and Sethi, R. 1986. An ideal model for recursive polymorphism.

Information and Control 71, 1/2 (October/November), 95–130. Milner, R., Tofte, M., Harper, R., and MacQueen, D. 1997. The Definition of Standard ML

(Revised). The MIT Press, Cambridge, MA. Mitchell, J. 1991. On the equivalence of data representations. In Artificial Intelligence and

Mathematical Theory of Computation: Papers in Honor of John McCarthy, V. Lifschitz, Ed. Academic Press, San Diego, CA, 305–330.

Mitchell, J. C. and Plotkin, G. D. 1988. Abstract types have existential type. ACM Trans-

actions on Programming Languages and Systems 10, 3 (July), 470–502. Morrisett, G. 1995. Compiling with types. Ph.D. thesis, Carnegie Mellon University. Published

as CMU Tech Report number CMU-CS-95-226. Myers, A. C. 1999. JFlow: Practical mostly-static information flow control. In 26th ACM

Symposium on Principles of Programming Languages. ACM Press, New York, NY, 228–241. Nielson, F. and Nielson, H. R. 1992. Two-Level Functional Languages. Number 34 in Cambridge

Tracts in Theoretical Computer Science. Cambridge University Press, Cambridge, UK. Peyton Jones, S., Hughes, J., Augustsson, L., Barton, D., Boutel, B., Fasel, J., Hammond,

K., Hinze, R., Hudak, P., Johnsson, T., Jones, M., Launchbury, J., Meijer, E., Peterson, J., Reid, A., Runciman, C., and Wadler, P. 1999. Haskell 98: A non-strict, purely functional language. http://www.haskell.org/onlinereport/.

Pierce, B. C. and Sangiorgi, D. 1999. Behavioral equivalence in the polymorphic pi-calculus. Tech. Rep. MS-CIS-99-10, University of Pennsylvania. Apr. (Summary in 24th ACM Symposium on Principles of Programming Languages).

Pitts, A. M. 1996. Relational properties of domains. Inf. Comput. 127, 66–90. Pitts, A. M. 2000. Parametric polymorphism and operational equivalence. Mathematical Struc-

tures in Computer Science 10, 1–39.

Reynolds, J. C. 1974. Towards a theory of type structure. In Programming Symposium. Lecture

Notes in Computer Science, vol. 19. Springer-Verlag, New York, NY, 408–425. Reynolds, J. C. 1983. Types, abstraction and parametric polymorphism. In Information Pro-

cessing 83, R. E. A. Mason, Ed. Elsevier Science Publishers B. V. (North-Holland), Amsterdam, 513–523.

Sewell, P. and Vitek, J. 1999. Secure composition of untrusted code with wrappers and causality

types. Work in Progress http://www.cs.purdue.edu/homes/jv/publist.html. Strachey, C. 1967. Fundamental concepts in programming languages. Unpublished Lecture

Notes, Summer School in Computer Programming. Volpano, D. and Smith, G. 1997. A type-based approach to program security. In TAPSOFT’97,

Theory and Practice of Software Development. Lecture Notes in Computer Science, vol. 1214. Springer-Verlag, New York, NY.

Wright, A. K. and Felleisen, M. 1994. A syntactic approach to type soundness. Inf. Com-

put. 115, 1, 38–94. Preliminary version in Rice Tech. Rep. 91-160. Zdancewic, S., Grossman, D., and Morrisett, G. 1999. Principals in programming languages: A

syntactic proof technique. In 4th ACM International Conference on Functional Programming. ACM Press, New York, NY, 197–207.

Received February 2000; revised September 2000; accepted November 2000