Principals in Programming Languages: A Syntactic Proof Technique

Steve Zdancewic Dan Grossman Greg Morrisett ^{∗}

Department of Computer Science Cornell University

Abstract

Programs are often structured around the idea that different pieces of code comprise distinct principals, each with a view of its environment. Typical examples include the modules of a large program, a host and its clients, or a collection of interactive agents.

In this paper, we formalize this notion of principal in the programming language itself. The result is a language in which intuitive statements such as, “the client must call open to obtain a file handle,” can be phrased and proven formally.

We add principals to variants of the simply-typed λcalculus and show how we can track the code corresponding to each principal throughout evaluation. This multiagent calculus yields syntactic proofs of some type abstraction properties that traditionally require semantic arguments.

1 Introduction

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

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

                                                        (* File handle implemented as int *)
                                                        abstype fh

open : string → fh read : fh → char

Figure 1: Abstract interface for file handles

Consider a host-provided interface for an abstract type of file handles, fh, and 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, while clients do not.

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

How do we prove such properties? One way of phrasing the result is to say that the agent behaves parametrically with respect to the type fh. Using this observation, we can encode the agent program in a language like Girard’s System F [5], the polymorphic λ-calculus [18] (see Figure 2). Here, the type fh is held abstract by encoding the agent as a polymorphic function. We can then appeal to Reynolds’ parametricity results [19] to conclude that the agent respects the host’s interface.

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

Figure 2: Polymorphic λ-calculus agent encoding

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

∗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.

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

To see why these new mechanisms are useful, consider the evaluation of our agent code when “linked” against a host implementation. As Figure 3 shows, linking is encoded as application. In one step of the standard operational semantics, the host-type is substituted throughout the agent code. It is impossible to talk about the type fh remaining abstract within the client because fh is replaced by int. After a second step, host code is substituted throughout agent code and all distinctions between principals are lost.

τ_{h} = {open : string → fh, read : fh → char}

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

Figure 3: “Linking” agent code

The next section describes a two-agent setting sufficient for proving interesting properties about the file handle example. It then discusses how to include more advanced language features, such as recursive types and state. Section 3 introduces a multiagent calculus which provides for multiple agents and abstract types. We then revisit the safety properties and language extensions of Section 2. The final sections conclude with related work and other potential uses for principals in programming languages.

2 The Two-agent Language

2.1 Syntax

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

\begin{aligned}τ & ::= & t | b | τ → τ′ \\ A & ::= & x_{a} | c | λx_{a}:τ. A | A A′ | ⌜ ⌞H⌝ ⌟_{h}^{τ} \\ Â & ::= & c | λx_{a}:τ. A | ⌜ ⌞Ĥ⌝ ⌟t_{h} \\ H & ::= & x_{h} | c | λx_{h}:τ. H | H H′ | ⌜ ⌞A⌝ ⌟_{a}^{τ} \\ Ĥ & ::= & c | λx_{h}:τ. H \end{aligned}

Figure 4: Two-agent Syntax

Figure 4 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 agent terms, A, agent values, Â, host terms, H, and host values, Ĥ. The metavariable x_{a} ranges over agent variables which are disjoint from host variables, ranged over by x_{h}. The metavariable c ranges over values of base type.

It is helpful to think of terms generated by A and H as having different colors (indicated by the subscripts a and h respectively) that indicate to which principal each belongs. As observed in the introduction, agent and host terms mix during evaluation. To keep track of this intermingling, agent terms contain embedded host terms of the form ⌜ ⌞H⌝ ⌟_{h}^{τ}. Intuitively, the brackets delimit a piece of h-colored code, where H is exported to the agent at type τ. Dually, host terms may contain embedded agents.

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

A good intuition for the semantics is to imagine two copies of the simply-typed λ-calculus augmented with a new type t. In the agent copy, t is abstract, while in the host copy, we have t = τ_{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}.

2.2 Notation

Before describing the semantics, we define some convenient notions. Let e range over both agent and host terms, and let ê range over both agent and host values. The color of e is a if e is an A term; otherwise e’s color is h. Note that both terms in a syntactically well-formed application are the same color. Since the host and agent terms share some semantic rules, we use polychromatic rules to range over both agent and host terms. The intention is that all terms mentioned in a polychromatic rule have the same color, and 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 α-conversion, where substituted variables are of the same color. We also define substitution on types, written {τ′/t}τ. Intuitively, we use the substitution {τ_{h}/t}τ to produce the host’s view of τ.

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

2.3 Dynamic Semantics

Figure 5 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 λ-calculus. The other rules handle embeddings.

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

Rules (A3) and (H3) maintain the distinction between agent and host code. For example, suppose the agent contains a host function that is being exported at type τ′ → τ′′.

Polychrome Steps (P1)  e e′ ⟼ e′′ e′ if e ⟼ e′′
(P2)  ê e′ ⟼ ê e′′  if e′ ⟼ e′′
(P3)  (λx:τ. e) ê ⟼ {ê/x}e
Agent Steps (A1)  ⌜ ⌞H⌝ ⌟_{h}^{τ} ⟼ ⌜ ⌞H′⌝ ⌟_{h}^{τ} if H ⟼ H′
(A2)  ⌜ ⌞c⌝ ⌟_{h}^{b} ⟼ c
(A3) ⌜ ⌞λx_{h}:τ. H⌝ ⌟_{h}^{τ′→τ′′} ⟼ λx_{a}:τ′. ⌜ ⌞{⌜ ⌞x_{a}⌝ ⌟_{a}^{τ}/x_{h}}H⌝ ⌟_{h}^{τ′′}
Host Steps (H1)  ⌜ ⌞A⌝ ⌟_{a}^{τ} ⟼ ⌜ ⌞A′⌝ ⌟_{a}^{τ} if A ⟼ A′
(H2)  ⌜ ⌞c⌝ ⌟_{a}^{b} ⟼ c
(H3) ⌜ ⌞λx_{a}:τ. A⌝ ⌟_{a}^{τ′→τ′′} ⟼ λx_{h}:{τ_{h}/t}τ′. ⌜ ⌞{⌜ ⌞x_{h}⌝ ⌟_{h}^{τ}/x_{a}}A⌝ ⌟_{a}^{τ′′}
(H4)  ⌜ ⌞⌜ ⌞Ĥ⌝ ⌟t_{h}⌝ ⌟_{a}^{τ_{h}} ⟼ Ĥ

Figure 5: Two-agent Dynamic Semantics

In this case the agent does know that the embedding contains a function, so the agent can apply it to an argument of a suitable type. If instead the function had been exported at type t, the agent would not have been able to apply it. The subtlety is that the host type of the function may be more specific than the agent type, such as when τ′ = t.

Thus, (A3) converts an embedded host function to an agent function with argument of type τ′. The body of the agent function is an embedding of the host code, except that, as the argument now comes from the agent, every occurrence of the original argument variable, x_{h}, is replaced by an embedding of the agent’s argument variable, ⌜ ⌞x_{a}⌝ ⌟_{a}^{τ}. This embedding is exported to the host at type τ, the type the host originally expected for the function argument. The rule for hosts, (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” an agent value that is really an embedded host value. This allows the host to recover a value that has been embedded abstractly in the agent.

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

2.4 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 agent functions. For host functions, the only difference is that t is not allowed to appear in the annotation for the argument to a function. Since the host knows that t = τ_{h}, this does not limit expressiveness. The convenient effect of this side condition is that types of host terms never contain t. The presence of t would complicate other rules such as (var) and (app), as well as the statement of Preservation, because additional type refinement would be necessary.

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

2.5 Examples

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

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

(λopen_{a}:string → fh. open_{a} “myfile”)

⌜ ⌞λs_{h}:string. ho(s_{h})⌝ ⌟_{h}^{string→fh}

(1) (λopen_{a}:string → fh. open_{a} “myfile′′)

λs_{a}:string. ⌜ ⌞ho(⌜ ⌞s_{a}⌝ ⌟_{a}^{string})⌝ ⌟fh_{h}

(2) ⟼ λs_{a}:string. ⌜ ⌞ho(⌜ ⌞s_{a}⌝ ⌟_{a}^{string})⌝ ⌟fh_{h} “myfile′′
(3) ⟼ ⌜ ⌞ho(⌜ ⌞“myfile′′⌝ ⌟_{a}^{string})⌝ ⌟fh_{h}
(4) ⟼ ⌜ ⌞ho(“myfile′′)⌝ ⌟fh_{h}
(n) ⟼^{∗} ⌜ ⌞3⌝ ⌟fh_{h}

Figure 6: Agent calling open

Step (1) uses (A3) to convert the embedded host function to an agent function. Note that the new variable, s_{a}, is

Polychrome Rules

(var) Γ ⊢ x : Γ(x)  (const) Γ ⊢ c : b  (app) \frac{Γ ⊢ e : τ′ → τ Γ ⊢ e′ : τ′}{Γ ⊢ e e′ : τ}

Agent Rules

(HinA) \frac{Γ ⊢ H : \{τ_{h}/t\}τ}{Γ ⊢ ⌜ ⌞H⌝ ⌟_{h}^{τ} : τ}  (Afn) \frac{Γ[x_{a} : τ′] ⊢ A : τ}{Γ ⊢ λx_{a}:τ′. A : τ′ → τ}

Host Rules

(AinH) \frac{Γ ⊢ A : τ}{Γ ⊢ ⌜ ⌞A⌝ ⌟_{a}^{τ} : \{τ_{h}/t\}τ}  (Hfn) \frac{Γ[x_{h} : τ′] ⊢ H : τ}{Γ ⊢ λx_{h}:τ′. H : τ′ → τ} (t ∉ τ′)

Figure 7: Two-agent Static Semantics

embedded in the host as an agent term. Step (2) is a standard β-reduction. Step (3) is another β-reduction, passing in the 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 (A1) allows the host function to proceed. We assume that ho returns 3 when applied to “myfile”. This result, embedded within the agent code at type fh, is an agent value.

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

(1) ⟼ λhandle_{a}:fh. ⌜ ⌞hr(⌜ ⌞handle_{a}⌝ ⌟_{a}^{int})⌝ ⌟_{h}^{char} ⌜ ⌞3⌝ ⌟fh_{h}
(2) ⟼ ⌜ ⌞hr(⌜ ⌞⌜ ⌞3⌝ ⌟fh_{h}⌝ ⌟_{a}^{int})⌝ ⌟_{h}^{char}
(3) ⟼ ⌜ ⌞hr(3)⌝ ⌟_{h}^{char}
(n) ⟼^{∗} ⌜ ⌞′A′⌝ ⌟_{h}^{char}

⟼ ′A′

Figure 8: Agent calling read

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

In step (1), the agent extracts the host function via rule (A3). The type of the argument handle_{a} is abstract in the agent, so the type annotation is changed to 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 agent, as a regular value. The application hr(3) proceeds as usual, until the host computes the character read from the file. At last, since this embedded character is exported to the agent as such, rule (A2) produces the value ′A′.

2.6 Safety Properties

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

The following lemmas establish type soundness:

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

• b, then ê = c for some c.

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

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

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 (Stuck Terms) 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 distinction between colors, erase the embeddings, and replace t with τ_{h}, we have a simply-typed λ-calculus term. Formally, Figure 9 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 ⟼^{∗} ê iff erase(e) ⟼^{∗} erase(ê).

The interesting fact is that the erasure of rule (A3) is basically λx:τ. e ⟼ λx′:τ. {x′/x}e. The two terms are αequivalent.

With soundness and erasure established, we re-examine the abstraction properties of the introduction. Since the host is always capable of providing information to the agent, we are particularly interested in evaluations where we assume the host does not do so. Toward this end, we define host-free to describe an agent term which has no host terms embedded in it.

One desirable property of the file handle interface is that the agent never breaks the type abstraction for file handles. For example, if ∅ ⊢ handle : fh, ∅ ⊢ λf:fh. A : τ, and A

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

Figure 9: Two-agent erase translation

is host-free, then (λf:fh. A) handle never steps to a context where handle is treated as an integer. This property is a corollary of type soundness.

Another property is that the agent is oblivious to the particular choice of integers used by the host to represent a given file handle. More formally:

Theorem 2.7 (Independence of Evaluation) If ⌜ ⌞Ĥ⌝ ⌟fh_{h} and ⌜ ⌞Ĥ′⌝ ⌟fh_{h} are well-typed, A is host-free, and ∅ ⊢ λf_{a}:fh. A : fh → b, then:

(λf_{a}:fh. A) ⌜ ⌞Ĥ⌝ ⌟fh_{h} ⟼^{∗} c

iff

(λf_{a}:fh. A) ⌜ ⌞Ĥ′⌝ ⌟fh_{h} ⟼^{∗} 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 A is host-free, [x_{a} : fh] ⊢ A : τ, and {⌜ ⌞Ĥ⌝ ⌟fh_{h}/x_{a}}A is not a value, then there exists a host-free term A′ such that:

• [x_{a} : fh] ⊢ A′ : τ
• {⌜ ⌞Ĥ⌝ ⌟fh_{h}/x_{a}}A ⟼ {⌜ ⌞Ĥ⌝ ⌟fh_{h}/x_{a}}A′
• {⌜ ⌞Ĥ′⌝ ⌟fh_{h}/x_{a}}A ⟼ {⌜ ⌞Ĥ′⌝ ⌟fh_{h}/x_{a}}A′

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

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

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

2.7 Extending the Language

The two-agent calculus lacks many features found in realistic programming languages, but our embedding approach scales to handle many additions.

It is straightforward to add standard type constructors such as products, records, sums, etc. The static semantics

τ ::= … | α | μα.τ
H ::= … | roll_{μα.τ} H | unroll_{μα.τ} H
Ĥ ::= … | roll_{μα.τ} Ĥ
⌜ ⌞roll_{μα.τ} Â⌝ ⌟_{a}^{μα.τ} ⟼ roll_{μα.{τ_{h}/t}τ} ⌜ ⌞Â⌝ ⌟_{a}^{{μα.τ/α}τ}

Figure 10: Adding recursive types

are standard, while the dynamic semantics, in addition to the usual rules, also include means of propagating embeddings. For example, ⌜ ⌞(Â, Â′)⌝ ⌟_{a}^{τ×τ′} ⟼ (⌜ ⌞Â⌝ ⌟_{a}^{τ}, ⌜ ⌞Â′⌝ ⌟_{a}^{τ′}).

Recursive types also pose no problems. The necessary additions and an example host dynamic step are shown in Figure 10. (The agent rule is similar.) Our type abstraction results carry through even in this setting.

Adding state is more subtle. A rigorous treatment of references appears in the companion technical report [25]. We have proven soundness, as well as stateful analogues of the abstraction theorems presented here.

The key issue is how to facilitate the sharing of heap values between the host and agent. Our approach assigns (possibly abstract) types to heap locations and records which agent last assigned to a location. An ensuing dereference by the other agent produces an embedded term. All of this extra information can be erased, so the target language of erasure is a standard language with references. An interesting technical issue is that it is unsound for the host to export a t ref value at type τ_{h} ref. Therefore, the definition of type substitution is modified so as not to perform substitution under the ref constructor.

Restating the type abstraction properties to account for the heap is somewhat trickier, since we must preclude the possibility that the host leaks information to the agent through a shared reference. Essentially, the notion of host-free must be extended to account for terms reachable through references.

With references and recursive types, we expect that our results could be extended to handle threads in the style of those in Reppy’s doctoral thesis [17]. Such scalability is due to the similarity of our proofs to standard subject-reduction, as popularized by Wright and Felleisen [24]. Namely, a property of interest is shown to be invariant during evaluation. Although these syntactic techniques yield weaker results than semantic accounts of parametricity, they are useful in practice because we do not have to build a model containing recursive types, references, and threads.

3 The Multiagent Language

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

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

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

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

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

Figure 11: Multiagent Syntax

Generalizing the language has another benefit: we can prove theorems once for a broad class of systems. The type abstraction properties for an instance of the system (such as our two-agent calculus) follow as corollaries.

3.1 Syntax

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

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

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

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

The goal is a language in which each agent has limited knowledge of type information. Thus, we must somehow represent what an agent “knows” and ensure that agents sharing information do so consistently. For example, agent i might know that fh = int. Agent j may or may not have this piece of information, but if j does know the realization of fh, that knowledge must be compatible with what i knows. (It shouldn’t be the case that j thinks fh = string.)

To capture this information, we assume that for each agent i there is a finite partial map from type variables to types called δ_{i}. Each δ_{i} extends naturally to a map, Δ_{i}, from an arbitrary type τ as follows:

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

To maintain consistency between agents, we require that for every pair of agents, i and j, if t ∈ Dom(δ_{i}) ∩ Dom(δ_{j}), then δ_{i}(t) = δ_{j}(t).^{1} We further restrict the δ_{i} maps so that they interact in a well-founded manner. For example, we do not allow δ_{i}(t) = t → t, or the more subtle δ_{i}(t) = s → s, δ_{j}(s) = t. In general, we assume the collection of type variables can be globally ordered such that for all i and t, all variables in δ_{i}(t) precede t.

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

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

3.2 Dynamic Semantics

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

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

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

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

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

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

The most interesting rule is (9), which is really what tracks the principals. The embedded function is lifted to the outside. Its argument now belongs to the outer agent, i, instead of the inside agent, j. As such, it must be given the type that i thinks the argument should have. The body of the function is still a j-term embedded in an i-term so any occurrence of the new formal argument x_{i} must be embedded as an i-term inside a j-term. The corresponding type annotation must be the type which j expects the argu-

1We can encode multiple interfaces to an abstract datatype while satisfying consistency by introducing extra type variables (see the companion technical report).

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

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

Figure 12: Multiagent Dynamic Semantics

(λy:int → int. y 3)⌜ ⌞λx:fh → fh. x⌝ ⌟_{a}^{fh→fh}

(7) ⟼^{h} (λy:int → int. y 3)⌜ ⌞λx:fh → fh. x⌝ ⌟_{a}^{int→int}
(9) ⟼^{h} (λy:int → int. y 3)(λx′:int. ⌜ ⌞⌜ ⌞x′⌝ ⌟fh_{h:a}⌝ ⌟_{a}^{int})
(5) ⟼^{h} (λx′:int. ⌜ ⌞⌜ ⌞x′⌝ ⌟fh_{h:a}⌝ ⌟_{a}^{int})3
(5) ⟼^{h} ⌜ ⌞⌜ ⌞3⌝ ⌟fh_{h:a}⌝ ⌟_{a}^{int}
(8) ⟼^{h} ⌜ ⌞3⌝ ⌟_{h:a:a}^{int}
(6) ⟼^{h} 3

Figure 13: Multiagent Evaluation Example

ment to have. Hence the function body is still abstract to i and when the function is applied, the actual argument will be held abstract from j. The only remaining issue is the agent list on the formal argument embeddings. Since the “inside type” and “outside type” have reversed roles, the agent-list must be in reverse order. Intuitively, the agents which successively provided the function argument type to i must undo their work in the body of the function which is a j-term.

3.3 Example

As an example, we encode our two-agent calculus by letting δ_{h} map fh to int and letting δ_{a} be undefined everywhere. An evaluation which uses all of the novel rules appears in Figure 13. The numbers in the figure are the reduction rules used to take the step. Notice 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.4 Static Semantics

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

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

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

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

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

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

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

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

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

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

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

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

Figure 14: Multiagent Static Semantics

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

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

Figure 15: Type relations: {Δ} ⊢ τ ≲_{ℓ_{i}} τ′

we were to use sets of agents, instead of (ordered) lists, the reasonable typing rules become too permissive.

3.5 Safety Properties

This section illustrates some of the standard safety theorems of typed programming languages and then discusses abstraction properties that generalize those presented earlier. Rigorous proofs appear in the companion technical report [25].

We begin with type soundness:

Lemma 3.1 (Preservation)

If {Δ}; ∅ ⊢_{i} e_{i} : τ and e_{i} ⟼^{i} e′_{i} then {Δ}; ∅ ⊢_{i} e′_{i} : τ.

The interesting rules in proving preservation are (7) through (9) since they rely crucially on the ≲ relations. In the Appendix, we state the relevant lemmas and present these cases of the proof.

Lemma 3.2 (Progress) If e_{i} is well-typed then either e_{i} is a value or there exists an e′_{i} such that e_{i} ⟼^{i} e′_{i}.

The important point is that rules (6) through (9) guarantee that ⌜ ⌞v_{j}⌝ ⌟_{ℓ_{j}}^{τ} is not stuck unless it is a value.

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

The cost of including embeddings is the addition of several dynamic rules. Worse yet, with recursion and multiple

erase(x_{i}) = x
erase(c) = c
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}⌝ ⌟_{ℓ_{j}}^{τ}) = erase(e_{j})
where Φ = ⋃_{i} Δ_{i}

Figure 16: Multiagent erase translation

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 use the combined type information of all of the agents. The multiagent definition of erase is given in Figure 16, where Φ is the map obtained by taking the union of the compatible Δ_{i} maps. Informally, Φ̄(τ) is the most concrete type for τ that can be found using all n agents’ knowledge.

The target language is the simply-typed λ-calculus augmented with fix. We have the following lemma:

Lemma 3.4 (Erasure) If e_{i} is well-typed then either

e_{i} ⟼^{i}^{∗} v_{i} and erase(e_{i}) ⟼^{∗} erase(v_{i}), or e_{i} and

erase(e_{i}) both diverge.

Proof (sketch): By induction on the source derivation. Strengthen the inductive hypothesis to show that for every step of the source language, the erased version takes either zero steps (rules (6) through (9)) or one step (rules (4) and (5)). For divergence, show the contrapositive: any term erasing to a non-diverging term is non-diverging. □

We use arguments in the style of subject-reduction to prove safety properties that generalize those of the two-agent case.

Definition 3.5 (Agents(e_{i})) Let \underline{Agents(e_{i})} be i and the set of agent subscripts appearing in e_{i}.

Definition 3.6 (j-free) Let e_{i} be \underline{j-free} if j ∉ Agents(e_{i}).

Definition 3.7 (Oblivious to t) A set of agents, S, is \underline{oblivious} to type t if for all i ∈ S, t ∉ Dom(Δ_{i}) and for all t’ ≠ t, Δ_{i}(t’) ≠ t.

Theorem 3.8 (Independence of Evaluation) Let v̂_{j} and v̂′_{j} have type Δ̄_{j}(t). If {Δ}; ∅ ⊢_{i} λx_{i}:t. e_{i} : t → b and Agents(e_{i}) are oblivious to t then: (λx_{i}:t. e_{i}) ⌜ ⌞v̂_{j}⌝ ⌟t_{j} ⟼^{∗} c

iff (λx_{i}:t. e_{i}) ⌜ ⌞v̂′_{j}⌝ ⌟t_{j} ⟼^{∗} c.

The proof strengthens the claim to a step-by-step evaluation correspondence when using v̂_{j} and v̂′_{j}:

Lemma 3.9 (Value Abstraction) Let v̂_{j} and v̂′_{j} have type Δ̄_{j}(t). Let φ(e_{i}) mean Agents(e_{i}) are oblivious to t, e_{i} is j-free, and {Δ}; [x_{i} : t] ⊢_{i} e_{i} : τ for some τ. Then if φ(e_{i}) and {⌜ ⌞v̂_{j}⌝ ⌟t_{j}/e_{i}} is not an i-value, then there exists a term e′_{i} such that:

• {⌜ ⌞v̂_{j}⌝ ⌟t_{j}/x_{i}}e_{i} ⟼^{i} {⌜ ⌞v̂_{j}⌝ ⌟t_{j}/x_{i}}e′_{i}

• {⌜ ⌞v̂′_{j}⌝ ⌟t_{j}/x_{i}}e_{i} ⟼^{i} {⌜ ⌞v̂′_{j}⌝ ⌟t_{j}/x_{i}}e′_{i}

• φ(e′_{i})

Proof (sketch): We show that each rule of the operational semantics preserves property φ. □

The generalization of Theorem 2.9 is the following theorem, in which f_{h} plays the rôle of ho. It effectively says that a client containing a value of abstract type t must have obtained that value via a host-provided function.

Theorem 3.10 (Host-Provided Values) Let h be an agent such that Δ̄_{h}(t) = τ_{h}. Suppose {Δ}; ∅ ⊢_{h} f_{h} : b → τ_{h}. Let e_{i} be a term such that Agents(e_{i}) are oblivious to t and {Δ}; ∅ ⊢_{i} λp_{i}:b → t. e_{i} : τ. Further suppose (λp_{i}:b → t. e_{i}) ⌜ ⌞f_{h}⌝ ⌟_{h}^{b→t} ⟼^{i}^{∗} e′_{i}. If v is any value of type t which is a subterm of e′_{i}, then v = ⌜ ⌞v̂_{h}⌝ ⌟t_{ℓ_{h}} where

f_{h} v̂′_{h} ⟼^{h}^{∗} v̂_{h}.

3.6 Language Extensions

The multiagent language can easily be extended to include new constructs. Products, records, and sums are straightforward to add. To prove the soundness of the rules which propagate embeddings, we need a type relations lemma of the form {Δ} ⊢ τ^{0} ⊗ τ^{1} ≲_{ℓ_{i}} τ^{2} ⊗ τ^{3} if and only if {Δ} ⊢ τ^{0} ≲_{ℓ_{i}} τ^{2} and {Δ} ⊢ τ^{1} ≲_{ℓ_{i}} τ^{3}. Recursive types need a similar lemma that relates a μ-type with its unrolling.

Adding state to the multiagent calculus follows analogously to its addition in the two-agent case. In fact, the symmetry of the multiagent calculus significantly reduces the proliferation of dynamic rules. As noted in Section 2, type soundness does not hold if a reference can be exported at different levels of abstraction. In the multiagent setting, we can succinctly enforce this by extending the definition of Δ_{i} such that Δ_{i}(τ ref) = τ ref.

4 Future Work

4.1 Polymorphism and Existential Types

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

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

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

The typing rule for existential types is similar to that of our embeddings, which is not surprising given that both embeddings and existentials attempt to capture different “views” of a value. Indeed there is a strong connection between abstract types and existentials [12] which may indicate that they are a more natural extension to our language than polymorphic types.

4.2 Beyond Type Abstraction

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

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

Rule (9) essentially keeps track dynamically of which principals are executing in which stack frame. By adding primitives to the language to examine the lists of agents on embeddings, we gain a form of stack inspection, which has been studied in the context of Java security [22, 23]. We intend to investigate the kinds of security properties that can be expressed in such a language.

5 Related Work

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

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

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

Pierce and Sangiori [16] 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.

None of the above work (except Leroy and Rouaix’s) explicitly involves the notion of principal. Our syntactic separation of agents is similar to Nielson and Nielson’s Two-Level λ-calculus [14]. 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 [8] or Volpano and Smith’s work on type-based security [21]. A more syntactic approach to security is taken by Myers [13].

6 Conclusion

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

7 Acknowledgments

We thank David Walker, Stephanie Weirich, and the anonymous referees for their helpful comments on earlier drafts of this paper.

References

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

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

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

[4] Karl Crary. A simple proof technique for certain parametricity results. In Proceedings of the 4th ACM SIGPLAN International Conference on Functional Programming, Paris, France, September 1999. This volume.

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

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

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

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

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

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

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

[12] John C. Mitchell and Gordon D. Plotkin. Abstract types have existential type. ACM Transactions on Programming Languages and Systems, 10(3):470–502, July 1988.

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

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

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

[16] Benjamin C. Pierce and Davide Sangiorgi. Behavioral equivalence in the polymorphic pi-calculus. Technical Report MS-CIS-99-10, University of Pennsylvania, April 1999.

[17] John Hamilton Reppy. Higher-order Concurrency. PhD thesis, Cornell University, Ithaca, NY, June 1992. TR 92-1852.

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

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

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

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

[22] Dan S. Wallach and Edward W. Felten. Understanding Java stack inspection. In Proceedings of 1998 IEEE Symposium on Security and Privacy, Oakland, CA, May 1998.

[23] Dan Seth Wallach. A New Approach to Mobile Code Security. PhD thesis, Princeton University, 1999.

[24] Andrew K. Wright and Mattias Felleisen. A syntactic approach to type soundness. Information and Computation, 115(1):38–94, 1994. Preliminary version in Rice TR 91-160.

[25] Steve Zdancewic and Dan Grossman. Syntax and semantics for multiple agents and abstract types. Technical Report 99-1752, Cornell University, March 1999.

A Appendix

We present the most interesting parts of the proof of the Preservation Lemma for the multiagent calculus. We will use the following lemmas; the proofs are in the companion technical report [25].

Lemma A.1 (Idempotency) For all agents i, and (possibly empty) lists ℓ and ℓ′, {Δ} ⊢ τ ≲_{ℓ:i:i:ℓ′} τ′ iff {Δ} ⊢ τ ≲_{ℓ:i:ℓ′} τ′

Lemma A.2 (Reversal) If {Δ} ⊢ τ^{0} ≲_{ℓ_{i}} τ^{1} then {Δ} ⊢ τ^{1} ≲_{rev(ℓ_{i})} τ^{0}

Lemma A.3 (Arrow Type) If {Δ} ⊢ τ^{0} → τ^{1} ≲_{ℓ_{i}} τ^{2} → τ^{3} then {Δ} ⊢ τ^{0} ≲_{ℓ_{i}} τ^{2} and {Δ} ⊢ τ^{1} ≲_{ℓ_{i}} τ^{3}.

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

We recall the statement of Preservation: If {Δ}; ∅ ⊢_{i} e_{i} : τ and e_{i} ⟼^{i} e′_{i} then {Δ}; ∅ ⊢_{i} e′_{i} : τ. The proof is by induction on the derivation that e_{i} ⟼^{i} e′_{i} and is by cases on the last rule in the derivation. For formatting reasons, we omit the {Δ} antecedents throughout. Similarly, an omitted environment should be interpreted as ∅. Here are the cases for the rules peculiar to our calculus:

(6) Trivial.

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

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

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

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

The conclusion is the desired result.

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

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

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

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

The conclusion is the desired result.

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

\frac{[x_{j} : τ^{0}] ⊢_{j} e_{j} : τ^{3} Δ_{j}(τ^{0}) = τ^{0}}{⊢_{j} λx_{j}:τ^{0}. e_{j} : τ^{0} → τ^{3}}

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

Furthermore, Δ_{i}(τ^{1} → τ^{2}) = τ^{1} → τ^{2}, so we know from the definition of Δ_{i} that Δ̄_{i}(τ^{1}) = Δ_{i}(τ^{1}) = τ^{1} and similarly for τ^{2}. From the Arrow Type Lemma and the right hand premise of the bottom step, we conclude that ⊢ τ^{0} ≲_{ℓ_{j}:i} τ^{1} and ⊢ τ^{3} ≲_{ℓ_{j}:i} τ^{2}. Now notice that the reverse of ℓ_{j}: i is i : rev(ℓ_{j}) which we shall write ℓ′: j. So by the Reversal Lemma, ⊢ τ^{1} ≲_{ℓ′:j} τ^{0}. Thus we can derive:

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

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

\frac{[x_{i} : τ^{1}] ⊢_{j} \{⌜ ⌞x_{i}⌝ ⌟_{ℓ′}^{τ^{0}}/x_{j}\}e_{j} : τ_{3} ⊢ τ^{3} ≲_{ℓ_{j}:i} τ^{2}}{[x_{i} : τ^{1}] ⊢_{i} ⌜ ⌞\{⌜ ⌞x_{i}⌝ ⌟_{ℓ′}^{τ^{0}}/x_{j}\}e_{j}⌝ ⌟_{ℓ_{j}}^{τ^{2}} : Δ̄_{i}(τ^{2})}

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

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