{'fraction_non_alphanumeric': 0.03553690431283792, 'fraction_numerical': 0.010200553250345782, 'mean_word_length': 4.352485908976193, 'pattern_counts': {'":': 1, '<': 1, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 18, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Pirouette: Higher-Order Typed Functional Choreographies

We present Pirouette, a language for typed higher-order functional choreographic programming. Pirouette offers programmers the ability to write a centralized functional program and compile it via endpoint projection into programs for each node in a distributed system. Moreover, Pirouette is defined generically over a (local) language of messages, and lifts guarantees about the message type system to its own. Message type soundness also guarantees deadlock freedom. All of our results are verified in Coq.


INTRODUCTION
Higher-order typed functional programming has proven to be a powerful technique for writing single-machine programs. It allows for strong guarantees through types along with code reuse through higher-order programming. However, currently, writing distributed programs using functional programming requires writing separate code for each node in the distributed system, then using send and receive expressions to transmit data between nodes. This makes it easy to write code that deadlocks, or gets stuck because patterns of sends and receives do not match.
Session types [Carbone et al. 2007; Dardha et al. 2012;DeYoung et al. 2012;Scalas and Yoshida 2019;Wadler 2012] offer one solution. Session types describe the pattern of sends and receives in a program, allowing a compiler to catch the possibility of deadlock. However, session types are complicated to work with, and the programmer is still left trying to match up send and receive patterns by hand.
Choreographic programming [Cruz-Filipe and Montesi 2017a,b;Dalla Preda et al. 2015;Lanese et al. 2013;Montesi 2013Montesi , 2020 offers another solution. This is a programming paradigm that writes the distributed program as a single program, ensuring that sends and receives match by combining send and receive into one construct. Choreographic languages guarantee deadlock freedom by design, so the programmer gets strong guarantees on the communication patterns in their program. Until now, however, choreographic programming forced the user into a lowerorder, imperative, and un(i)typed universe. This paper presents Pirouette, the first language for choreographic programming which is also higher-order, functional, and typed.
Consider a standard example: the bookseller protocol. In this protocol, a buyer is looking to buy a book, so they send the book's title to a bookseller. The bookseller returns its price, and the buyer checks if that price is within their budget. If they can afford the book, they inform the bookseller who tells them a delivery date for their book; otherwise, they tell the seller they will not buy the book. After this, the protocol ends.
To write this program with session types, we first create a type describing the interactions from both points of view. That is, we create a type for the buyer that includes "send the title to the seller, and then receive back a price" along with a (dual) type for the seller that includes "receive the title from the buyer, then send them the price. " First, we must ensure that the two types match: when the buyer sends to the seller, the seller receives from the buyer. These types do not describe details like "if the book is within budget, tell the seller yes. " Instead, it says "either send the seller 'yes' and receive a delivery date, or send them 'no' and end the protocol". We then write a program for the buyer and another for the seller, which contain all the nasty details, and a type-checker ensures that these programs have the correct communication patterns.
In contrast, a choreographic programmer would write a single program, and expect the language and compiler to ensure that the resulting programs for the buyer and bookseller are deadlock free. For instance, such a programmer might write the following: In order to use session types to describe this communication pattern, we must use multiparty session types, a major increase in complexity [Carbone et al. 2007;Scalas and Yoshida 2019]. However, choreographies handle this without difficulty.
The choreographies explained so far can be expressed in prior work. This paper introduces functional choreographies. To understand the need for these, notice how we can abstract out a pattern from our two protocols. A buyer (say Buyer) sends a book title to Seller, who looks up its price. There is then some process, possibly involving communications, which results in a decision by Buyer, who then informs Seller of that decision. If Buyer decides to buy the book, they get back a delivery date, otherwise they get nothing. We can modify the choreography so that the decision is its own function as follows: fun Moreover, we can give a type which enforces that it takes a price located on Seller to a Boolean value on Buyer, as desired. We write this type price@Seller → Buyer.bool. Then we can give Bookseller the type (price@Seller → Buyer.bool) → Buyer.date, indicating that it is a higher-order function which expects an input that abstracts the decision in the bookseller example. This illustrates the programming convenience gained by combining higher-order functional programming with the choreographic-programming paradigm. For instance, previous works on choreographies could not treat choreographic functions as data, preventing this form of abstraction [Cruz-Filipe and Montesi 2017b].
Contributions. As stated before, Pirouette is the first (higher-order) choreographic functional programming language. Pirouette features simple located types of the form Buyer.bool and familiar type constructs like function spaces. Following the choreography philosophy, Pirouette guarantees deadlock freedom by design, without the use of complicated session types. Previously, higherorder choreographic programming was only supported through the informal development in Choral [Giallorenzo et al. 2020], which is useful despite offering no guarantees. In the following, we point out some salient technical contributions of our design.
First, Pirouette is generic in the language of messages. Note that, sometimes, locations send non-atomic messages like /2, which can be arbitrary expressions. In previous work, messages were either from a particular (and very simple) language [Cruz-Filipe and Montesi 2017a] or were assumed to compute to a value in finite time [Carbone and Montesi 2013]. Pirouette is defined generically on top of any message language (which we refer to as the local language), with very few syntactic constraints. We further show that a sound type system for the expression language can be lifted to the level of choreographies.
Two key features of choreographies are out-of-order execution and endpoint projection. We can think of a choreography as an arbitrary interleaving of communication between programs running at different locations. However, programs with the same communication pattern can have other interleavings as well. Choreographies, despite syntactically being one arbitrary interleaving are able to semantically represent all interleavings by allowing out-of-order execution. We follow previous work by defining an equivalence relation ≡ on choreographies to reason about out-oforder execution. However, unlike previous work, we are able to show that defining our operational semantics by appealing to ≡ gives a weaker-than-desired semantics. Pirouette's semantics provides a stronger form of out-of-order execution via a novel combination of a labeled-transition system and a block set, which guarantees that out-of-order execution does not violate causality.
Endpoint projection formalizes the intuition of a choreography as representing a collection of programs running at different locations by extracting a program for each location (later, we use the term control program for the projected program at each location). This justifies choreographies as a way of writing distributed programs, and allows us to state and prove that Pirouette programs are deadlock free. We follow a new design principle for choreographies: equivalence begets equality. That is, equivalent choreographies always project to exactly the same program for each location. In previous work, equivalence was used more liberally which prevented such a clean theorem. For instance, Cruz-Filipe and Montesi [2017a] use equivalence to reason about recursion unfolding, so equivalent programs may project to programs where unfolding has and has not been applied.
Moreover, somewhat surprisingly, we show that deadlock freedom is a corollary to the soundness of our type system as well as the soundness and completeness of endpoint projection. Previous work was able to take advantage of the assumption that messages always produce a value along with the lower-order nature of their choreographies. Because our choreographies are higher-order and our messages are not assumed to compute, we have to appeal to the soundness of our type system to ensure that our choreographies are always able to take a step.
We have formalized our entire development in Coq and mechanically verified proofs of all of our theorems. As mentioned by Cruz-Filipe et al. [2019], there have been several instances of flaws found in proofs of major theorems in concurrency theory in recent years. Therefore, in order to show that Pirouette's guarantees about deadlock freedom are trustworthy, we formalize our arguments. In soon-to-be-published work, a small choreography language has been formalized along with its endpoint-projection operation [Cruz-Filipe et al. 2021b,c]. However, Pirouette is a much more substantial language than was formalized in that work.
To summarize, we make the following contributions: • We introduce Pirouette, the first functional choreography language. We present its operational semantics and a (simple) type system. The operational semantics allow for out-of-order execution, mimicking the execution of a distributed program. These semantics are based on a novel idea of blocking sets -locations that are blocked on other operations and cannot reduce (Section 3). • We describe a general set of constraints on the local (message) language, allowing almost any expression-based language to be used as the local language (Section 2). Type soundness for functional choreographies lifts from type soundness for the local language (Section 3.2). • We study equivalence for functional choreographies, which allows for reasoning about out-oforder execution. We show that defining out-of-order execution based on this equivalence leads to a weaker-than-desired operational semantics when local reduction is allowed (Section 4). • We show how endpoint projection extracts programs with explicit send and receive constructs from functional choreographies. This translation is sound and complete. Moreover, we show that well-typed, projected systems are deadlock free by design, and that this deadlock freedom follows from the soundness of the type system and the soundness and completeness of endpoint projection (Section 5). • All our metatheory has been formalized in Coq and all our theorems have been mechanically verified. We discuss the particularities of our Coq implementation in Section 6.
Concurrent, independent work [Cruz-Filipe et al. 2021a] also explores higher-order functional choreographies. However, they have a very different design philosophy, which leads to a very different technical setup. For more comparison, see the discussion of related work in Section 7.

SYSTEM MODEL
We begin by discussing the assumptions we make about the system that Pirouette programs run on. We have made these assumptions as lightweight as possible. In particular, we assume that the system consists of a collection of nodes, each of which can run local programs and which can send and receive messages from other nodes. We also allow local programs to be typed, so that we can lift the type system to the choreography level.

Locations
We assume a set L of locations, which we write as ℓ, ℓ 1 , ℓ 2 , and so on. These names are treated atomically, so we do not assume any additional operations on locations. However, we do assume that location equality is decidable, so we can distinguish different locations.
Intuitively, locations refer to nodes in a distributed system. However, it's worth noting that there is nothing that prevents a node from being a thread, or a process, or any other entity that can run Turing-complete programs and send and receive messages.

Communication
We assume that every location can communicate with every other location synchronously. That is, if ℓ 1 sends a message to ℓ 2 , then ℓ 1 does not continue until ℓ 2 has received the message, and then ℓ 1 may continue. Message sending is instantaneous and certain: messages do not get "lost in the air. " Nodes should be able to send and receive two kinds of messages: values of local programs (described below) and two special synchronization messages, written L and R. These will be used in the choreography language to ensure that different locations stay in lock-step with each other.
We also require that each node be able to run a functional control program which can send and receive messages, while also running programs in the local language. We describe the precise requirements in Section 5.1, when we have the necessary background.

Local Programs
We assume that every node runs programs in a local expression-based language. Our design treats this language generically, requiring only that it allows certain operations and equations.
Our first requirement is that expressions include variables. We model messages as values, and receipt as binding a value to a variable. We implement variable binding via substitution, which we write 1 [ ↦ → 2 ]. Substitution must satisfy three standard equations: We require a function ( ) which returns the set of free variables in . We require that if ∉ FV( 1 ), then 1 [ ↦ → 2 ] = 1 .
We only send values as messages, so we assume a predicate Value( ) which determines whether is a value. We require two special values, true and false, which we use for branching in choreographies. We additionally require that all values are closed, in order to allow them to be sent. To see why, imagine that we send some open expression from ℓ 1 to ℓ 2 . Since is open, contains some free variable , which refers to some data on ℓ 1 . However, when we send to ℓ 2 , this information is lost and might be captured by a binder in ℓ 2 's program.
Finally, we require that an operational semantics be defined relationally for local expressions. We write 1 ⇒ e 2 to denote that 1 steps to 2 in the operational semantics. The only requirement on this semantics is that values do not take steps: if Value( ), then ̸ ⇒ e for any .

Examples.
Simply-typed functional languages easily satisfy the requirements above. However, any expression-based language can be used, not only ones which define functions. We discuss two examples here.
Example 1 (Call-by-Value -Calculus). The call-by-value -calculus, extended with recursive functions, Boolean values and if-then-else expression, almost fits our requirements. However, we must restrict values to be closed.
Example 2 (A Natural-Number Language). We provide a language with the following syntax: Intuitively, 0 stands for 0 as a natural number, is the successor operation on natural numbers, and true and false stand for Boolean truth and falsity, respectively. Since there are no binders, substitution is easy to define. Any closed term is a value. This is similar to the language of messages in Cruz-Filipe and Montesi [2017a], but modified to fit our requirements. In particular, we (a) allow more than one variable, which is treated via substitution instead of as a reference to state, and (b) add the true and false terms.
We include this language to demonstrate that our requirements do not force the choice ofcalculus as an expression language. Indeed, we will see later that we can equip this language with a type system which results in a sound choreographic type system.

Typed Local Programs
The guarantees we provide for Pirouette depend on the guarantees provided by the local language's type system. If we do not consider the local type system, then we are able to provide a sound and complete translation to a language with explicit send and receive constructs. If the local type system guarantees preservation, but not progress (as in a unityped system), then we are also able to prove preservation of the choreographic type system. Finally, soundness of the local type system implies not only type soundness for Pirouette, but also deadlock freedom.
We allow the types for the local language to be any language of simple types. We require that true and false have the same type, which we refer to as bool. Note, however, that this type may not be called bool, as we will see in Example 5.
We assume that the type system can be presented in terms of a judgment Γ ⊢ : , where Γ is a sequence of variable-type pairs written : . We additionally require that typing be unique: if Γ ⊢ : 1 and Γ ⊢ : 2 , then 1 = 2 . We only use this requirement to show that types play well with equational reasoning (Theorem 3). While this requirement is unusual, we note that it is usually satisfied by simple-type systems. We conjecture that this requirement could be removed with a small change to our choreographic language; we return to this point in Section 4.
The other requirements can all be framed as admissible rules; those rules can be found in Figure 1. Since these rules should be admissible, we do not require that these are actual rules in the type system; merely that we can use them to build typing proofs. This will be important when building typing proofs for choreographies on top of typing proofs for the local language. First, we require that variables be typed according to the context, and that true and false be typed in the bool type. We also require that the standard structural rules of Exchange and Weakening be allowed. The Strengthening rule is unusually-presented, but is common in most type systems: non-free variables can be safely removed from the typing context. Finally, we require the standard property of Substitution: substituting a well-typed variable into a well-typed expression yields a well-typed expression.
Sound Type Systems. We say that a local type system is sound if it additionally satisfies the following three requirements: • (Boolean Invertibility) The type bool is invertible for values: if is a value and ⊢ : bool then either = true or = false. • (Preservation) If 1 ⇒ e 2 and Γ ⊢ 1 : , then Γ ⊢ 2 : . • (Progress) If 1 is closed and ⊢ 1 : , then either 1 is a value or there is an 2 such that 1 ⇒ e 2 . 2.4.1 Examples. Each of the languages that served as examples above can be given type systems that satisfy the requirements above. In fact, we can give the -calculus two type systems, though one is not sound.
Example 3 (Simply-Typed -Calculus). This is the paradigmatic example of a typed local language. None of the rules in Figure 1 are difficult; most of the proofs are completely standard. Moreover, it is sound: the progress and preservation proofs are standard, and the invertability proof is easy.
Example 4 (Typed Natural-Numbers). We use two types: int and bool. Then, we have the following rules: : ∈ Γ Γ ⊢ : This makes the rules in Figure 1 easy to prove, and soundness is trivial.
Example 5 (Unityped -Calculus). Using the idea of "untyped is unityped", we develop a type system for -calculus with only one type, * , and only one typing rule:

Fig. 2. Functional Choreographies Syntax
Here, we satisfy the requirement to have a type for Boolean values by setting bool = * . The rules in Figure 1 are trivial, as is Preservation. However, this system is not sound: bool is not invertible, and uni-typed -calculus does not satisfy progress (programs may get stuck).

FUNCTIONAL CHOREOGRAPHIES
We introduce Pirouette, our language for writing distributed programs in a functional, choreographic style. We guarantee deadlock freedom along with the standard static guarantees of simple-type systems. Moreover, we allow higher-order computations by allowing choreographies to be passed to other choreographies as inputs.
The syntax of Pirouette can be found in Figure 2. Note that choreographies contain two types of variables: choreography variables, which stand for the result of a distributed computation (i.e., a choreography), and local variables which are the variables of the local language seen in Section 2. We write choreography variables in upper case ( , , etc.) and choreography variables in lower case ( , , etc.).
Every location has its own namespace of local variables, so ℓ 1 . ≠ ℓ 2 . . This is reflected in the defintion of substitution: substitution of choreography variables has the standard form 1 [ ↦ → 2 ], while substitution of local variables has the form [ℓ| ↦ → ]. The first notion of substitution is standard. The second walks through a term looking for a subterm of the form ℓ. ′ , and then replaces ′ with ′ [ ↦ → ]. (Note that the location name ℓ must be the same as the one in the substitution!) We write ℓ. to represent the choreography that returns the result of running on ℓ. To use this value in a future choreography, we use the syntax let ℓ. 1 in 2 . This runs 1 until it returns a value on ℓ, and then binds that value to under ℓ in 2 .
We write ℓ 1 . ⇝ ℓ 2 . ; to represent ℓ 1 evaluating and then sending the resulting value to ℓ 2 . The variable ℓ 2 . is bound to in the continuation choreography , representing ℓ 2 's receipt of the message.
The distributed program can branch based on the result of a test on a local machine. We write this if ℓ. then 1 else 2 . However, this can quickly break causality. To see why, consider the program if ℓ 1 . then ℓ 2 .3 else ℓ 2 .4. In this program, ℓ 2 behaves differently depending on the behavior of a test performed on ℓ 1 , but ℓ 2 has never been told about the result of that test! In order to fix this problem, we require that ℓ 1 inform ℓ 2 of which branch was taken before ℓ 2 can behave differently in the two branches. We do this using the syntax ℓ 1 [ ] ⇝ ℓ 2 ; . Here can either be L or R, where L represents taking the then branch, while R represents taking the else branch. Thus, we can safely write the following program: Note that this is only required because ℓ 2 's behavior differs in the two branches. If ℓ 2 behaves the same, no synchronization is required. Thus, the following program is okay: Because it behaves the same in both branches, ℓ 3 never needs to be informed about which branch is taken, even though it appears in the branches. Moreover, ℓ 2 only needs to be informed about which branch is taken after it receives its message from ℓ 3 . There are two types of functions available in Pirouette, local and global functions. Local functions expect a local value as input, stored on some particular node, whereas global functions expect a choreography as input. Both types of functions may be recursive. We write fun (ℓ. ) for the (recursive) function named which expects a local value on ℓ as input, and has body . We write ℓ. for the application of function to input which is stored on ℓ. For the global function named which takes an input named and has body , we write fun ( ) . As is traditional, we write 1 2 for the application of function 1 to 2 .
We adopt a call-by-value semantics, so we evaluate inputs to values before applying functions. As described in Section 2, local values are defined by the local language and are always closed. Choreography values are programs of any of the forms: (a) ℓ. (where is a local value), (b) fun (ℓ. ) (where the only free variables in are and ℓ. ), or (c) fun ( ) (where the only free variables in are and ).
We define an operation LN ( ) which collects all of the location names in in a set. We write FCV( ) for the free choreography variables in , and FEV( ) for the collection of free expression variables in , tagged with the locations that own them. We write FEV ℓ ( ) for the collection of expression variables free under ℓ in C.

Operational Semantics
Intuitively, if two locations ℓ 1 and ℓ 2 both take actions, they should be able to do this in either order. For instance, consider the Pirouette program ℓ 1 .2 + 3 ⇝ ℓ 2 . ; ℓ 3 .3 * 4 ⇝ ℓ 2 . ; . Here, ℓ 1 and ℓ 3 are both working on computations whose results they expect to send to ℓ 2 . Since these are different locations, both should be able to work on their programs at the same time. Thus in the semantics we should be able to reduce this program to either ℓ 1 .5 ⇝ ℓ 2 . ; ℓ 3 .3 * 4 ⇝ ℓ 2 . ; or ℓ 1 .2 + 3 ⇝ ℓ 2 . ; ℓ 3 .12 ⇝ ℓ 2 . ; , performing the local reductions in either order. However, ℓ 2 is just one location, so it cannot listen for two messages at once. Thus, even if we reduce the above program to ℓ 1 .5 ⇝ ℓ 2 . ; ℓ 3 .12 ⇝ ℓ 2 . ; we are forced to reduce the send from ℓ 1 before the send from ℓ 3 , since the second is waiting on ℓ 2 .
In order to allow for this behavior, we keep track of a set of blocked locations in our operational semantics. Intuitively, blocked locations cannot take a step. By keeping track of what locations are blocked, we can allow out-of-order-execution among non-blocked locations.
However, this is not quite enough to get the behavior we want. Consider this program, which represents a system where ℓ 1 branches on and then does nothing, while ℓ 2 returns the result of 3+5 independent of ℓ 1 's choice: if ℓ 1 . then ℓ 2 .3 + 5 else ℓ 2 .3 + 5. Here, ℓ 2 ought to be able to make progress, reducing this program to if ℓ 1 . then ℓ 2 .8 else ℓ 2 .8. Note that this progress was atomic. Thus, it would be illegitimate to reduce different programs in the two branches. For instance, reducing if ℓ 1 . then ℓ 2 .3 + 5 else ℓ 2 .3 * 4 to if ℓ 1 . then ℓ 2 .8 else ℓ 2 .12 requires reducing different

Fig. 3. Selected Choreography Operational Semantics
programs in the two branches, whereas, in reality, only one of those two programs should be reduced and that program should be chosen by ℓ 1 . In order to prevent this type of reduction, we track what reduction is happening, resulting in a labeled transition system. We refer to labels in Pirouette as "redices," and to a single label as a "redex. " In the second-to-last example above, we note that in each branch, we reduce a 3+5 to 8 on ℓ 2 . Since we are doing the same reduction in each branch, we can reduce the whole program.
Selected rules from the operational semantics can be found in Figure 3. The full rules, along with the syntax of redices, can be found in Appendix A.2.
Each rule has the form 1 = == ⇒ c 2 , where is a redex, is a set of locations, and 1 and 2 are choreographies. Intuitively, this says that 1 can reduce to 2 using redex even if every location in is blocked. With this interpretation, the rule SendE allows a location to reduce a message to a value before sending it. The notation ℓ 1 .( 1 ⇒ 2 ) ⇝ ℓ 2 is the redex for this reduction rule. Note that we check both that ℓ 1 ∉ and that ℓ 1 ≠ ℓ 2 in the premise of this rule. The first check ensures Choreography Types ::= ℓ 1 . | 1 @ℓ → 2 | 1 → 2 Local Contexts Γ ::= · | Γ, ℓ. : Choreography Contexts Δ ::= · | Δ, :

Fig. 4. Pirouette Types (Syntax and Selected Rules)
that ℓ 1 is not blocked, since the reduction happens at that location. The second check reflects the fact that sends from a node to itself is not meaningful. The rule SendI allows reductions under a send construct, but only when the reduction can take place with both the sender and the receiver blocked. This formalizes the intuition that while some locations are waiting, other locations can take actions. Sending is formalized with the rule SendV. This removes a send entirely. Note that in the substitution, ℓ 2 's variable is substituted with the message. This formalizes the intuition that sends are modeled by binding the message to a variable in the receiver's program.
The IfI rule is the only rule that makes use of redices. By ensuring that the same redex is reduced on each branch of the if, we make sure that the only reductions that can be made are those which are invariant under which branch is taken. Note that we again ensure that ℓ 1 is not taking an action in this reduction step, since it is currently occupied with the if itself.
The rules SyncI and Sync demonstrate the rather subtle effect that Sync has on the semantics. The first rule demonstrates that synchronization induces blocking on the relevant locations. However, Sync shows that this is the only effect that it has on the semantics of the choreography.
Finally, the rules AppGlobalFun, AppGlobalArg, and AppGlobal demonstrate how functions are treated. Both the function and its argument can be evaluated in any order, but the redex is tagged with which choice is made. This ensures that if statements don't reduce a function in one branch and its argument in the other. Finally, the AppGlobal rule shows that the semantics of a function is given as standard, with a parallel substitution. However, we require that there be no blockers. This comes from the fact that all of the locations work together to reduce functions at the same time.

Type System
Assuming that the local expression language has a type system as described in Section 2.4, we can develop a language of types for Pirouette. The syntax of Pirouette types can be found in Figure 4, along with selected typing rules. The full typing rules are in Appendix B.
There are three categories of Pirouette types, corresponding to the three categories of choreographic values. The first category is a local type at some location, which we write ℓ. . This is the type given to values of the form ℓ. . Then there is the type of local functions, which we write 1 @ℓ → 2 . Here, 1 is an expression type, corresponding to the type of the input to the function, which is expected to be located on ℓ. The function then returns a 2 , which is a choreography type.
Finally, there is the type of global functions which take an arbitrary choreographic type as an input. Thus, we write 1 → 2 , where 1 and 2 are both Pirouette types.
The choreographic type judgment is of the form Γ; Δ ⊢ : where Γ is a local context, Δ is a global context, is a choreography, and is a choreographic type. Global contexts are normal typing contexts relating choreography variables to choreography types. However, local contexts have to relate variables to types, but must also keep track of the location of the variable. Since each location is its own namespace, we relate variables paired with locations to local types (see the syntax of Γ in Figure 4).
For any location ℓ, we can recursively project the typing context of the location from a local context Γ as follows: Intuitively, this gives the context for the namespace ℓ.
We can see projection in action in the Send rule. Here, we check that has the local type at the location ℓ. We then check the remainder of the choreography under the assumption that has type at ℓ 2 , since after the send will be bound to the result of evaluating . Note that this works because values are closed; otherwise, might not typecheck in ℓ 2 's namespace.
The rule DefLocal shows how the program let ℓ. 1 in 2 acts as an elimination rule for the type ℓ. . We ensure that 1 has the type ℓ. , and then we bind to locally in 2 . Finally, FunLocal and FunGlobal produce local and global function types, respectively. Both also bind the function name to the appropriate function type, allowing for recursive function definitions. The choreographic type system enjoys progress and preservation if the local type system is sound. However, we can get more-precise guarantees, which we call relative progress and relative preservation.
Theorem 1 (Relative Preservation). If the local type system enjoys Preservation, then for every choreography 1 such that Γ; Δ ⊢ 1 : and 1 = == ⇒ c 2 , Γ; Δ ⊢ 2 : . Theorem 2 (Relative Progress). If the local type system enjoys Boolean Invertability and Progress, then for every choreography 1 such that ·; · ⊢ 1 : , either 1 is a choreography value or there are some , , and 2 such that 1 = == ⇒ c 2 . Corollary 1 (Relative Soundness). If the local type system is sound, as defined in Section 2.4, then the choreographic type system enjoys progress and preservation.
By dividing up the result into more-precise theorems, we are able to get some guarantees even when the local type system is not sound. For instance, the unityped -calculus example (Example 5) is not sound, but does guarantee preservation. Thus, Theorem 1 allows us to lift preservation to the choreographic system. In this case, we do not get choreographic progress, intuitively because we may get stuck when trying to evaluate a local expression, or when an if expression tries to discriminate on a non-boolean value.

EQUATIONAL REASONING
Choreographies represent collections of programs running in parallel. In order to represent these programs serially, we are forced to decide what behavior to write first. For instance, consider the program ℓ 1 .2 + 3 ⇝ ℓ 2 . ; ℓ 3 .3 * 4 ⇝ ℓ 4 . ; . The program represents ℓ 1 sending a message to ℓ 2 while ℓ 3 sends a message to ℓ 4 . We could have just as well represented that program as ; . Since these choreographies represent the same collection of programs, all of our constructs treat them the same way. In prior work on choreographies, this fact is typically formalized using a separate notion of equivalence, which says when two choreographies represent the same collection of programs [Cruz-Filipe and Montesi 2017a,b;Lanese et al. 2013;Montesi 2013]. Following that tradition, we define a notion of structural equivalence for Pirouette and study its properties. We define choreography equivalence as the smallest equivalence relation which is also a congruence and satisfies the rules in Figure 5. The complete formal definition can be found in Appendix C.
Choreography equivalence respects types, even for open programs: Theorem 3 (Equivalence Respects Types). If Γ; Δ ⊢ 1 : and 1 ≡ 2 , then Γ; Δ ⊢ 2 : Interestingly, Theorem 3 has an outsized influence on our system model. In particular, in order to prove that the rule SwapSendIf respects types, we need to know that expressions have unique types. After all, if 2 is given type 1 in the true branch, but type 2 in the false branch, there might not be a type that we could assign to 2 that makes both branches type check. Including a typing annotation on send statements might solve this problem. However, this would require mixing the type system with the syntax of choreographies. While this is a reasonable choice in many situations, here we choose to keep them separate, since that makes it easy to tell when our results rely on the type system and when they do not.
Equivalence can be used to define a new, seemingly simpler operational semantics for choreographies. This new semantics, which we write ⇒ ≡ , has no redices or block sets and it replaces internal steps from our semantics with the following rule: We formalize this semantics in Appendix A.4.
In fact, much of the prior work on choreographies defined their operational semantics in precisely this way [Carbone et al. 2014;Cruz-Filipe and Montesi 2017a,b;Lanese et al. 2013;Montesi 2013]. While this new semantics is good for prior work, it is too weak for Pirouette, which allows reduction of local expressions. To see why, consider the program ℓ 1 . 1 ⇝ ℓ 2 . ; ℓ 3 . 2 . It should be possible for ℓ 3 to evaluate its return value, even though ℓ 1 has not yet sent its message to ℓ 2 . However, under the equivalence-based semantics, there is no way to reduce 2 , since we cannot use an equivalence to bring it up to the top.
A similar problem appears for sends. Consider the program ℓ 1 . 1 ⇝ ℓ 2 . ; ℓ 3 . 2 ⇝ ℓ 2 . ; . In this example, both ℓ 1 and ℓ 3 are trying to send a message to ℓ 2 . If 2 can be reduced further, then ℓ 3 ought to be able to reduce 2 while waiting for ℓ 2 to be ready to receive the second message. However, in the equivalence-based semantics, we cannot use SwapSendSend to bring up the second send, since that would swap the order of ℓ 2 's receives.
Finally, consider programs that contain function applications, such as This program allows ℓ 1 to send a message to ℓ 2 and then applies the identity function to another choreography. Importantly, the argument choreography does not mention ℓ 1 or ℓ 2 . Therefore, ℓ 3 should be able to reduce 2 before ℓ 1 completes its send. However, it is not possible to do this in the equivalence-based definition mentioned before. This makes reasoning with ≡ much less powerful here than in previous choreographic systems. However, the difficulty is limited to the problems mentioned above.
Theorem 5 (Weak Semantics). Let = == ⇒ w be the relation obtained by modifying the relation = == ⇒ c as follows: • ℓ. can only reduce when the block set is empty, • messages can only be reduced when neither the sender nor the receiver are in the block set, and • in let ℓ. 1 in 2 and function application, subchoreographies can only reduce when the block set is empty.
(The semantics = == ⇒ w is formalized in Appendix A.3.) Then whenever 1 = == ⇒ w 2 , 1 ⇒ ≡ 2 . Moreover, whenever 1 ⇒ ≡ 2 , there is a redex and choreography ′ 2 such that 1 While this makes our connection to previous work more clear, we prefer to work with the = == ⇒ c relation defined in Section 3 due to its extra power.

ENDPOINT PROJECTION
While Pirouette programs are designed to represent a collection of concurrently-executing programs, so far that has been a guiding intuition rather than a formal property. In order to change that, we define the endpoint projection operation, which extracts a program for each location from a choreography, if it is possible to do so. This extracted program is expressed in a language called the control language which features local execution and explicit constructs for message passing. The extracted programs of all locations are composed in parallel. Here, we explain the control language, then explain the extraction and finally show that the parallel composition of all extracted programs reflects and preserves the operational semantics of the choreography.

The Control Language
Our control language ( Figure 6) is a concurrent -calculus where messages are values of local programs. It is inspired both by work on process calculi and by concurrent ML. Like with Pirouette, control programs have two types of variable: local variables and control variables. We write control variables with capital letters, because they play a role similar to that played by choreography variables. Local variables are the variables of local programs. There are correspondingly two types of functions, local functions and global functions (written fun l ( ) and fun g ( ) , respectively). Note that because in the control language-unlike in Pirouetteevery local program is at the same location, local substitution does not take location into account.
Control programs can return the result of evaluating a local program, which we write ret( ). We can use the result of such a program in another program using the syntax let ret( ) 1 in 2 . However, unlike choreographies, control programs can also return the trivial value ( ). This is used for control programs that do not have a return value on them.
Communication happens between control programs composed in parallel through explicit send and receive commands. We will see later how parallel composition works, and how communication takes place.
There are two forms of branching in the control language. "If" statements are standard, and are a sequential form of branching. We also have external choice, which is a distributed form of branching. The program allow ℓ choice | L ⇒ 1 | R ⇒ 2 represents allowing ℓ to choose which branch to take: 1 , labeled L, or 2 , labeled R. The syntax choose for ℓ; represents telling ℓ to take the branch labeled .
We refer to the parallel composition of a control program for each location as a system (we use the symbol Π to refer to systems). The notation ℓ ⊲ says that program is running on the node ℓ. As can be seen in Figure 6, a system is a finite parallel compositions of such ℓ ⊲ .
We often use the syntax ∥ ℓ ∈ ℓ to refer to a system where is a finite set of locations and − is a function from locations to control program expressions.

Label
: Location semantics. In defining the operational semantics of systems, two syntactic operations will be useful. The first is system lookup (written Π(A)), which refers to the control program bound to a particular location A. The second is system update (written Π[A ↦ → ]), which replaces the program bound to A. We define them as follows: The semantics of control programs is given via a labeled transition system. This allows systems to match up corresponding rules in their semantics. The syntax of labels and selected rules can be found in Figure 7, and the full set of rules can be found in Appendix D.
Internal steps that do not interact with the outside are given the label 1 . For instance, the rule SendE takes a local step in a message to be sent to ℓ, which is an internal step. Every step of a local program corresponds to an step.
Sends and receives are labeled with matching labels: ⇝ ℓ 2 for sends, and ℓ 1 : ⇝ for receives. Note that from the perspective of a single control-language program, receives are treated nondeterministically-any value could be received. Our system semantics will force sends and receives to match up. Similarly, external choice and its resolution have matching labels: ℓ : [ ] for external choice and [ ] ⇝ ℓ for its resolution.

System Label
: In choreographies, all participants must -reduce function applications together. For instance, consider reducing a local function: (fun (ℓ. ) ) ℓ.
Because the choreography steps from a choreography with a function application to one without, every location's control program changes. In order to accommodate this, we use a new label, sync . The only three rules labeled with sync are LetRet, AppLocal, and AppGlobal, all of which can be found in Figure 7.
System semantics. Systems are also given semantics via a labeled transition system. The system labels arise from a merging operator on control-language labels, where 1 ⊲⊳ 2 ensures that labels 1 and 2 match, producing an output system label . It also ensures that, in a function application, either both steps reduce the function or both reduce its argument. The syntax of system labels, label merge operator, and system semantics can all be found in Figure 8.
The labels and sync both refer to internal steps of a production. Hence, they can be merged with themselves to yield the corresponding system label. The rule Internal allows any location ℓ to take an internal step without interfering with any other location. Synchronized steps require the use of the Synchronized Internal rule, which requires that every location take a sync step.
Send and receive labels must be matched together. If ℓ 1 sends to ℓ 2 , their labels merge together to a system label ℓ 1 . −→ ℓ 2 in rule MergeComm. The rule Comm then allows both ℓ 1 and ℓ 2 to take their corresponding steps together, without interfering with any other locations. The Choice rule behaves similarly, but for choice-based branching.

Merging Control Programs
Our goal is to extract a control program for every location in a choreography compositionally. However, compositionality is greatly complicated by if branches. To see why, consider the following choreography: Intuitively, we want ℓ 2 to be associated with the control program send 3 to ℓ 1 ; allow ℓ 1 choice | L ⇒ ret(0) | R ⇒ ret (1) However, when defining our procedure formally, we want to extract a program for each branch of the if expression, and combine them together to get the final program. This leads to two issues. First, we need to be able to define a program for each branch. Second, we need to be able to merge those two programs into a single program.
To see why it is difficult to define a program for each branch, consider the true branch of the program above. We know that ℓ 1 will send a synchronization message to ℓ 2 . Thus, ℓ 2 must allow ℓ 1 to make a choice for it, as we saw earlier. However, here we only have the L branch available; the R branch will not be available until we merge.
To solve this problem, we add one-branch choice constructs to our control language: allow ℓ choice | L ⇒ and allow ℓ choice | R ⇒ These act precisely like the two-choice construct, except that they only allow their one branch to be taken. With these, we now have a program for ℓ 2 we intend to extract from the branch above: send 3 to ℓ 1 ; allow ℓ 1 choice | L ⇒ ret(0) We now need a way to merge the extracted programs from each branch into a single program. We define a partial merge operator ⊔, which ensures that two programs are the same until they allow both choices. We adopt notation from computability theory and write ( ) ↑ when is a partial function to denote that the function is undefined. So we would write 1 ⊔ 2 ↑ if the merge of 1 and 2 is undefined. We further write ( ) ↓ (so 1 ⊔ 2 ↓) if ( ) is defined, but we do not care about the value. In Figure 9, you can find the definition of the merge operator when the left-hand side is allow ℓ choice | L ⇒ 1 . The remaining parts of the definition can be found in Appendix E. Additional properties can be found in Appendix G.3.

Endpoint Projection, Defined
We are now ready to define endpoint projection, or EPP. Merging is an important part of the definition of EPP, and EPP inherits partiality from merging. We continue to use ( ) ↑ if ( ) is undefined and ( ) ↓ if ( ) is defined, but we do not care about the value.
Endpoint projection is defined as follows: Note a simple design principle: local expressions owned by a location other than the one being projected to are projected to ( ). This allows us to define a control program with the same control flow, but which does not know about the precise local expressions held at other locations.
This definition tells us what the control program for a single location is. However, we are interested in a system of control programs. We can lift the single-location definition to a multilocation system definition: = ∥ ℓ ∈ ℓ ⊲ ℓ . One way of thinking about ℓ is that it gives ℓ's view of . From this perspective, it makes sense to ask what ℓ's view of a step of computation is. We can provide this by projecting a choreography redex to a control-language label, as follows: Just as we can ask what some location's view of a step of computation is, we can ask what a system's view of a step of computation is. Interestingly, this does not rely on which locations are in the system, and it is therefore a total operation.

Properties of Endpoint Projection
EPP is one of the most-important operations on choreographies. It is what gives them a ground-truth interpretation as a parallel composition of programs. In fact, without EPP it would be almost impossible to state one of our most-important theorems: deadlock freedom by construction (Theorem 12 below). The first property we examine is how EPP treats equivalence. As with every other operation on choreographies, we would like it if EPP treated equivalent choreographies the same. Note that we have no notion of equivalence on control-language programs, so we get a strong notion of "treating the same": Theorem 6 (Equivalence Begets Equality). If 1 ≡ 2 , then 1 ℓ = 2 ℓ for every ℓ ∈ L.
Next we would like to examine the relationship between the semantics of a choreography and the semantics of its projection. However, there is still one remaining disconnect between the semantics of choreographies and that of systems that comes into play. Yet again, it has to do with the semantics of external choice. To see the issue, consider the following example: As you can see, by taking a choreography step which corresponds to a completely internal step on ℓ 1 , we have lost information about a possible path on ℓ 2 . This comes because the choice of the path is up to ℓ 1 , who "makes up their mind" in that internal step. One way to view this is from ℓ 2 's point of view. In the program 1 , ℓ 2 has a nondeterministic program: a message will come in to tell them which of two branches to take. This is evident in the semantics of the control language, since 1 ℓ 2 can take either of two steps. However, 1 is deterministic from ℓ 2 's point of view, since only one message is possible. Hence, this step has resolved some nondeterminism.
We formalize this notion of "the same program, but with some nondeterminism resolved" in a new relation called ≤ nd . This is nearly defined as the smallest relation that commutes with all of the control-language constructs and also fulfills the following extra rules: However, there is a small complication: functions are only related to themselves. The full definition can be found in Appendix F. The relation ≤ nd is a partial order. We extend the ≤ nd relation to systems pointwise, so Π 1 ≤ nd Π 2 if for every ℓ such that Π 1 (ℓ) ↓, Π 2 (ℓ) ↓ and Π 1 (ℓ) ≤ nd Π 2 (ℓ). The following theorem relates ≤ nd to the semantics of systems. It may look complicated, but is not. Its two bullet points respectively say: (1) If a less nondeterministic system takes a step, then that step is available to any more-nondeterministic system, and (2) If a more nondeterministic system takes a step but the less nondeterministic system is the result of projecting some choreography, then we can take advantage of the fact that choices are always paired in choreographies to mimic the step in the less nondeterministic system.
Theorem 7 (Lifting and Lowering System Steps Across ≤ nd ). If Π 1 ≤ nd Π 2 , then the following are both true: Finally, the less-nondeterminism relation allows us to connect the semantics of choreographies with the semantics of our control language. Steps in the choreographies correspond to actions by one or more locations. If a step involves a location, then that location's control program also takes a step; the label of that step is the projection of the redex of the choreographic step. However, if a step does not involve a location, then that location's control program does not take a step and the projection of the redex for that location is undefined. While an uninvolved location does not take a step, it may find its nondeterminism reduced as other locations "make up their minds" about what branch it should take in the future.
The requirement that every location named in is in is important: if represents ℓ 1 sending a message to ℓ 2 , but ℓ 2 is not in , then there is no one in to do the receiving. This blocks ℓ 1 from sending its message (since message passing is synchronous) and thus blocks the system step from taking place. However, if both ℓ 1 and ℓ 2 are in , then Theorem 8 tells us that ℓ 2 is guaranteed to be ready to receive ℓ 1 's message.
A similar difficulty comes when trying to go in the other direction: it is not enough to know that ℓ 1 's projection sends a message for a choreography to take a step; we must also know that ℓ 2 's projection receives it. This means that we have to state local soundness differently depending on the label of the control-program step: Theorem 10 (Local Soundness). All of the following are true: The requirement that LN ( 1 ) ⊆ ≠ ∅ may seem unusual in the last case of Theorem 10. In order to -reduce a function call or a subexpression let ℓ.
1 in 2 inside a choreography , every location in must be able to perform the same -reduction. However, if we only require that every location in LN ( ) be able to make a step, the requirement might be trivial if does not name any locations. Therefore, we require that every location in some nonempty set of locations which contains every location in LN ( ) be able to make a step. In the common case where LN ( ) is nonempty, this restriction is the same as the simpler requirement.
Lifting soundness from control programs to systems yields a much simpler theorem. However, note how the strange requirement for -reduction steps infects the theorem: Theorem 11 (Global Soundness). If LN ( 1 ) ⊆ ≠ ∅ and 1 = ⇒ S Π then there is an and 2 such that (a) 2 ↓, (b) 2 ≤ nd Π, (c) = , and (d) 1 We use these to develop the most important theorem for Pirouette (and choreographies in general): deadlock freedom by design. Interestingly, the proof is a simple interplay of soundness and completeness for our translation along with type soundness.
Theorem 12 (Deadlock Freedom By Design). If choreography typing enjoys both progress and preservation (e.g., if local typing is sound), ·; · ⊢ 1 : , and 1 = = ⇒ * S Π, then either every location in Π maps to a control-language value, or there are and Π ′ such that Π = ⇒ S Π ′ .
Sketch of the mechanized proof. By soundness, there are a list of redices and a choreography 2 such that 1 ∅ = == ⇒ c 2 and 2 ≤ nd Π. By preservation, ·; · ⊢ 2 : , and by progress either 2 is a choreography value or there are and 3 such that 2 ∅ = = ⇒ c 3 . If 2 is a value, then every location in Π maps to a control-language value, and we are done. Otherwise, completeness tells us there is a Π ′′ such that 2 = == ⇒ S Π ′′ . We can then use Theorem 7 to get a Π ′ such that Π = == ⇒ S Π ′ , as desired. □

NOTES ON THE COQ CODE
In this paper, we have presented all of our work in a standard, named style. However, in our Coq code we use a nameless style with de Bruijn indices. While normally this would not pose any difficulties, we have taken the unusual step of treating the local language generically. Here, we give the nameless version of our requirements on the local language, ensuring that the transition to the named style does not create undue confusion. First, we require that expressions have decidable syntactic equality-usually a trivial requirement, since programs are usually sentences from a context-free grammar. Next, we formalize the fact that variables must be expressions by requiring a mathematical function var from natural numbers to expressions. In all of our examples, this is a terminal in the language, but this is not required. Instead of the ability to compute the set of free variables of an expression, we require a predicate Closed ( ), which means that there are no free variables above in . We require that Closed (var( )) if and only if < , and we write Closed( ) for Closed 0 ( ).
Substitution is changed to allow for infinite parallel substitution. Formally, we require an operation [ ] where is a mathematical function from natural numbers to expressions. This must obey the following equations: The last requirement is important because Coq is an intensional type theory, so functions that behave the same on all inputs are not necessarily equal. The other three equations are nameless versions of the equations in Section 2. Finally, we require an additional renaming operation, which we write ⟨ ⟩, where is a mathematical function from natural numbers to natural numbers. This must satisfy the equation ⟨ ⟩ = [ ↦ → var( ( ))]. While this equation could serve as a definition of renaming, it is often useful to define and reason about it separately. For instance, we can use renaming to define exchange and weakening in typing.
Typing judgments in the nameless setting use contexts which are mathematical functions from natural numbers to types. The requirements in Figure 1 are then equivalent to the following requirements: Note that both Exchange and Weakening are absorbed into the more-general Weakening rule. Moreover, we made Substitution infinitary. The Var and Strengthening rules are straightforward transformations of the named versions in Figure 1.

Choreographies
Choreographies originate as a way of writing web services. The W3C released a report on choreographies as a way to write web services [(W3C) 2004], which originated the idea of endpoint projection [Zongyan et al. 2007] (see Cruz-Filipe and Montesi [2017a] for the historical note). Soon, there was work formalizing and understanding choreographies from this point of view. Choreographic programming as a paradigm originates with Montesi's Ph.D. thesis [Montesi 2013]. There, he develops the first choreographic programming language and begins exploring the formal properties thereof. Later works extend this idea, with Cruz-Filipe and Montesi [2017a] creating a core calculus of choreographies and Carbone and Montesi [2013] combining choreographies with session types to ensure that endpoint projection never fails. However these works were all lower-order, used equivalence-based semantics, and had no mechanized metatheory.
More closely related with this project, Cruz-Filipe and Montesi [2017b] create a choreographic language with procedures and the ability to make procedure calls. While parts of our endpoint projection definition are inspired by this work, procedural choreographies remain resolutely lowerorder. Procedures are global and shared, but cannot be treated as data; moreover, they cannot take other choreographies as inputs nor return them as outputs. However, unlike our functions, these procedures are able to take locations as inputs. This is harder in our setting because locations are part of types; we consider polymorphism (including location polymorphism) to be future work.
Some work has been done on higher-order choreographies. The Choral Project [Giallorenzo et al. 2020] builds choreographies on top of object-oriented programming. However, Choral has never been formalized, and so the theoretical underpinnings of higher-order choreographies were left unexplored.
Significantly, concurrent and completely independent work on functional choreographies has recently been undertaken by Cruz-Filipe et al. [2021a]. This work resembles Pirouette in several ways, but has a significantly different design. Most importantly, they identify the local language with the choreography language. This design choice allows functions to be sent as messages, but they require that messages only mention a single location, preventing functions sent as messages from including communication. It also leads to a simpler system, but makes it much harder for them to identify the core features of the local language which allow for type soundness of the choreographic language. Moreover, their operational semantics allows for functions to be reduced; this allows them to not need as many synchronizations as Pirouette projection requires. However, it violates the common requirement of call-by-value languages that functions be treated as values and makes execution more unpredictable. We preferred to keep the simpler and more-traditional operational semantics. Finally, they do not have any mechanized formalization of their system.
Mechanization. Two very recent papers have mechanized the metatheory of core choreographies, but both are lower-order. Cruz-Filipe et al. [2021c] use Coq to formalize the core calculus of choreographies developed by Cruz-Filipe and Montesi [2017a], modified so that the language of local computations is a parameter. The focus is on proving that the language is Turing-complete. In the meantime, Cruz-Filipe et al. [2021b] extend that work to verify (in Coq) endpoint projection and deadlock freedom of the same language.
Interestingly, both these papers formalize out-of-order execution for choreographies using a labeled-transition system, similar to ours. As far as we are aware, they, along with a forthcoming book on choreographies [Montesi 2020] were the first to do so, though our work was formalized before we discovered their concurrent work. Their work takes inspiration from Honda et al. [2016], who use a similar labeled-transition system semantics for multiparty session types. Thus, they do not use any construct similar to our block sets. This means that they cannot allow locations to locally reduce their messages when the receiver of that message is blocked. While for their language this does not matter (since messages do not reduce at all), in our setting this would be problematic.

Functional Concurrent Programming
There is a long tradition of mixing functional and concurrent programming in principled ways. In practice, this often leads to languages that look a lot like our control language, including the concurrency features in Racket [The Racket Team 2021]. The first academic language with channels and communication in a functional language was Facile [Giacalone et al. 1989]. Even before then, work on parallelizing compilers for functional programming was popular. Burton [1987] considered adding annotations to functions describing when arguments should be evaluated at what location.
Currently, the most related academic project might be Links [Cooper et al. 2006] and its core language, the RPC calculus [Cooper and Wadler 2009]. Links also provides for a mixture of higherorder typed functional programming and concurrency. However, in Links, communication always happens at function boundaries, unlike Pirouette. Moreover, the RPC calculus only allows for one thread of execution, even when multiple unrelated locations can profitably be taking actions. This is in contradiction to the work on choreographies-and Pirouette in particular-where unrelated locations can compute and even pass messages concurrently.
Another language which mixes functional and concurrent programming is Murphy VII et al.'s ML5 [Licata and Harper 2010;Murphy VII et al. 2007]. ML5 has a type system for communication based on the Kripke semantics of modal logic. Interestingly, our type system also takes inspiration from modal logic: our type system can be seen as (the Curry-Howard analogue of) a degenerate form of the proof system for modal logic. Their use of the Kripke semantics makes sense, however, because different worlds can be viewed as different machines. Unfortunately, this led to difficulties in shipping some data that could be treated as code, so ML5 focuses on annotating mobile code, which includes static types like strings and integers, but not functions or local resources like arrays. This restriction is necessary due to their use of local state. Since Pirouette has no state, is has no such constraint.

A.2 Block-Set Semantics
See Section 3.1 for discussion.

A.3 Weak Block-Set Semantics
See Section 4 for discussion.

A.4 Equivalence-Based Semantics
See Section 4 for discussion. EqivStep

G.1 Additional Properties of the Pirouette Type System
While we do not explicitly supply the structural rules, our type system admits them: Theorem 13 (Pirouette Types Structural Rules). The choreographic type system admits weakening, exchange, and strengthening in both contexts. In other words, the following rules are admissible:

G.2 Additional Properties of Choreography Equivalence
Our syntactic operations respect choreography equivalence: Theorem 14 (Equivalence of Syntactic Operations). If 1 ≡ ′ 1 and 2 ≡ ′ 2 , then all of the following statements are true: •
When a more-nondeterministic expression takes a step, it may be taking advantage of the extra nondeterminism to take a step not available to the original. We can take advantage of the fact that our operational semantics is defined via a labeled-transition system to lift steps which do not resolve nondeterminism. In order to turn this into a theorem, we need to determine when a label may reduce an external choice. We do this with the predicate Choice ( ), which we define as follows: Choice ( )

Choice (Arg( ))
With the definition of Choice (−) in hand, we can prove the following theorem: