refcaps.lyx

#LyX 2.2 created this file. For more info see http://www.lyx.org/
\lyxformat 508
\begin_document
\begin_header
\save_transient_properties true
\origin unavailable
\textclass extreport
\use_default_options true
\begin_modules
fixltx2e
fix-cm
theorems-ams-bytype
\end_modules
\maintain_unincluded_children false
\language british
\language_package default
\inputencoding auto
\fontencoding global
\font_roman "default" "default"
\font_sans "default" "default"
\font_typewriter "default" "default"
\font_math "auto" "auto"
\font_default_family default
\use_non_tex_fonts false
\font_sc false
\font_osf false
\font_sf_scale 100 100
\font_tt_scale 100 100
\graphics default
\default_output_format default
\output_sync 0
\bibtex_command default
\index_command default
\paperfontsize default
\spacing single
\use_hyperref false
\papersize default
\use_geometry false
\use_package amsmath 1
\use_package amssymb 1
\use_package cancel 1
\use_package esint 1
\use_package mathdots 1
\use_package mathtools 1
\use_package mhchem 1
\use_package stackrel 1
\use_package stmaryrd 1
\use_package undertilde 1
\cite_engine basic
\cite_engine_type default
\biblio_style plain
\use_bibtopic false
\use_indices false
\paperorientation portrait
\suppress_date true
\justification true
\use_refstyle 1
\index Index
\shortcut idx
\color #008000
\end_index
\secnumdepth 3
\tocdepth 1
\paragraph_separation indent
\paragraph_indentation default
\quotes_language english
\papercolumns 1
\papersides 2
\paperpagestyle default
\tracking_changes false
\output_changes false
\html_math_output 0
\html_css_as_file 0
\html_be_strict false
\end_header

\begin_body

\begin_layout Chapter
\begin_inset CommandInset label
LatexCommand label
name "chap:Reference-Capabilities"

\end_inset

Reference Capabilities
\end_layout

\begin_layout Standard
Capabilities were introduced to support protection across processes 
\begin_inset CommandInset citation
LatexCommand cite
key "lampson1974protection"

\end_inset

, and have been adopted into several branches of computing since.
 The term 
\emph on
object capabilities
\emph default
 was coined by Mark Miller 
\begin_inset CommandInset citation
LatexCommand cite
key "miller2006robust,miller2003capability"

\end_inset

 to describe the set of operations an object is allowed to apply on some
 other object.
 Mark Miller proposes that in order to restrict this set, one should create
 a new object which only offers these capabilities, and which delegates
 to the original object.
 This is a critical insight: in a memory safe language, the methods on an
 object are the capabilities available on that object.
\end_layout

\begin_layout Standard
A 
\emph on
reference capability
\emph default
 is a type qualifier annotation on a reference, rather than an object, that
 modifies the capabilities available on the underlying object when it is
 accessed through that reference.
 In Pony, reference capabilities are used to statically ensure data-race
 freedom.
 The term 
\emph on
reference capability
\emph default
 was introduced specifically to distinguish these Pony annotations from
 object capabilities 
\begin_inset CommandInset citation
LatexCommand cite
key "clebsch2015deny"

\end_inset

.
\end_layout

\begin_layout Standard
In previous work, type qualifiers for data-race freedom have been expressed
 as 
\emph on
permissions
\emph default
 
\begin_inset CommandInset citation
LatexCommand citep*
key "boyland2001capabilities"

\end_inset

, 
\emph on
fractional permissions
\emph default
 
\begin_inset CommandInset citation
LatexCommand citep*
key "boyland2003checking"

\end_inset

, 
\emph on
uniqueness
\emph default
 
\begin_inset CommandInset citation
LatexCommand citep*
key "clarke2003external"

\end_inset

, 
\emph on
immutability
\emph default
 
\begin_inset CommandInset citation
LatexCommand citep*
key "ostlund2008ownership"

\end_inset

, and 
\emph on
isolation
\emph default
 
\begin_inset CommandInset citation
LatexCommand citep*
key "gordon2012uniqueness"

\end_inset

 (a refinement of 
\emph on
separate uniqueness
\emph default
 
\begin_inset CommandInset citation
LatexCommand cite
key "haller2010capabilities"

\end_inset

, which is a refinement of 
\emph on
external uniqueness
\emph default
 
\begin_inset CommandInset citation
LatexCommand citep*
key "clarke2003external"

\end_inset

).
\end_layout

\begin_layout Standard
These approaches use type qualifiers to describe what a reference is 
\emph on
allowed
\emph default
 to do.
 Pony's type system takes a different approach and uses reference capabilities
 to describe what other aliases are 
\emph on
denied
\emph default
 
\begin_inset CommandInset citation
LatexCommand citep*
key "dodds2009deny"

\end_inset

 by the existence of a reference.
 This is accomplished using a matrix of 
\emph on
deny properties
\emph default
, with notions such as isolation, mutability, and immutability all being
 derived from these properties.
 What aliases to the object are allowed to do is explicit rather than implied,
 whereas what the reference is allowed is derived.
 This change in approach gives a derivation for properties previously considered
 intrinsic, and models a reduction in reference capabilities as a weaker
 guarantee.
\end_layout

\begin_layout Standard
Other approaches have combined actors with data-race freedom, such as minimal
 ownership for active objects 
\begin_inset CommandInset citation
LatexCommand cite
key "clarke2008minimal"

\end_inset

, capabilities for uniqueness and borrowing in Scala 
\begin_inset CommandInset citation
LatexCommand cite
key "haller2010capabilities"

\end_inset

, and Kilim 
\begin_inset CommandInset citation
LatexCommand cite
key "srinivasan2008kilim"

\end_inset

.
 However, various useful patterns have not been supported, e.g.
 traversing and modifying an isolated data structure, or updating an object
 and then sending it in a message while keeping read access to it.
 By taking a more fundamental view of reference capabilities, a more flexible
 type system that supports such patterns became possible.
\end_layout

\begin_layout Standard
The matrix of deny properties exposes two novel reference capability types,
 
\begin_inset Formula $\mathtt{tag}$
\end_inset

 and 
\begin_inset Formula $\mathtt{trn}$
\end_inset

 (
\emph on
transition
\emph default
).
 A 
\begin_inset Formula $\mathtt{tag}$
\end_inset

 reference capability allows identity comparison and 
\emph on
asynchronous 
\emph default
method call, but does not allow reading from or writing to the reference.
 Actors are typed as 
\begin_inset Formula $\mathtt{tag}$
\end_inset

, which allows them to be integrated into the object type system and passed
 in messages.
 A 
\begin_inset Formula $\mathtt{trn}$
\end_inset

 reference capability is a new form of uniqueness, 
\emph on
write uniqueness
\emph default
, that describes objects that can only be written to through a single reference,
 but can be read from through many aliases.
\end_layout

\begin_layout Standard
This work also extends 
\emph on
viewpoint adaptation
\emph default
 
\begin_inset CommandInset citation
LatexCommand cite
key "cunningham2008universe,gordon2012uniqueness"

\end_inset

 to apply to every reference capability and introduce the concept of 
\emph on
safe to write
\emph default
, which, taken together, allow reading from and writing to both unique objects
 and unique fields.
 The types of 
\emph on
temporary identifiers
\emph default
 are treated differently from those of permanent paths, which allows the
 traversal of unique structures, something that is not possible using other
 approaches 
\begin_inset CommandInset citation
LatexCommand cite
key "gordon2012uniqueness,haller2010capabilities,clarke2008minimal"

\end_inset

.
\end_layout

\begin_layout Standard
In this system, an alias may have a different reference capability from
 the initial reference.
 This addresses a key issue in reference capability systems, namely that
 sub-typing is not reflexive: an isolated type cannot be assigned to a field
 or local variable unless the source reference is eliminated with a technique
 such as 
\emph on
destructive read 
\emph default
or 
\emph on
alias burying
\emph default
 
\begin_inset CommandInset citation
LatexCommand citep*
key "boyland2001alias"

\end_inset

.
 As a part of this, the type system supports 
\emph on
unaliased types
\emph default
, which provide static alias tracking without alias analysis.
\end_layout

\begin_layout Standard
Reference capabilities based on deny properties also provide a static 
\emph on
region
\emph default
 system 
\begin_inset CommandInset citation
LatexCommand citep*
key "grossman2002region"

\end_inset

, requiring no additional annotation.
 The 
\begin_inset Formula $\mathtt{trn}$
\end_inset

 reference capability provides a new form of 
\emph on
write region
\emph default
, in which a region boundary applies to write operations but not read operations.
\end_layout

\begin_layout Section
Deny Properties
\end_layout

\begin_layout Standard
\begin_inset Float table
wide true
sideways false
status open

\begin_layout Plain Layout
\begin_inset ERT
status open

\begin_layout Plain Layout


\backslash
makebox[
\backslash
textwidth][c]{
\end_layout

\end_inset


\end_layout

\begin_layout Plain Layout
\align center
\begin_inset Tabular
<lyxtabular version="3" rows="5" columns="4">
<features tabularvalignment="middle">
<column alignment="center" valignment="top" width="0pt">
<column alignment="center" valignment="top" width="0pt">
<column alignment="center" valignment="top">
<column alignment="center" valignment="top">
<row>
<cell alignment="center" valignment="top" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" bottomline="true" leftline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\size tiny
Deny global read/write aliases
\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" bottomline="true" leftline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\size tiny
Deny global write aliases
\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" bottomline="true" leftline="true" rightline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\size tiny
Allow all global aliases
\end_layout

\end_inset
</cell>
</row>
<row>
<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\size tiny
Deny local read/write aliases
\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\size tiny
\emph on
\begin_inset ERT
status open

\begin_layout Plain Layout


\backslash
cellcolor{writeable}
\end_layout

\end_inset

Isolated (
\begin_inset Formula $iso$
\end_inset

)
\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" leftline="true" rightline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\end_layout

\end_inset
</cell>
</row>
<row>
<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\size tiny
Deny local write aliases
\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\size tiny
\emph on
\begin_inset ERT
status open

\begin_layout Plain Layout


\backslash
cellcolor{writeable}
\end_layout

\end_inset


\emph default
Transition (
\begin_inset Formula $\mathtt{trn}$
\end_inset

)
\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\size tiny
\emph on
\begin_inset ERT
status open

\begin_layout Plain Layout


\backslash
cellcolor{readable}
\end_layout

\end_inset

Value (
\begin_inset Formula $val$
\end_inset

)
\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" leftline="true" rightline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\end_layout

\end_inset
</cell>
</row>
<row>
<cell alignment="center" valignment="top" topline="true" bottomline="true" leftline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\size tiny
Allow all local aliases
\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" bottomline="true" leftline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\size tiny
\emph on
\begin_inset ERT
status open

\begin_layout Plain Layout


\backslash
cellcolor{writeable}
\end_layout

\end_inset


\emph default
Reference (
\begin_inset Formula $\mathtt{ref}$
\end_inset

)
\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" bottomline="true" leftline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\size tiny
\emph on
\begin_inset ERT
status open

\begin_layout Plain Layout


\backslash
cellcolor{readable}
\end_layout

\end_inset


\emph default
Box (
\begin_inset Formula $\mathtt{box}$
\end_inset

)
\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" bottomline="true" leftline="true" rightline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\size tiny
\emph on
\begin_inset ERT
status open

\begin_layout Plain Layout


\backslash
cellcolor{opaque}
\end_layout

\end_inset

Tag (
\begin_inset Formula $tag$
\end_inset

)
\end_layout

\end_inset
</cell>
</row>
<row>
<cell alignment="center" valignment="top" topline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" bottomline="true" leftline="true" rightline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\size tiny
\emph on
\begin_inset ERT
status open

\begin_layout Plain Layout


\backslash
cellcolor{writeable}
\end_layout

\end_inset


\emph default
(Mutable)
\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" bottomline="true" rightline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\size tiny
\emph on
\begin_inset ERT
status open

\begin_layout Plain Layout


\backslash
cellcolor{readable}
\end_layout

\end_inset


\emph default
(Immutable)
\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" bottomline="true" rightline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\size tiny
\emph on
\begin_inset ERT
status open

\begin_layout Plain Layout


\backslash
cellcolor{opaque}
\end_layout

\end_inset


\emph default
(Opaque)
\end_layout

\end_inset
</cell>
</row>
</lyxtabular>

\end_inset


\end_layout

\begin_layout Plain Layout
\begin_inset ERT
status open

\begin_layout Plain Layout

}
\end_layout

\end_inset


\end_layout

\begin_layout Plain Layout
\begin_inset Caption Standard

\begin_layout Plain Layout
\begin_inset CommandInset label
LatexCommand label
name "tab:Capability-matrix.-Capabilities"

\end_inset

Reference capability matrix
\end_layout

\end_inset


\end_layout

\end_inset


\end_layout

\begin_layout Standard
Rather than indicate which operations are allowed on a reference
\begin_inset Foot
status collapsed

\begin_layout Plain Layout
The term 
\emph on
reference 
\emph default
is used to mean the path currently being considered, and 
\emph on
alias
\emph default
 to mean any other path to the same object.
\end_layout

\end_inset

, reference capabilities indicate what operations are 
\emph on
denied
\emph default
 on aliases (other references) to the same object.
 Deny properties distinguish what is denied to the actor that holds a reference
 (local aliases) from what is denied to all other actors (global aliases).
 Each reference capability stands for a pair of local and global deny properties.
 These are shown in table 
\begin_inset CommandInset ref
LatexCommand ref
reference "tab:Capability-matrix.-Capabilities"

\end_inset

.
 For example, 
\begin_inset Formula $\mathtt{ref}$
\end_inset

 denies global aliases that can read from or write to the object, but it
 allows local aliases to both read from and write to it.
\end_layout

\begin_layout Standard
No reference capability can deny local aliases that it allows globally.
 Therefore, some cells in the matrix are empty.
 For example, there is no reference capability that denies local read and
 write aliases, but denies only write aliases globally.
 This is because local execution is a subset of global execution.
 As such, local deny properties can be weaker than global deny properties,
 but not stronger.
\end_layout

\begin_layout Standard
These deny properties are used to derive the operations permitted on a reference.
 A reference that denies global read and write aliases is safe to both read
 and write, i.e.
 is 
\emph on
mutable
\emph default
, since it guarantees that no other actor can read from or write to the
 object.
 A reference that denies only global write aliases is only safe to read,
 i.e.
 
\emph on
immutable
\emph default
, since it guarantees no other actor will write to the object, but does
 not guarantee no other actor will read from it.
 A reference that allows all global aliases is not safe to either read or
 write, i.e.
 it is opaque.
\end_layout

\begin_layout Standard
When the local deny properties and the global deny properties of a reference
 are the same, the reference can be safely sent as an argument to an asynchronou
s method call to another actor, i.e.
 it is 
\emph on
sendable
\emph default
.
 In other words, when the local alias deny properties are the same as the
 global alias deny properties, it does not matter which actor holds the
 reference.
 Reference capabilities in italics in table 
\begin_inset CommandInset ref
LatexCommand ref
reference "tab:Capability-matrix.-Capabilities"

\end_inset

 are 
\emph on
sendable.
\end_layout

\begin_layout Section
Short Examples
\end_layout

\begin_layout Standard
The following examples are compact and artificial.
 A more complete example, using a sample program from the compiler distribution,
 is in section 
\begin_inset CommandInset ref
LatexCommand ref
reference "sec:Code-Example"

\end_inset

, along with a line by line explanation.
\end_layout

\begin_layout Standard
A 
\begin_inset Formula $\mathtt{ref}$
\end_inset

 reference to an object denies global read/write aliases.
 As a result, it is safe to mutate the object, since no other actor can
 read from it.
 This is effectively a traditional object-oriented 
\emph on
reference type
\emph default
.
\end_layout

\begin_layout Standard
If an actor has a 
\begin_inset Formula $\mathtt{box}$
\end_inset

 reference to an object, no alias can be used by other actors to write to
 that object.
 This means that other actors may be able to read the object, and aliases
 in the same actor may be able to write to it (although not both: if the
 actor can write to the object, other actors cannot read from it).
 Using 
\begin_inset Formula $\mathtt{box}$
\end_inset

 for immutability allows a program to enforce read-only behaviour, similar
 to 
\begin_inset Formula $\mathtt{const}$
\end_inset

 in C/C++.
 For example:
\end_layout

\begin_layout Standard
\begin_inset listings
inline false
status open

\begin_layout Plain Layout

class List
\end_layout

\begin_layout Plain Layout

  fun box size1(): Int => ...
\end_layout

\begin_layout Plain Layout

  fun val size2(): Int => ...
\end_layout

\end_inset


\end_layout

\begin_layout Standard
Note that the receiver reference capability is specified after the keyword
 
\begin_inset Formula $\mathtt{fun}$
\end_inset

.
 In 
\begin_inset Formula $\mathtt{size1}$
\end_inset

, by indicating that the receiver has 
\begin_inset Formula $\mathtt{box}$
\end_inset

 reference capability, we can be certain that 
\begin_inset Formula $\mathtt{this}$
\end_inset

 will not be mutated when calculating its size.
 In addition, immutability is transitive, so no readable fields of 
\begin_inset Formula $\mathtt{this}$
\end_inset

 will be mutated either.
 Since 
\begin_inset Formula $\mathtt{box}$
\end_inset

 denies global write aliases but does not deny local write aliases, it is
 possible for 
\begin_inset Formula $\mathtt{this}$
\end_inset

 to be mutated through some alias if that alias is held by the same actor.
 The 
\begin_inset Formula $\mathtt{box}$
\end_inset

 reference functions as a 
\emph on
black box
\emph default
: the underlying object may be mutable through an alias or it may be immutable
 through any alias, but in any case it is immutable through this reference.
 This form of immutability is referred to as 
\emph on
local immutability
\emph default
.
\end_layout

\begin_layout Standard
In 
\begin_inset Formula $\mathtt{size2}$
\end_inset

, by indicating that the receiver has 
\begin_inset Formula $\mathtt{val}$
\end_inset

 reference capability, we make a stronger guarantee: we deny both local
 and global write aliases.
 As a result, it is not possible for 
\begin_inset Formula $\mathtt{this}$
\end_inset

 (and all its readable fields) to be mutated, regardless of other aliases,
 nor will it be mutated at any time in the future.
 This form of immutability is referred to as 
\emph on
global immutability
\emph default
.
\end_layout

\begin_layout Standard
Since a 
\begin_inset Formula $\mathtt{val}$
\end_inset

 reference has the same local and global deny properties, it is possible
 to 
\emph on
send
\emph default
 a 
\begin_inset Formula $\mathtt{val}$
\end_inset

 reference to another actor.
 A 
\begin_inset Formula $\mathtt{val}$
\end_inset

 reference is effectively a 
\emph on
value type
\emph default
, similar to values in functional languages.
\end_layout

\begin_layout Standard
\begin_inset listings
inline false
status open

\begin_layout Plain Layout

actor Dataflow
\end_layout

\begin_layout Plain Layout

  be calculate1(list: List val) => ...
\end_layout

\begin_layout Plain Layout

  be calculate2(list: List box) // Not allowed
\end_layout

\end_inset


\end_layout

\begin_layout Standard
The keyword 
\begin_inset Formula $\mathtt{actor}$
\end_inset

 is used to indicate a class that can have 
\emph on
behaviours
\emph default
 (asynchronous methods), and the keyword 
\begin_inset Formula $\mathtt{be}$
\end_inset

 is used to define behaviours.
 A behaviour is executed asynchronously by the receiving actor, and a given
 actor executes only one behaviour at a time, making behaviours 
\emph on
atomic
\emph default
.
 While executing a behaviour, the receiver sees itself (i.e.
 
\begin_inset Formula $\mathtt{this}$
\end_inset

 in the behaviour) as 
\begin_inset Formula $\mathtt{ref}$
\end_inset

, and is able to freely read from and write to its own fields.
 However, at the call-site, a behaviour does not read from or write to the
 receiver, and so a behaviour can be called on a 
\begin_inset Formula $\mathtt{tag}$
\end_inset

 receiver.
\end_layout

\begin_layout Standard
In 
\begin_inset Formula $\mathtt{calculate1}$
\end_inset

, the 
\begin_inset Formula $\mathtt{list}$
\end_inset

 parameter is guaranteed to be deeply and globally immutable, because a
 
\begin_inset Formula $\mathtt{val}$
\end_inset

 is guaranteed to have no local or global write aliases.
 As a result, it is safe to share this object amongst actors.
 Denying local and global write aliases means no actor can write to the
 object, regardless of how many actors have an alias to 
\begin_inset Formula $\mathtt{list}$
\end_inset

, making concurrent reads safe without copying, locks, or any other runtime
 safety mechanism.
 In 
\begin_inset Formula $\mathtt{calculate2}$
\end_inset

, a parameter of type 
\begin_inset Formula $\mathtt{List\,box}$
\end_inset

 is rejected by the type system, as a 
\begin_inset Formula $\mathtt{box}$
\end_inset

 does not deny local write aliases, making it unsafe to send a 
\begin_inset Formula $\mathtt{box}$
\end_inset

 to another actor as the sending actor could retain a mutable alias.
\end_layout

\begin_layout Standard
A 
\begin_inset Formula $\mathtt{tag}$
\end_inset

 reference has no deny properties, but it can be used for 
\emph on
asynchronous 
\emph default
method calls, i.e.
 calling behaviours.
 A reference capability with no permissions has appeared in previous work
 
\begin_inset CommandInset citation
LatexCommand cite
key "Naden:2012:TSB:2103621.2103722"

\end_inset

, but without allowing asynchronous method calls.
\end_layout

\begin_layout Standard
\begin_inset listings
inline false
status open

\begin_layout Plain Layout

actor Dataflow
\end_layout

\begin_layout Plain Layout

  be step(list: List val, flow: Dataflow tag) => ...
\end_layout

\end_inset


\end_layout

\begin_layout Standard
Here, we can call behaviours on 
\begin_inset Formula $\mathtt{flow}$
\end_inset

, but we cannot read or write the fields of 
\begin_inset Formula $\mathtt{flow}$
\end_inset

.
 However, when 
\begin_inset Formula $\mathtt{flow}$
\end_inset

 executes those behaviours asynchronously, it will see itself as a 
\begin_inset Formula $\mathtt{ref}$
\end_inset

, allowing it to mutate its own state.
 As such, 
\begin_inset Formula $\mathtt{tag}$
\end_inset

 allows actors themselves to have a reference capability, thus integrating
 them into the type system and allowing threads of control (in the form
 of actors) to be treated as first-class values.
 In contrast to existing systems 
\begin_inset CommandInset citation
LatexCommand cite
key "gordon2012uniqueness"

\end_inset

, this allows for the formalisation of both dynamic thread creation (actor
 constructors) and communicating actor graphs of any shape (including cycles).
\end_layout

\begin_layout Standard
In order to pass mutable data between actors, we use 
\begin_inset Formula $\mathtt{iso}$
\end_inset

 references.
 All mutable reference capabilities deny global read/write aliases, allowing
 them to be written to because no other actor can read from the object.
 An 
\begin_inset Formula $\mathtt{iso}$
\end_inset

 reference also denies local read/write aliases, which means if the 
\begin_inset Formula $\mathtt{iso}$
\end_inset

 reference is sent to another actor, we are guaranteed that the sending
 actor no longer holds either read or write aliases to the object sent.
\end_layout

\begin_layout Standard
\begin_inset listings
inline false
status open

\begin_layout Plain Layout

actor Dataflow
\end_layout

\begin_layout Plain Layout

  be step(list: List iso, flow: Dataflow tag) => ...
\end_layout

\end_inset


\end_layout

\begin_layout Standard
Here, by passing an 
\begin_inset Formula $\mathtt{iso}$
\end_inset

 reference, a 
\begin_inset Formula $\mathtt{Dataflow}$
\end_inset

 actor can mutate the 
\begin_inset Formula $\mathtt{list}$
\end_inset

 before sending it to the 
\begin_inset Formula $\mathtt{flow}$
\end_inset

 actor.
 In order to do this, we must be certain the sending actor does not retain
 a read or write alias.
 To this end we use an 
\emph on
aliasing 
\emph default
type system wherein a newly created alias to an object cannot violate the
 deny properties of the reference being aliased.
 For example, a newly created alias of an 
\begin_inset Formula $\mathtt{iso}$
\end_inset

 reference must be neither readable nor writeable (i.e.
 a 
\begin_inset Formula $\mathtt{tag}$
\end_inset

).
 
\end_layout

\begin_layout Standard
To 
\emph on
move 
\emph default
deny properties, we 
\emph on
consume
\emph default
 a reference or use a 
\emph on
destructive read
\emph default
, both with the expected semantics.
\end_layout

\begin_layout Standard
\begin_inset listings
inline false
status open

\begin_layout Plain Layout

actor Dataflow
\end_layout

\begin_layout Plain Layout

  be step(list: List iso, flow: Dataflow tag) =>
\end_layout

\begin_layout Plain Layout

    flow.step(list, this) // Not allowed
\end_layout

\begin_layout Plain Layout

    flow.step(consume list, this)
\end_layout

\end_inset


\end_layout

\begin_layout Standard
The type system introduces the concept of 
\emph on
unaliased types,
\emph default
 annotated with 
\begin_inset Formula $\circ$
\end_inset

, in order to type
\emph on
 
\emph default
values for which an alias has been removed.
 Here, the 
\begin_inset Formula $\mathtt{consume}$
\end_inset

 produces a 
\begin_inset Formula $\mathtt{List\,iso\circ}$
\end_inset

 which is aliased as a 
\begin_inset Formula $\mathtt{List\,iso}$
\end_inset

 when the behaviour is called.
 The non-destructive read produces a 
\begin_inset Formula $\mathtt{List\,iso}$
\end_inset

 which is aliased as a 
\begin_inset Formula $\mathtt{List\,tag}$
\end_inset

, which is rejected by the type system.
\end_layout

\begin_layout Standard
Aliases which outlive the execution of an expression are treated differently
 from 
\emph on
temporary identifiers
\emph default
, which do not.
 The use of 
\emph on
temporary identifiers
\emph default
, combined with 
\emph on
viewpoint adaptation
\emph default
, allows reading from and writing to isolated objects and isolated fields.
 Earlier work on isolation and external uniqueness systems 
\begin_inset CommandInset citation
LatexCommand cite
key "clarke2003external,gordon2012uniqueness,haller2010capabilities"

\end_inset

 does not provide this.
\end_layout

\begin_layout Standard
\begin_inset listings
inline false
status open

\begin_layout Plain Layout

actor Dataflow
\end_layout

\begin_layout Plain Layout

  be step(list1: List iso, list2: List iso,
\end_layout

\begin_layout Plain Layout

      flow: Dataflow tag) =>
\end_layout

\begin_layout Plain Layout

    list1.next = consume list2
\end_layout

\begin_layout Plain Layout

    flow.step(consume list1)
\end_layout

\end_inset


\end_layout

\begin_layout Standard
Here, we mutate 
\begin_inset Formula $\mathtt{list1}$
\end_inset

 by assigning 
\begin_inset Formula $\mathtt{list2}$
\end_inset

 to its 
\begin_inset Formula $\mathtt{next}$
\end_inset

 field, maintaining isolation for both 
\begin_inset Formula $\mathtt{list1}$
\end_inset

 and 
\begin_inset Formula $\mathtt{list1.next}$
\end_inset

.
 Similarly, we could read from or write to fields of 
\begin_inset Formula $\mathtt{list1.next}$
\end_inset

, since path traversal is allowed.
 This also allows calling methods on isolated references and fields of any
 path depth.
 
\end_layout

\begin_layout Standard
Unsafe reads are prevented by 
\emph on
viewpoint adaptation
\emph default
, and unsafe writes are prevented by 
\emph on
safe-to-write
\emph default
 rules.
 For example:
\end_layout

\begin_layout Standard
\begin_inset listings
inline false
status open

\begin_layout Plain Layout

actor Dataflow
\end_layout

\begin_layout Plain Layout

  fun ref append(list1: List iso,
\end_layout

\begin_layout Plain Layout

      list2: List ref) =>
\end_layout

\begin_layout Plain Layout

    list1.next = list2 // Not allowed
\end_layout

\end_inset


\end_layout

\begin_layout Standard
Even if 
\begin_inset Formula $\mathtt{list1.next}$
\end_inset

 had the type 
\begin_inset Formula $\mathtt{List\,ref}$
\end_inset

, this assignment is rejected.
 As a result, isolated references form 
\emph on
static regions
\emph default
, wherein mutable references reachable by the 
\begin_inset Formula $\mathtt{iso}$
\end_inset

 reference can only be reached via the 
\begin_inset Formula $\mathtt{iso}$
\end_inset

 reference and immutable references reachable by the 
\begin_inset Formula $\mathtt{iso}$
\end_inset

 reference are either globally immutable or can only be reached via the
 
\begin_inset Formula $\mathtt{iso}$
\end_inset

 reference.
\end_layout

\begin_layout Standard
A 
\begin_inset Formula $\mathtt{trn}$
\end_inset

 reference makes a novel guarantee: 
\emph on
write uniqueness
\emph default
 without 
\emph on
read uniqueness
\emph default
.
 By denying global read/write aliases, but only denying local write aliases,
 it allows an object to be written to only via the 
\begin_inset Formula $\mathtt{trn}$
\end_inset

 reference, but read from via other aliases held by the same actor.
 This allows the object to be mutable while still allowing it to 
\emph on
transition 
\emph default
to an immutable reference capability in the future, in order to share it
 with another actor.
\end_layout

\begin_layout Standard
\begin_inset listings
inline false
status open

\begin_layout Plain Layout

class BookingManager
\end_layout

\begin_layout Plain Layout

  var accountant: Accountant
\end_layout

\begin_layout Plain Layout

  var all: Map[Date, Booking box]
\end_layout

\begin_layout Plain Layout

  var future: Map[Date, Booking trn]
\end_layout

\begin_layout Plain Layout

  fun ref close(date: Date) =>
\end_layout

\begin_layout Plain Layout

    accountant.account(future.remove(date))
\end_layout

\begin_layout Plain Layout

\end_layout

\begin_layout Plain Layout

actor Accountant
\end_layout

\begin_layout Plain Layout

  be account(booking: Booking val) => ...
\end_layout

\end_inset


\end_layout

\begin_layout Standard
Here
\begin_inset Foot
status collapsed

\begin_layout Plain Layout
In this example, generic types and default reference capabilities (
\begin_inset Formula $\mathtt{ref}$
\end_inset

 for objects and 
\begin_inset Formula $\mathtt{tag}$
\end_inset

 for actors) are used.
 While the full Pony language supports these, they are not formalised here.
\end_layout

\end_inset

 we use a 
\begin_inset Formula $\mathtt{trn}$
\end_inset

 reference to model bookings that remain mutable until they are closed and
 sent for accounting.
 All bookings are in the 
\begin_inset Formula $\mathtt{all}$
\end_inset

 map, but only mappings that have not been closed out and are still mutable
 are in the 
\begin_inset Formula $\mathtt{future}$
\end_inset

 map.
 When a booking is closed, it is removed from the 
\begin_inset Formula $\mathtt{future}$
\end_inset

 map, returning a 
\begin_inset Formula $\mathtt{Booking\,trn\circ}$
\end_inset

, which is aliased as a 
\begin_inset Formula $\mathtt{Booking\,trn}$
\end_inset

, which is a subtype of 
\begin_inset Formula $\mathtt{Booking\,val}$
\end_inset

 and can be shared with the 
\begin_inset Formula $\mathtt{Accountant}$
\end_inset

 actor.
 Without a 
\emph on
write unique
\emph default
 type, namely 
\begin_inset Formula $\mathtt{trn}$
\end_inset

, this would require copying the 
\begin_inset Formula $\mathtt{Booking}$
\end_inset

.
\end_layout

\begin_layout Standard
A 
\begin_inset Formula $\mathtt{trn}$
\end_inset

 reference also forms a 
\emph on
static region
\emph default
, but with a looser guarantee than an 
\begin_inset Formula $\mathtt{iso}$
\end_inset

 reference.
 Mutable references reachable by the 
\begin_inset Formula $\mathtt{trn}$
\end_inset

 reference can only be reached via the 
\begin_inset Formula $\mathtt{trn}$
\end_inset

 reference, but immutable references, whether global or local, are not contained
 in the resulting 
\emph on
write region
\emph default
.
\end_layout

\begin_layout Section
Type System
\end_layout

\begin_layout Standard
\begin_inset Float figure
wide false
sideways false
status open

\begin_layout Plain Layout
\align center
\begin_inset ERT
status open

\begin_layout Plain Layout


\backslash
makebox[
\backslash
textwidth][c]{
\end_layout

\end_inset


\begin_inset Formula $\begin{array}{ccc}
\dfrac{\mathtt{x}\in\Gamma}{\Gamma\vdash\mathtt{x:}\Gamma(\mathtt{x})\,|\,\Gamma}\;\textrm{\textsc{T-Local}} &  & \dfrac{\Gamma\vdash\mathtt{e:S}\,\kappa\,|\,\Gamma'\quad\mathcal{F}(\mathtt{S,f})=\mathtt{S'}\,\kappa'}{\Gamma\vdash\mathtt{e.f:S'}\,\kappa\triangleright\kappa'\,|\,\Gamma'}\;\textrm{\textsc{T-Fld}}\\
\\
\dfrac{\mathtt{\mathtt{x}\notin\Gamma}}{\Gamma\vdash\mathtt{var\,x:ET}\,|\,\Gamma[\mathtt{x}\mapsto\mathtt{ET}]}\;\textrm{\textsc{T-DeclLocal}} &  & \dfrac{\Gamma\vdash\mathtt{e:ET\,|\,\Gamma'}\quad\Gamma'\vdash\mathtt{e':ET'}\,\Gamma''}{\Gamma\vdash\mathtt{e;e':ET'}\,|\,\Gamma''}\;\textrm{\textsc{T-Seq}}\\
\\
\dfrac{\Gamma(\mathtt{x})=\mathtt{S\,\kappa}\quad\Gamma\vdash_{\mathcal{A}}\mathtt{e:S\,\kappa}\,|\,\Gamma'}{\Gamma\vdash\mathtt{x=e}:\mathcal{U}(\mathtt{S}\,\kappa)\,|\,\Gamma'}\;\textrm{\textsc{T-AsnLocal}} &  & \dfrac{\begin{array}{c}
\Gamma\vdash_{\mathcal{A}}\mathtt{e':S'}\,\kappa'\,|\,\Gamma'\\
\Gamma'\vdash\mathtt{e:S\,\kappa\,|\,\Gamma''}\\
\mathcal{F}(\mathtt{S,f})=\mathtt{S'}\,\kappa''\quad\kappa'\le\kappa''\\
\vdash\kappa\triangleleft\kappa'\vee\vdash\kappa\triangleleft\kappa''
\end{array}}{\Gamma\vdash\mathtt{e.f=e'}:\mathcal{U}(\mathtt{S'}\,\kappa\triangleright\kappa'')\,|\,\Gamma''}\;\textrm{\textsc{T-AsnFld}}\\
\\
\dfrac{\begin{array}{c}
\mathcal{M}(\mathtt{S,m})=\mathtt{(T,\overline{x}:\mathtt{\overline{T}},e,ET)}\\
\Gamma_{0}=\Gamma\quad\Gamma_{\mathtt{i-1}}\vdash_{\mathcal{A}}\mathtt{e_{i}:T{}_{i}}\,|\,\Gamma_{\mathtt{i}}\\
\Gamma_{\mathtt{|\overline{e}|}}\vdash_{\mathcal{A}}\mathtt{e:T}\,|\,\Gamma'
\end{array}}{\Gamma\vdash\mathtt{e.m(\overline{e}):ET}\,|\,\Gamma'}\;\textrm{\textsc{T-Sync}} &  & \dfrac{\begin{array}{c}
\mathcal{M}(\mathtt{A,b})=\mathtt{(A\,ref,\overline{x}:\mathtt{\overline{T}},e,A\,tag)}\\
\Gamma_{0}=\Gamma\quad\Gamma_{\mathtt{i-1}}\vdash_{\mathcal{A}}\mathtt{e_{i}:T{}_{i}}\,|\,\Gamma_{\mathtt{i}}\\
\Gamma_{\mathtt{|\overline{e}|}}\vdash_{\mathcal{A}}\mathtt{e:A\,tag}\,|\,\Gamma'
\end{array}}{\Gamma\vdash\mathtt{e.b(\overline{e}):A\,tag}\,|\,\Gamma'}\;\textrm{\textsc{T-Async}}\\
\\
\dfrac{\begin{array}{c}
\mathcal{M}(\mathtt{C,k})=\mathtt{(C\,ref,\overline{x}:\mathtt{\overline{T}},e,C\,ref\circ)}\\
\Gamma_{0}=\Gamma\quad\Gamma_{\mathtt{i-1}}\vdash_{\mathcal{A}}\mathtt{e_{i}:T{}_{i}}\,|\,\Gamma_{\mathtt{i}}
\end{array}}{\Gamma\vdash\mathtt{C.k(\overline{e}):C\,ref\circ}\,|\,\Gamma_{\mathtt{|\overline{e}|}}}\;\textrm{\textsc{T-Ctor}} &  & \dfrac{\begin{array}{c}
\mathcal{M}(\mathtt{A,k})=\mathtt{(A\,ref,\overline{x}:\mathtt{\overline{T}},e,A\,tag)}\\
\Gamma_{0}=\Gamma\quad\Gamma_{\mathtt{i-1}}\vdash_{\mathcal{A}}\mathtt{e_{i}:T{}_{i}}\,|\,\Gamma_{\mathtt{i}}
\end{array}}{\Gamma\vdash\mathtt{A.k(\overline{e}):A\,tag}\,|\,\Gamma_{\mathtt{|\overline{e}|}}}\;\textrm{\textsc{T-Ator}}\\
\\
\dfrac{\mathtt{x}\in\Gamma}{\Gamma\vdash\mathtt{consume\,x}:\mathcal{U}(\Gamma(\mathtt{x}))\,|\,\Gamma\backslash\{\mathtt{x}\}}\;\textrm{\textsc{T-Consume}} &  & \dfrac{\Gamma\backslash\{\mathtt{x}\,|\,\neg\mathit{Sendable}(\Gamma(\mathtt{x}))\}\vdash\mathtt{e:ET}\,|\,\Gamma'}{\Gamma\vdash\mathtt{recover\,e:}\mathcal{R}(\mathtt{ET})\,|\,\Gamma\cap\Gamma'}\;\textrm{\textsc{T-Rec}}\\
\\
\dfrac{\Gamma\vdash\mathtt{e:ET'}\,|\,\Gamma'\quad\mathcal{A}(\mathtt{ET'})\le\mathtt{T}}{\Gamma\vdash_{\mathcal{A}}\mathtt{e:T}\,|\,\Gamma'}\;\textrm{\textsc{T-Alias}} &  & \dfrac{\Gamma\vdash\mathtt{e:S}\,\kappa\circ\,|\,\Gamma'}{\Gamma\vdash\mathtt{e:S}\,\kappa\,|\,\Gamma'}\;\textrm{\textsc{T-Subsume}}
\end{array}$
\end_inset


\begin_inset ERT
status open

\begin_layout Plain Layout

}
\end_layout

\end_inset


\end_layout

\begin_layout Plain Layout
\begin_inset Caption Standard

\begin_layout Plain Layout
\begin_inset CommandInset label
LatexCommand label
name "fig:Expression-typing"

\end_inset

Expression typing
\end_layout

\end_inset


\end_layout

\end_inset


\end_layout

\begin_layout Standard
\begin_inset Float figure
wide false
sideways false
status open

\begin_layout Plain Layout
\align center
\begin_inset Formula $\begin{array}{c}
\begin{array}{ccccc}
\dfrac{\mathtt{ET\le ET''}\quad\mathtt{ET''\le ET'}}{\mathtt{ET\le ET'}} &  & \dfrac{}{\mathtt{S\,\kappa\circ\le S\,\kappa}} &  & \dfrac{\mathtt{\kappa\le\kappa'}}{\mathtt{S\,\kappa\le S\,\kappa'}}\end{array}\\
\\
\mathit{\mathtt{iso\le trn\le\{ref,val\}\le box\le tag}}\\
\\
\mathit{Sendable}(\mathtt{T})\,\mathit{iff}\,\mathtt{T=S\,\kappa\wedge\kappa\in\{iso,val,tag\}}
\end{array}$
\end_inset


\end_layout

\begin_layout Plain Layout
\begin_inset Caption Standard

\begin_layout Plain Layout
\begin_inset CommandInset label
LatexCommand label
name "fig:Sub-types"

\end_inset


\begin_inset CommandInset label
LatexCommand label
name "fig:Sendable-types."

\end_inset

Sub-types and auxiliary type definitions
\end_layout

\end_inset


\end_layout

\end_inset


\end_layout

\begin_layout Standard
The type system has the format 
\begin_inset Formula $\Gamma\vdash\mathtt{e:ET}\,|\,\Gamma'$
\end_inset

 and is defined in figure 
\begin_inset CommandInset ref
LatexCommand ref
reference "fig:Expression-typing"

\end_inset

.
 A new environment is generated in order to allow local variable declaration
 and 
\begin_inset Formula $\mathtt{consume}$
\end_inset

 to be simply expressed.
\end_layout

\begin_layout Standard
Because this simplified type system does not formalise traits, interfaces,
 type expressions, or generic types, the 
\noun on
T-Subsume 
\noun default
rule and the subtyping rules account only for reference capabilities.
\end_layout

\begin_layout Section
Well-Formedness
\end_layout

\begin_layout Standard
\begin_inset Float figure
wide false
sideways false
status open

\begin_layout Plain Layout
\align center
\begin_inset Formula $\begin{array}{c}
\dfrac{\mathtt{\forall S\in P.\vdash S\diamond}}{\vdash\mathtt{P}\diamond}\;\textrm{\textsc{WF-Program}}\\
\\
\dfrac{\begin{array}{c}
\mathcal{P}(\mathtt{S})=\mathtt{\overline{F}\,\overline{K}\,\overline{M}\,\overline{B}}\\
\forall\mathtt{var\,f:S\,\kappa}\in\mathtt{\overline{F}}.\vdash\mathtt{S}\diamond\quad\forall\mathtt{K}\in\mathtt{\overline{K}}.\mathtt{S}\vdash\mathtt{K}\diamond\\
\forall\mathtt{M}\in\mathtt{\overline{M}}.\mathtt{S}\vdash\mathtt{M}\diamond\quad\forall\mathtt{B}\in\mathtt{\overline{B}}.\mathtt{S}\vdash\mathtt{B}\diamond
\end{array}}{\vdash\mathtt{S}\diamond}\;\textrm{\textsc{WF-Type}}\\
\\
\dfrac{[\mathtt{this\mapsto C\,var,\overline{x}\mapsto\overline{T}]}\vdash\mathtt{e:C\,ref\circ}}{\mathtt{C}\vdash\mathtt{new\,k(\overline{x}:\overline{T})\Rightarrow e}\diamond}\;\textrm{\textsc{WF-Ctor}}\\
\\
\dfrac{[\mathtt{this\mapsto S\kappa_{r},\overline{x}\mapsto\overline{T}]}\vdash\mathtt{e:ET}}{\mathtt{S}\vdash\mathtt{fun\,\kappa\,m(\overline{x}:\overline{T}):ET\Rightarrow e}\diamond}\;\textrm{\textsc{WF-Sync}}\\
\\
\dfrac{\begin{array}{c}
Sendable(\mathtt{T_{i}})\\
\mathtt{[this\mapsto A\,var,\overline{x}\mapsto\overline{T}]}\vdash\mathtt{e:A\,tag}
\end{array}}{\mathtt{A}\vdash\mathtt{new\,k(\overline{x}:\overline{T})\Rightarrow e}\diamond}\;\textrm{\textsc{WF-Ator}}\\
\\
\dfrac{\begin{array}{c}
Sendable(\mathtt{T_{i}})\\
\mathtt{[this\mapsto A\,var,\overline{x}\mapsto\overline{T}]}\vdash\mathtt{e:A\,tag}
\end{array}}{\mathtt{A}\vdash\mathtt{be\,b(\overline{x}:\overline{T})\Rightarrow e}\diamond}\;\textrm{\textsc{WF-Async}}
\end{array}$
\end_inset


\end_layout

\begin_layout Plain Layout
\begin_inset Caption Standard

\begin_layout Plain Layout
\begin_inset CommandInset label
LatexCommand label
name "fig:Well-formed-programs"

\end_inset

Well-formed programs
\end_layout

\end_inset


\end_layout

\end_inset


\end_layout

\begin_layout Standard
\begin_inset Float figure
wide false
sideways false
status open

\begin_layout Itemize
\begin_inset Formula $\mathtt{z}\in\varphi$
\end_inset

 iff 
\begin_inset Formula $\mathtt{z}\in dom(\varphi\downarrow_{2})$
\end_inset


\end_layout

\begin_layout Itemize
\begin_inset Formula $\alpha\in\chi$
\end_inset

 iff 
\begin_inset Formula $\alpha\in\mathit{dom}(\chi)$
\end_inset


\end_layout

\begin_layout Itemize
\begin_inset Formula $\Delta\vdash\alpha\in\chi$
\end_inset

 iff 
\begin_inset Formula $\alpha\in\mathit{dom}(\chi)$
\end_inset


\end_layout

\begin_layout Itemize
\begin_inset Formula $\Delta\vdash\iota\in\chi$
\end_inset

 iff 
\begin_inset Formula $\exists\iota'$
\end_inset

 such that 
\begin_inset Formula $\Delta\vdash\iota'\in\chi$
\end_inset

 and 
\begin_inset Formula $\Delta,\chi,\iota'\vdash\iota:\_$
\end_inset


\end_layout

\begin_layout Itemize
\begin_inset Formula $\mathcal{M}(\varphi,\chi)=\mathcal{M}(\chi(\varphi(\mathtt{this})\downarrow_{1},\varphi\downarrow_{1})$
\end_inset


\end_layout

\begin_layout Plain Layout
\begin_inset Caption Standard

\begin_layout Plain Layout
Auxiliary well-formedness definitions
\end_layout

\end_inset


\end_layout

\end_inset


\end_layout

\begin_layout Standard
The rules for a well-formed program are presented in figure 
\begin_inset CommandInset ref
LatexCommand ref
reference "fig:Well-formed-programs"

\end_inset

.
 The 
\noun on
WF-Program
\noun default
 rule indicates a program is well-formed if all types in the program are
 well-formed.
 The 
\noun on
WF-Type 
\noun default
rule indicates that a type is well-formed if the types of all of its fields
 are well-formed, its constructors are well-formed, and its synchronous
 and asynchronous methods are well-formed.
 The 
\noun on
WF-Ctor, WF-Sync, 
\noun default
and 
\noun on
WF-Async
\noun default
 rules indicate that a method is well-formed when the body of the method
 in results in a subtype of the return type of the method.
 Additionally, 
\noun on
WF-Async
\noun default
 requires that behaviour parameters are 
\begin_inset Formula $\mathit{Sendable}$
\end_inset

.
 The body of the method is evaluated using an environment composed of the
 receiver and the method parameters, each mapped to their type, as shown
 in figure 
\begin_inset CommandInset ref
LatexCommand ref
reference "fig:Expression-typing"

\end_inset

.
\end_layout

\begin_layout Subsection
Constructor Reference Capabilities
\end_layout

\begin_layout Standard
The reference capability of the receiver and the return type can vary for
 synchronous methods, but not for constructors or asynchronous methods.
 Constructors always operate on a 
\begin_inset Formula $\mathtt{ref}$
\end_inset

 receiver, since the constructor must write to the new object's fields,
 and return a 
\begin_inset Formula $\mathtt{ref\circ}$
\end_inset

 result, since the new object is initially mutable but also unaliased, as
 the constructor's reference to the receiver (
\begin_inset Formula $\mathtt{this}$
\end_inset

) is discarded when the constructor returns.
 This allows a constructor that is passed only sendable references as parameters
 to be embedded in a 
\begin_inset Formula $\mathtt{recover}$
\end_inset

 expression, which allows constructing an object with any reference capability.
 
\end_layout

\begin_layout Standard
In the full language, a class constructor may specify an alternate reference
 capability for the constructed object.
\end_layout

\begin_layout Subsection
Behaviour Reference Capabilities
\end_layout

\begin_layout Standard
Asynchronous methods always operate on a 
\begin_inset Formula $\mathtt{ref}$
\end_inset

 receiver.
 This is because the receiver of an asynchronous method is always an actor;
 when the body is executed, a new stack with the receiver as the root actor
 is created.
 Since each actor executes the body of a single behaviour (or asynchronous
 constructor) at any given time, every behaviour body can read from and
 write to the receiver.
 
\end_layout

\begin_layout Standard
Since an asynchronous method cannot, by definition, perform any operations
 at the call site to construct a return value before returning, the receiver
 is returned to allow chaining method calls.
 For the same reason, a behaviour can be called on a 
\begin_inset Formula $\mathtt{tag}$
\end_inset

 actor (i.e.
 an actor of any reference capability).
\end_layout

\begin_layout Section
Viewpoint Adaptation
\end_layout

\begin_layout Standard
\begin_inset Float table
wide false
sideways false
status open

\begin_layout Plain Layout
\align center
\begin_inset Tabular
<lyxtabular version="3" rows="8" columns="7">
<features booktabs="true" tabularvalignment="middle">
<column alignment="center" valignment="top">
<column alignment="center" valignment="top">
<column alignment="center" valignment="top">
<column alignment="center" valignment="top">
<column alignment="center" valignment="top">
<column alignment="center" valignment="top">
<column alignment="center" valignment="top">
<row>
<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
\begin_inset Formula $\kappa\triangleright\kappa'$
\end_inset


\end_layout

\end_inset
</cell>
<cell multicolumn="1" alignment="center" valignment="top" topline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
\begin_inset Formula $\kappa'$
\end_inset


\end_layout

\end_inset
</cell>
<cell multicolumn="2" alignment="center" valignment="top" topline="true" leftline="true" rightline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\end_layout

\end_inset
</cell>
<cell multicolumn="2" alignment="center" valignment="top" topline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\end_layout

\end_inset
</cell>
<cell multicolumn="2" alignment="center" valignment="top" topline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\end_layout

\end_inset
</cell>
<cell multicolumn="2" alignment="center" valignment="top" topline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\end_layout

\end_inset
</cell>
<cell multicolumn="2" alignment="center" valignment="top" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\end_layout

\end_inset
</cell>
</row>
<row>
<cell alignment="center" valignment="top" topline="true" bottomline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
\begin_inset Formula $\kappa$
\end_inset


\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" bottomline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
iso
\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" bottomline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
trn
\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" bottomline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
ref
\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" bottomline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
val
\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" bottomline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
box
\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" bottomline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
tag
\end_layout

\end_inset
</cell>
</row>
<row>
<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
iso
\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
iso
\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" leftline="true" rightline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
tag
\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
tag
\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
val
\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
tag
\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
tag
\end_layout

\end_inset
</cell>
</row>
<row>
<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
trn
\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
iso
\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" leftline="true" rightline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
trn
\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
box
\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
val
\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
box
\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
tag
\end_layout

\end_inset
</cell>
</row>
<row>
<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
ref
\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
iso
\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" leftline="true" rightline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
trn
\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
ref
\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
val
\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
box
\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
tag
\end_layout

\end_inset
</cell>
</row>
<row>
<cell alignment="center" valignment="top" topline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
val
\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
val
\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
val
\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
val
\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
val
\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
val
\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
tag
\end_layout

\end_inset
</cell>
</row>
<row>
<cell alignment="center" valignment="top" topline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
box
\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
tag
\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
box
\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
box
\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
val
\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
box
\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
tag
\end_layout

\end_inset
</cell>
</row>
<row>
<cell alignment="center" valignment="top" topline="true" bottomline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
tag
\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" bottomline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
\begin_inset Formula $\bot$
\end_inset


\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" bottomline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
\begin_inset Formula $\bot$
\end_inset


\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" bottomline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
\begin_inset Formula $\bot$
\end_inset


\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" bottomline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
\begin_inset Formula $\bot$
\end_inset


\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" bottomline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
\begin_inset Formula $\bot$
\end_inset


\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" bottomline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
\begin_inset Formula $\bot$
\end_inset


\end_layout

\end_inset
</cell>
</row>
</lyxtabular>

\end_inset


\end_layout

\begin_layout Plain Layout
\begin_inset Caption Standard

\begin_layout Plain Layout
\begin_inset CommandInset label
LatexCommand label
name "tab:Viewpoint-adaptation"

\end_inset

Viewpoint adaptation.
 Given an object reference of capability 
\begin_inset Formula $\kappa$
\end_inset

 with a field of capability 
\begin_inset Formula $\kappa'$
\end_inset

, reading the field via that reference produces a reference of capability
 
\begin_inset Formula $\kappa\triangleright\kappa'$
\end_inset

.
\end_layout

\end_inset


\end_layout

\end_inset


\end_layout

\begin_layout Standard
\begin_inset Float table
wide false
sideways false
status open

\begin_layout Plain Layout
\align center
\begin_inset Tabular
<lyxtabular version="3" rows="8" columns="7">
<features booktabs="true" tabularvalignment="middle">
<column alignment="center" valignment="top">
<column alignment="center" valignment="top">
<column alignment="center" valignment="top">
<column alignment="center" valignment="top">
<column alignment="center" valignment="top">
<column alignment="center" valignment="top">
<column alignment="center" valignment="top">
<row>
<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
\begin_inset Formula $\kappa\triangleleft\kappa'$
\end_inset


\end_layout

\end_inset
</cell>
<cell multicolumn="1" alignment="center" valignment="top" topline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
\begin_inset Formula $\kappa'$
\end_inset


\end_layout

\end_inset
</cell>
<cell multicolumn="2" alignment="center" valignment="top" topline="true" leftline="true" rightline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\end_layout

\end_inset
</cell>
<cell multicolumn="2" alignment="center" valignment="top" topline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\end_layout

\end_inset
</cell>
<cell multicolumn="2" alignment="center" valignment="top" topline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\end_layout

\end_inset
</cell>
<cell multicolumn="2" alignment="center" valignment="top" topline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\end_layout

\end_inset
</cell>
<cell multicolumn="2" alignment="center" valignment="top" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\end_layout

\end_inset
</cell>
</row>
<row>
<cell alignment="center" valignment="top" topline="true" bottomline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
\begin_inset Formula $\kappa$
\end_inset


\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" bottomline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
iso
\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" bottomline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
trn
\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" bottomline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
ref
\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" bottomline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
val
\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" bottomline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
box
\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" bottomline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
tag
\end_layout

\end_inset
</cell>
</row>
<row>
<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
iso
\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
\begin_inset Formula $\surd$
\end_inset


\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" leftline="true" rightline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
\begin_inset Formula $\surd$
\end_inset


\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
\begin_inset Formula $\surd$
\end_inset


\end_layout

\end_inset
</cell>
</row>
<row>
<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
trn
\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
\begin_inset Formula $\surd$
\end_inset


\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" leftline="true" rightline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
\begin_inset Formula $\surd$
\end_inset


\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
\begin_inset Formula $\surd$
\end_inset


\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
\begin_inset Formula $\surd$
\end_inset


\end_layout

\end_inset
</cell>
</row>
<row>
<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
ref
\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
\begin_inset Formula $\surd$
\end_inset


\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" leftline="true" rightline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
\begin_inset Formula $\surd$
\end_inset


\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
\begin_inset Formula $\surd$
\end_inset


\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
\begin_inset Formula $\surd$
\end_inset


\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
\begin_inset Formula $\surd$
\end_inset


\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
\begin_inset Formula $\surd$
\end_inset


\end_layout

\end_inset
</cell>
</row>
<row>
<cell alignment="center" valignment="top" topline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
val
\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\end_layout

\end_inset
</cell>
</row>
<row>
<cell alignment="center" valignment="top" topline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
box
\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\end_layout

\end_inset
</cell>
</row>
<row>
<cell alignment="center" valignment="top" topline="true" bottomline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
tag
\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" bottomline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" bottomline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" bottomline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" bottomline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" bottomline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" bottomline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\end_layout

\end_inset
</cell>
</row>
</lyxtabular>

\end_inset


\end_layout

\begin_layout Plain Layout
\begin_inset Caption Standard

\begin_layout Plain Layout
\begin_inset CommandInset label
LatexCommand label
name "tab:Safe-to-write,"

\end_inset

Safe to write.
 Given an object reference of capability 
\begin_inset Formula $\kappa$
\end_inset

, the relation 
\begin_inset Formula $\kappa\triangleleft\kappa'$
\end_inset

 expresses which reference capabilities 
\begin_inset Formula $\kappa'$
\end_inset

 are safe to store into a field of an object via that reference.
\end_layout

\end_inset


\end_layout

\end_inset


\end_layout

\begin_layout Standard
When reading a field 
\family typewriter

\begin_inset Formula $\mathtt{f}$
\end_inset


\family default
 from an object 
\begin_inset Formula $\mathtt{\iota}$
\end_inset

 we obtain a temporary identifier.
 The reference capability of this temporary identifier must be a combination
 of 
\begin_inset Formula $\kappa$
\end_inset

, the reference capability of the path leading to 
\begin_inset Formula $\iota$
\end_inset

, and 
\begin_inset Formula $\kappa'$
\end_inset

, the reference capability with which 
\begin_inset Formula $\iota$
\end_inset

 sees the field.
 This is expressed through the operator 
\begin_inset Formula $\triangleright$
\end_inset

, defined in table 
\begin_inset CommandInset ref
LatexCommand ref
reference "tab:Viewpoint-adaptation"

\end_inset

.
 When reading a field through an origin, the result must not violate the
 deny properties of either the origin or the field.
 For example, reading a 
\begin_inset Formula $\mathtt{ref}$
\end_inset

 field from an 
\begin_inset Formula $\mathtt{iso}$
\end_inset

 reference returns 
\begin_inset Formula $\mathtt{tag}$
\end_inset

 — thus we do not violate the deny properties of the origin or the field
 itself.
\end_layout

\begin_layout Standard
Storing a reference into a field of an object 
\begin_inset Formula $\iota$
\end_inset

 is legal if the type of the reference is both a subtype of the type of
 the field and also 
\emph on
safe to write
\emph default
 into the origin.
 The relation 
\begin_inset Formula $\kappa\triangleleft\kappa'$
\end_inset

, as defined in table  
\begin_inset CommandInset ref
LatexCommand ref
reference "tab:Safe-to-write,"

\end_inset

, expresses which reference capabilities 
\begin_inset Formula $\kappa'$
\end_inset

 are safe to write into origin 
\begin_inset Formula $\kappa$
\end_inset

.
 When writing to a field through an origin, no alias of the object being
 written may exist that would violate the deny properties of the origin.
 Therefore, all entries for 
\begin_inset Formula $\mathtt{val}$
\end_inset

, 
\begin_inset Formula $\mathtt{box}$
\end_inset

 and 
\begin_inset Formula $\mathtt{tag}$
\end_inset

 are empty.
 Moreover, only 
\begin_inset Formula $\mathtt{iso}$
\end_inset

, 
\begin_inset Formula $\mathtt{val}$
\end_inset

 or 
\begin_inset Formula $\mathtt{tag}$
\end_inset

 references may be stored into an 
\begin_inset Formula $\mathtt{iso}$
\end_inset

 origin; all other writes would violate the region introduced by the 
\begin_inset Formula $\mathtt{iso}$
\end_inset

 origin.
\end_layout

\begin_layout Section
Reference Capability Recovery
\end_layout

\begin_layout Standard
The evaluation of an expression which has access only to sendable variables
 (i.e.
 
\family typewriter

\begin_inset Formula $\mathtt{iso}$
\end_inset


\family default
, 
\begin_inset Formula $\mathtt{val}$
\end_inset

, and 
\begin_inset Formula $\mathtt{tag}$
\end_inset

) can return a sendable type, even if the result of the expression would
 otherwise not be sendable.
 This is an extension of previous work on 
\emph on
recovery
\emph default
 
\begin_inset CommandInset citation
LatexCommand cite
key "gordon2012uniqueness"

\end_inset

, which is related to work on 
\emph on
borrowing
\emph default
 
\begin_inset CommandInset citation
LatexCommand cite
key "haller2010capabilities"

\end_inset

.
 Such expressions are introduced using the 
\begin_inset Formula $\mathtt{recover}$
\end_inset

 keyword (
\noun on
T-Rec
\noun default
).
 The return type of 
\begin_inset Formula $\mathtt{recover\,e}$
\end_inset

 is the sendable version of the return type of 
\begin_inset Formula $\mathtt{e}$
\end_inset

.
 For example, if 
\begin_inset Formula $\mathtt{e}$
\end_inset

 has type 
\begin_inset Formula $\mathtt{ref}$
\end_inset

, then 
\begin_inset Formula $\mathtt{recover\,e}$
\end_inset

 has type 
\begin_inset Formula $\mathtt{iso}$
\end_inset

, and if 
\begin_inset Formula $\mathtt{e}$
\end_inset

 has type 
\begin_inset Formula $\mathtt{ref\circ}$
\end_inset

, then 
\begin_inset Formula $\mathtt{recover\,e}$
\end_inset

 has type 
\begin_inset Formula $\mathtt{iso\circ}$
\end_inset

.
\end_layout

\begin_layout Definition
Reference capability recovery
\end_layout

\begin_layout Definition
\begin_inset Formula $\mathcal{R}(\mathtt{S}\,\kappa\,\phi)=\begin{cases}
\mathtt{S\,iso\,\phi} & \mathit{iff}\,\kappa\in\mathtt{\{iso,trn,ref\}}\\
\mathtt{S\,val} & \mathit{iff}\,\kappa\in\mathtt{\{val,box\}}\\
\mathtt{S\,tag} & \mathit{otherwise}
\end{cases}$
\end_inset


\end_layout

\begin_layout Standard
\begin_inset Formula $\mathcal{R}(\mathtt{ET})$
\end_inset

 is the sendable reference capability that retains the same local read and/or
 write guarantee.
 In other words, a writeable reference capability can become 
\begin_inset Formula $\mathtt{iso}$
\end_inset

 and a readable reference capability can become 
\family typewriter

\begin_inset Formula $\mathtt{val}$
\end_inset


\family default
.
 In Pony, explicit 
\begin_inset Formula $\mathtt{recover}$
\end_inset

 expressions are used along with implicit recovery detected by the compiler.
\end_layout

\begin_layout Section
Treatment of Actors
\end_layout

\begin_layout Standard
Actors introduce the question of who may read or update the actor’s fields,
 the possibility of synchronous calls on actors, and the type required for
 asynchronous calls.
\end_layout

\begin_layout Standard
Field read and write requires that the actor should see itself as a 
\begin_inset Formula $\mathtt{ref}$
\end_inset

.
 As a result, any other actor will see it as 
\begin_inset Formula $\mathtt{tag}$
\end_inset

.
 Therefore no other actor except the current one will be allowed to observe
 an actor’s fields — a nice consequence of the type system.
\end_layout

\begin_layout Standard
By a similar argument, because the actor sees itself as 
\begin_inset Formula $\mathtt{ref}$
\end_inset

, any other paths that point to it will do so as 
\begin_inset Formula $\mathtt{box}$
\end_inset

, 
\begin_inset Formula $\mathtt{ref}$
\end_inset

, or 
\begin_inset Formula $\mathtt{tag}$
\end_inset

, and this means that the actor may call synchronous methods on itself,
 provided that the receiver reference capability of the method declaration
 is 
\begin_inset Formula $\mathtt{ref}$
\end_inset

, 
\begin_inset Formula $\mathtt{box}$
\end_inset

, or 
\begin_inset Formula $\mathtt{tag}$
\end_inset

.
 Interestingly, for asynchronous (behaviour) calls, the receiving actor
 only needs to be seen as a 
\begin_inset Formula $\mathtt{tag}$
\end_inset

, even though the receiver reference capability in the behaviour is 
\begin_inset Formula $\mathtt{ref}$
\end_inset

.
 This is in contrast to method calls, where the receiving object or actor
 has to be seen as a reference capability which is a subtype of the receiver
 reference capability in the method declaration.
 The looser requirement for actors is sound, because, as discussed above,
 no other actor may obtain access to the actor’s state.
\end_layout

\begin_layout Section
Aliasing and Unaliasing
\end_layout

\begin_layout Standard
Assignment operations discard aliases, as they return the previous value
 of the left-hand side (
\noun on
AsnLocal
\noun default
 and 
\noun on
AsnField
\noun default
) after overwriting it.
 The fact that an alias has been discarded is important in the cases where
 the reference capability is unique (
\begin_inset Formula $\mathtt{iso}$
\end_inset

 or 
\begin_inset Formula $\mathtt{trn}$
\end_inset

).
 This is indicated through the unaliased annotation 
\begin_inset Formula $\circ$
\end_inset

, which expresses that there is no stable path to the corresponding object.
\end_layout

\begin_layout Standard
Because unaliasing is of importance only when the underlying reference capabilit
y is 
\begin_inset Formula $\mathtt{iso}$
\end_inset

, 
\begin_inset Formula $\mathtt{trn}$
\end_inset

 or 
\begin_inset Formula $\mathtt{ref}$
\end_inset

, the unaliasing operation 
\begin_inset Formula $\mathcal{U}$
\end_inset

 is defined, which takes a type and returns an extended type, as seen in
 definition 
\begin_inset CommandInset ref
LatexCommand ref
reference "def:Aliasing-and-unaliasing."

\end_inset

.
 This operator is used whenever an alias is discarded, for example in the
 type system rules 
\noun on
T-AsnLocal
\noun default
 and 
\noun on
T-AsnFld
\noun default
.
 Object constructors also introduce unaliased values, as indicated in the
 type system rule 
\noun on
T-Ctor
\noun default
.
\end_layout

\begin_layout Standard
Some operations introduce stable aliases (e.g.
 assignment), while others introduce only unstable ones (e.g.
 field read).
 The distinction is expressed in the type system through the difference
 between the type judgments 
\begin_inset Formula $\Gamma\vdash\mathtt{e:ET}$
\end_inset

 and the 
\emph on
aliased
\emph default
 type judgment 
\begin_inset Formula $\Gamma\vdash_{{\cal A}}\mathtt{e:ET}$
\end_inset

.
 For example, when assigning an expression 
\begin_inset Formula $\mathtt{e}$
\end_inset

 to a variable 
\begin_inset Formula $\mathtt{x}$
\end_inset

, the right-hand side is typed in the judgment 
\begin_inset Formula $\vdash_{\mathcal{A}}$
\end_inset

 (cf.
 
\noun on
T-AsnLocal
\noun default
).
 The aliasing judgement is also applied to the receiver and arguments of
 method calls and asynchronous behaviours (
\noun on
T-Sync
\noun default
 and 
\noun on
T-Async
\noun default
), the arguments to object and actor constructors (
\noun on
T-Ctor
\noun default
 and 
\noun on
T-Ator
\noun default
), and the right-hand side of a field assignment (
\noun on
T-AsnFld
\noun default
).
\end_layout

\begin_layout Standard
The aliased type judgment 
\begin_inset Formula $\Gamma\vdash_{{\cal A}}\mathtt{e:ET}$
\end_inset

 is defined in terms of the unaliased type judgment 
\begin_inset Formula $\Gamma\vdash\mathtt{e:ET'}$
\end_inset

, where 
\begin_inset Formula $\mathtt{ET}$
\end_inset

 has to be a super-type of the aliased version of 
\begin_inset Formula $\mathtt{ET'}$
\end_inset

, i.e.
 
\begin_inset Formula ${\cal A}(\mathtt{ET'})\le\mathtt{ET}$
\end_inset

.
 The operation 
\begin_inset Formula ${\cal A}(\mathtt{ET})$
\end_inset

 gives the type that an alias of 
\begin_inset Formula $\mathtt{ET}$
\end_inset

 would have.
 When aliasing an unaliased type there is no previous alias to consider,
 and therefore 
\begin_inset Formula ${\cal A}(\mathtt{S}\,\kappa\circ)=\mathtt{S}\,\kappa$
\end_inset

.
 For other types, the result must be the minimal super-type of the underlying
 type which is locally compatible with it, i.e.
 
\begin_inset Formula $\mathcal{A}(\mathtt{S}\,\kappa)=\mathtt{S}\,\kappa'$
\end_inset

 where 
\begin_inset Formula $\kappa'\le\mathcal{A}(\kappa')$
\end_inset

 and 
\begin_inset Formula $\mathcal{A}(\kappa')$
\end_inset

 does not locally deny 
\begin_inset Formula $\kappa'$
\end_inset

.
\end_layout

\begin_layout Definition
\begin_inset CommandInset label
LatexCommand label
name "def:Aliasing-and-unaliasing."

\end_inset

Aliasing and unaliasing.
\begin_inset Separator latexpar
\end_inset


\end_layout

\begin_deeper
\begin_layout Itemize
\begin_inset Formula $\mathcal{A}(\mathtt{S}\,\mathtt{\kappa}\circ)=\mathtt{S}\,\kappa$
\end_inset


\end_layout

\begin_layout Itemize
\begin_inset Formula $\mathcal{A}(\mathtt{S}\,\kappa)=\begin{cases}
\mathtt{\mathtt{S}\,tag} & \mathit{iff}\,\kappa=\mathtt{iso}\\
\mathtt{\mathtt{S}\,box} & \mathit{iff}\,\kappa=\mathtt{trn}\\
\mathtt{S}\,\kappa & \mathit{otherwise}
\end{cases}$
\end_inset


\end_layout

\begin_layout Itemize
\begin_inset Formula $\mathcal{U}(\mathtt{S}\,\kappa)=\begin{cases}
\mathtt{\mathtt{S}}\,\kappa\circ & \mathit{iff}\,\kappa\in\mathtt{\{iso,trn,ref\}}\\
\mathtt{S}\,\kappa & \mathit{otherwise}
\end{cases}$
\end_inset


\end_layout

\end_deeper
\begin_layout Standard
Thus, through a combination of aliasing and unaliasing, the programmer can
 obtain unique types when needed.
 For example, for 
\begin_inset Formula $\mathtt{x}$
\end_inset

 and 
\begin_inset Formula $\mathtt{y}$
\end_inset

 of type 
\begin_inset Formula $\mathtt{C\,trn}$
\end_inset

, the assignment 
\begin_inset Formula $\mathtt{x=y}$
\end_inset

 is illegal, because the aliased type of 
\begin_inset Formula $\mathtt{y}$
\end_inset

 is 
\begin_inset Formula $\mathtt{C\,box}$
\end_inset

 and 
\begin_inset Formula $\mathtt{C\,box}\not\le\mathtt{C\,trn}$
\end_inset

.
 However, the assignment 
\begin_inset Formula $\mathtt{x=consume\,y}$
\end_inset

 is legal, because the type of 
\begin_inset Formula $\mathtt{consume\,y}$
\end_inset

 is 
\begin_inset Formula $\mathtt{C\,trn\circ}$
\end_inset

, and the alias of 
\begin_inset Formula $\mathtt{C\,trn\circ}$
\end_inset

 is 
\begin_inset Formula $\mathtt{C\,trn}$
\end_inset

.
\end_layout

\begin_layout Section
\begin_inset CommandInset label
LatexCommand label
name "sec:Consistent-heap-visibility"

\end_inset

Consistent heap visibility
\end_layout

\begin_layout Standard
The core of the soundness of this approach is 
\emph on
consistent heap visibility
\emph default
, which requires that aliasing in the heap must satisfy all the deny properties
 specified by the capabilities attached to fields and variables.
 This leads to the notions of local and global compatibility.
 Namely, two capabilities are 
\emph on
locally compatible
\emph default
 
\begin_inset Formula $\kappa\sim_{\ell}\kappa'$
\end_inset

 if neither has a local deny property that prevents the existence of the
 other.
 Similarly, they are 
\emph on
globally compatible
\emph default
, 
\begin_inset Formula $\kappa\sim_{g}\kappa'$
\end_inset

, if neither has a global deny property that prevents the existence of the
 other.
 These relationships are defined in table 
\begin_inset CommandInset ref
LatexCommand ref
reference "tab:Compatible-capabilities-2"

\end_inset

, e.g.
 
\begin_inset Formula $\mathtt{ref\sim_{\ell}ref}$
\end_inset

 but 
\begin_inset Formula $\mathtt{ref}\not\sim_{g}\mathtt{ref}$
\end_inset

.
 Both relations are symmetric.
 It is interesting to note that global compatibility is a subset of local
 compatibility.
\end_layout

\begin_layout Standard
\begin_inset Float table
wide false
sideways false
status open

\begin_layout Plain Layout
\align center
\begin_inset Tabular
<lyxtabular version="3" rows="8" columns="7">
<features booktabs="true" tabularvalignment="middle">
<column alignment="center" valignment="top">
<column alignment="center" valignment="top">
<column alignment="center" valignment="top">
<column alignment="center" valignment="top">
<column alignment="center" valignment="top">
<column alignment="center" valignment="top">
<column alignment="center" valignment="top">
<row>
<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
\begin_inset Formula $\kappa\sim\kappa'$
\end_inset


\end_layout

\end_inset
</cell>
<cell multicolumn="1" alignment="center" valignment="top" topline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
\begin_inset Formula $\kappa'$
\end_inset


\end_layout

\end_inset
</cell>
<cell multicolumn="2" alignment="center" valignment="top" topline="true" leftline="true" rightline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\end_layout

\end_inset
</cell>
<cell multicolumn="2" alignment="center" valignment="top" topline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\end_layout

\end_inset
</cell>
<cell multicolumn="2" alignment="center" valignment="top" topline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\end_layout

\end_inset
</cell>
<cell multicolumn="2" alignment="center" valignment="top" topline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\end_layout

\end_inset
</cell>
<cell multicolumn="2" alignment="center" valignment="top" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\end_layout

\end_inset
</cell>
</row>
<row>
<cell alignment="center" valignment="top" topline="true" bottomline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
\begin_inset Formula $\kappa$
\end_inset


\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" bottomline="true" leftline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
iso
\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" bottomline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
trn
\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" bottomline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
ref
\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" bottomline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
val
\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" bottomline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
box
\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" bottomline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
tag
\end_layout

\end_inset
</cell>
</row>
<row>
<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
iso
\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" leftline="true" rightline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
\begin_inset Formula $\ell,g$
\end_inset


\end_layout

\end_inset
</cell>
</row>
<row>
<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
trn
\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" leftline="true" rightline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
\begin_inset Formula $\ell$
\end_inset


\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
\begin_inset Formula $\ell,g$
\end_inset


\end_layout

\end_inset
</cell>
</row>
<row>
<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
ref
\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" leftline="true" rightline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
\begin_inset Formula $\ell$
\end_inset


\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
\begin_inset Formula $\ell$
\end_inset


\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
\begin_inset Formula $\ell,g$
\end_inset


\end_layout

\end_inset
</cell>
</row>
<row>
<cell alignment="center" valignment="top" topline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
val
\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
\begin_inset Formula $\ell,g$
\end_inset


\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
\begin_inset Formula $\ell,g$
\end_inset


\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
\begin_inset Formula $\ell,g$
\end_inset


\end_layout

\end_inset
</cell>
</row>
<row>
<cell alignment="center" valignment="top" topline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
box
\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
\begin_inset Formula $\ell$
\end_inset


\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
\begin_inset Formula $\ell$
\end_inset


\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
\begin_inset Formula $\ell,g$
\end_inset


\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
\begin_inset Formula $\ell,g$
\end_inset


\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
\begin_inset Formula $\ell,g$
\end_inset


\end_layout

\end_inset
</cell>
</row>
<row>
<cell alignment="center" valignment="top" topline="true" bottomline="true" leftline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
tag
\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" bottomline="true" leftline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
\begin_inset Formula $\ell,g$
\end_inset


\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" bottomline="true" leftline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
\begin_inset Formula $\ell,g$
\end_inset


\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" bottomline="true" leftline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
\begin_inset Formula $\ell,g$
\end_inset


\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" bottomline="true" leftline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
\begin_inset Formula $\ell,g$
\end_inset


\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" bottomline="true" leftline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
\begin_inset Formula $\ell,g$
\end_inset


\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" bottomline="true" leftline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
\begin_inset Formula $\ell,g$
\end_inset


\end_layout

\end_inset
</cell>
</row>
</lyxtabular>

\end_inset


\end_layout

\begin_layout Plain Layout
\begin_inset Caption Standard

\begin_layout Plain Layout
\begin_inset CommandInset label
LatexCommand label
name "tab:Compatible-capabilities-2"

\end_inset

Compatible capabilities.
\end_layout

\end_inset


\end_layout

\end_inset


\end_layout

\begin_layout Standard
\begin_inset Float figure
wide false
sideways false
status open

\begin_layout Plain Layout
\align center
\begin_inset Graphics
	filename graphics/fast-cheap-runtime.png
	width 90col%

\end_inset


\end_layout

\begin_layout Plain Layout
\begin_inset Caption Standard

\begin_layout Plain Layout
\begin_inset CommandInset label
LatexCommand label
name "fig:Diagrammatic-representation-of"

\end_inset

A representation of part of a heap.
\end_layout

\end_inset


\end_layout

\end_inset


\end_layout

\begin_layout Standard
Figure 
\begin_inset CommandInset ref
LatexCommand ref
reference "fig:Diagrammatic-representation-of"

\end_inset

 shows a diagrammatic representation of a heap 
\begin_inset Formula $\chi_{0}$
\end_inset

 which contains actors 
\begin_inset Formula $\alpha_{1}$
\end_inset

 and 
\begin_inset Formula $\alpha_{2}$
\end_inset

, and objects 
\begin_inset Formula $\iota_{10}...\iota_{19}$
\end_inset

.
 The top rectangles indicate stack frames, for example 
\begin_inset Formula $\chi_{0}(\alpha_{1})=(\_,\_,\alpha_{1}\cdot\varphi_{1}\cdot\varphi_{2},\_)$
\end_inset

 and 
\begin_inset Formula $\varphi_{1}(\mathtt{this})=\iota_{10}$
\end_inset

 and 
\begin_inset Formula $\varphi_{2}(\mathtt{t_{2}})=\iota_{18}$
\end_inset

.
 The objects are in rounded boxes, and the annotated arrows indicate the
 contents of their fields, e.g.
 
\begin_inset Formula $\chi_{0}(\iota_{14},\mathtt{f10})=\iota_{19}$
\end_inset

.
 The annotations next to the field identifiers (
\begin_inset Formula $\mathtt{ref}$
\end_inset

, 
\begin_inset Formula $\mathtt{val}$
\end_inset

, etc.) give types to the variables.
 Note that 
\begin_inset Formula $\alpha_{1}=\iota_{10}$
\end_inset

 and 
\begin_inset Formula $\mathtt{\alpha_{2}=\iota_{14}}$
\end_inset

.
\end_layout

\begin_layout Standard
For consistent heap visibility we require that different paths originating
 from the same actor and pointing to the same object have locally consistent
 visibility, while paths originating from different actors and pointing
 to the same object have globally consistent visibility.
 For example, in figure 
\begin_inset CommandInset ref
LatexCommand ref
reference "fig:Diagrammatic-representation-of"

\end_inset

 the path 
\begin_inset Formula $\mathtt{this.f1.f5.f8}$
\end_inset

 starting at the first frame of actor 
\begin_inset Formula $\alpha_{1}$
\end_inset

 and the path 
\begin_inset Formula $\mathtt{this.f10}$
\end_inset

 at the first frame of actor 
\begin_inset Formula $\alpha_{2}$
\end_inset

 are aliases, as they both reach object 
\begin_inset Formula $\iota_{19}$
\end_inset

.
 The first path sees 
\begin_inset Formula $\iota_{19}$
\end_inset

 as 
\begin_inset Formula $\mathtt{tag}$
\end_inset

, while the second sees it as 
\begin_inset Formula $\mathtt{val}$
\end_inset

.
 These are globally compatible capabilities, and therefore these paths preserve
 consistent heap visibility.
 On the other hand, if we added a 
\begin_inset Formula $\mathtt{ref}$
\end_inset

 field to 
\begin_inset Formula $\iota_{15}$
\end_inset

, such that it pointed to 
\begin_inset Formula $\iota_{19}$
\end_inset

, the resulting capabilities would not be globally compatible.
\end_layout

\begin_layout Standard
\begin_inset Float figure
wide false
sideways false
status open

\begin_layout Plain Layout
\begin_inset Formula 
\[
\begin{array}{ccccc}
\Gamma & \in & \mathit{Env} & = & \mathit{LocalID}\rightarrow\mathit{ExtType}\\
\Delta & \in & \mathit{GlobalEnv} & = & (\mathit{ActorAddr}\times\mathit{Integer})\rightarrow\mathit{Env}\\
p & \in & \mathit{Path} & = & (\mathit{Integer}\times\mathit{LocalID})\cdot\overline{\mathit{FieldID}}
\end{array}
\]

\end_inset


\end_layout

\begin_layout Plain Layout
\begin_inset Caption Standard

\begin_layout Plain Layout
\begin_inset CommandInset label
LatexCommand label
name "fig:Global-environments."

\end_inset

Global environments and paths.
\end_layout

\end_inset


\end_layout

\end_inset


\end_layout

\begin_layout Standard
\begin_inset Float figure
wide false
sideways false
status open

\begin_layout Itemize
\begin_inset Formula $\Delta,\chi,\iota\vdash\iota:\mathtt{ref},(0,\mathtt{this})$
\end_inset


\end_layout

\begin_layout Itemize
\begin_inset Formula $\Delta,\chi,\alpha\vdash\iota:\kappa,(i,\mathtt{z})$
\end_inset

 iff 
\begin_inset Formula $\chi(\alpha,(i\cdot\mathtt{z}))=\iota$
\end_inset

 and 
\begin_inset Formula $\Delta(\alpha,i,\mathtt{z})=\mathtt{S}\,\kappa\,\phi$
\end_inset

 and 
\begin_inset Formula $\kappa\neq\mathtt{tag}$
\end_inset


\end_layout

\begin_layout Itemize
\begin_inset Formula $\Delta,\chi,\iota\vdash\iota':\kappa\blacktriangleright\kappa',p\cdot\mathtt{f}$
\end_inset

 iff 
\begin_inset Formula $\Delta,\chi,\iota\vdash\iota'':\kappa,p$
\end_inset

 and 
\begin_inset Formula $\chi(\iota'',\mathtt{f})=\iota'$
\end_inset

 and 
\begin_inset Formula $\mathcal{F}(\chi(\iota'')\downarrow_{1},\mathtt{f})=\mathtt{S}\,\kappa'$
\end_inset

 and 
\begin_inset Formula $\kappa\blacktriangleright\kappa'\neq\mathtt{tag}$
\end_inset


\end_layout

\begin_layout Itemize
\begin_inset Formula $\Delta,\chi,\iota\vdash\iota':\kappa$
\end_inset

 iff 
\begin_inset Formula $\exists p$
\end_inset

 such that 
\begin_inset Formula $\Delta,\chi,\iota\vdash\iota':\kappa,p$
\end_inset


\end_layout

\begin_layout Plain Layout
\begin_inset Caption Standard

\begin_layout Plain Layout
\begin_inset CommandInset label
LatexCommand label
name "fig:Visibility."

\end_inset

Visibility.
\end_layout

\end_inset


\end_layout

\end_inset


\end_layout

\begin_layout Standard
\begin_inset Float figure
wide false
sideways false
status open

\begin_layout Itemize
\begin_inset Formula $\kappa\blacktriangleright\kappa'=\begin{cases}
\kappa' & \mathit{if}\,\kappa\in\{\mathtt{iso,trn,ref}\}\\
\mathtt{val} & \mathit{if}\,\kappa=\mathtt{val}\vee\kappa'=\mathtt{val}\\
\mathtt{box} & \mathit{if}\,\kappa=\mathtt{box}\wedge\kappa'\notin\{\mathtt{iso,val,tag}\}\\
\mathtt{tag} & \mathit{otherwise}
\end{cases}$
\end_inset


\end_layout

\begin_layout Itemize
\begin_inset Formula $\chi,\alpha\vdash p_{1}\cdot\mathtt{f}\sim p_{2}\cdot\mathtt{f}$
\end_inset

 iff 
\begin_inset Formula $\chi(\alpha,p_{1})=\chi(\alpha,p_{2})$
\end_inset


\end_layout

\begin_layout Itemize
\begin_inset Formula $\chi,\alpha\vdash(i,\mathtt{z})\sim(i,\mathtt{z})$
\end_inset


\end_layout

\begin_layout Itemize
\begin_inset Formula $\chi,\alpha\vdash\iota\in p$
\end_inset

 iff 
\begin_inset Formula $\exists p',\mathtt{\bar{f}}$
\end_inset

 such that 
\begin_inset Formula $p=p'.\mathtt{\bar{f}}$
\end_inset

 and 
\begin_inset Formula $\chi(\alpha,p')=\iota$
\end_inset


\end_layout

\begin_layout Itemize
\begin_inset Formula $\chi(\alpha,(i,\mathtt{z})\cdot\mathtt{\overline{f}})=\chi(\varphi_{i}(\mathtt{z}),\mathtt{\overline{f}})$
\end_inset

 where 
\begin_inset Formula $\chi(\alpha)\downarrow_{4}=\alpha\cdot\overline{\varphi}$
\end_inset


\end_layout

\begin_layout Itemize
\begin_inset Formula $\chi(\alpha,(-i,\mathtt{x_{j}})\cdot\mathtt{\overline{f}})=\chi(v_{j},\mathtt{\overline{f}})$
\end_inset

 where 
\begin_inset Formula $Q(\chi,\alpha)=\overline{\mu}$
\end_inset

 and 
\begin_inset Formula $\mu_{i}=(\_,\overline{v})$
\end_inset


\end_layout

\begin_layout Itemize
\begin_inset Formula $\mathit{Stable}(\Delta,\alpha,(i,\mathtt{z})\cdot\mathtt{\overline{f}})$
\end_inset

 iff 
\begin_inset Formula $\Delta(\alpha,i,\mathtt{z})\notin\{\mathtt{iso,trn}\}$
\end_inset

 or 
\begin_inset Formula $\mathtt{z}\neq\mathtt{t}$
\end_inset


\end_layout

\begin_layout Plain Layout
\begin_inset Caption Standard

\begin_layout Plain Layout
\begin_inset CommandInset label
LatexCommand label
name "fig:Paths"

\end_inset

Topological properties of paths.
\end_layout

\end_inset


\end_layout

\end_inset


\end_layout

\begin_layout Standard
For the formal definition of consistent heap visibility, we need notions
 of:
\end_layout

\begin_layout Enumerate
Paths 
\begin_inset Formula $p$
\end_inset

 and global environments 
\begin_inset Formula $\Delta$
\end_inset

, which give types to the local variables and temporaries in each frame
 or message, as defined in fig.
 
\begin_inset CommandInset ref
LatexCommand ref
reference "fig:Global-environments."

\end_inset

.
\end_layout

\begin_layout Enumerate
Path visibility 
\begin_inset Formula $\Delta,\chi,\iota\vdash\iota':\kappa,p$
\end_inset

, which says that the object or actor 
\begin_inset Formula $\iota$
\end_inset

 sees the object or actor 
\begin_inset Formula $\iota'$
\end_inset

 as capability 
\begin_inset Formula $\kappa$
\end_inset

 through path 
\begin_inset Formula $p$
\end_inset

, as defined in fig.
 
\begin_inset CommandInset ref
LatexCommand ref
reference "fig:Visibility."

\end_inset

.
\end_layout

\begin_layout Enumerate
Topological properties of paths, as defined in figure 
\begin_inset CommandInset ref
LatexCommand ref
reference "fig:Paths"

\end_inset

.
\end_layout

\begin_layout Standard
Environments, 
\begin_inset Formula $\Gamma$
\end_inset

, map variables (i.e.
 local variables or temporaries) to extended types and global environments,
 
\begin_inset Formula $\Delta$
\end_inset

, map actor addresses and integers to environments.
 Figure 
\begin_inset CommandInset ref
LatexCommand ref
reference "fig:Diagrammatic-representation-of"

\end_inset

 indicates the types assigned to local variables through the annotations.
 Thus, it has an implicit global environment 
\begin_inset Formula $\Delta_{0}$
\end_inset

, such that 
\begin_inset Formula $\Delta_{0},\chi_{0},\alpha_{1}\vdash\iota_{10}:\mathtt{ref},(1,\mathtt{this})$
\end_inset

, and 
\begin_inset Formula $\Delta_{0},\chi_{0},\alpha_{2}\vdash\iota_{19}:\mathtt{val},(1,\mathtt{this})\cdot\mathtt{f10}$
\end_inset

.
\end_layout

\begin_layout Standard
To define path visibility, the notion of deep viewpoint adaptation 
\begin_inset Formula $\kappa\blacktriangleright\kappa'$
\end_inset

 is used, which combines two capabilities as given in figure 
\begin_inset CommandInset ref
LatexCommand ref
reference "fig:Paths"

\end_inset

.
 The definition ensures that 
\begin_inset Formula $\kappa\blacktriangleright\kappa'=\kappa'$
\end_inset

 if 
\begin_inset Formula $\kappa$
\end_inset

 is writeable (deep mutability), 
\begin_inset Formula $\kappa\blacktriangleright\kappa'=\mathtt{val}$
\end_inset

 if either 
\begin_inset Formula $\kappa$
\end_inset

 or 
\begin_inset Formula $\kappa'$
\end_inset

 is 
\begin_inset Formula $\mathtt{val}$
\end_inset

 (deep immutability) and 
\begin_inset Formula $\mathtt{box}\blacktriangleright\kappa'=\mathtt{box}$
\end_inset

 unless 
\begin_inset Formula $\kappa'\in\{\mathtt{iso,val,tag}\}$
\end_inset

.
 For example, 
\begin_inset Formula $\mathtt{iso}\blacktriangleright\mathtt{ref}=\mathtt{ref}$
\end_inset

.
\end_layout

\begin_layout Standard
The rules in figure 
\begin_inset CommandInset ref
LatexCommand ref
reference "fig:Visibility."

\end_inset

 say that an address sees itself as 
\begin_inset Formula $\mathtt{ref}$
\end_inset

, an actor sees a stack identifier as the capability provided by 
\begin_inset Formula $\Delta$
\end_inset

, and an address sees another address as a deep viewpoint adapted capability.
 Note that, for visibility, 
\begin_inset Formula $\mathtt{tag}$
\end_inset

 types are not seen.
 Therefore, our example gives us:
\end_layout

\begin_layout Itemize
\begin_inset Formula $\Delta_{0},\chi_{0},\alpha_{1}\vdash\iota_{10}:\mathtt{ref},(1,\mathtt{this})$
\end_inset

, but also
\begin_inset Newline newline
\end_inset


\begin_inset Formula $\Delta_{0},\chi_{0},\alpha_{1}\vdash\iota_{10}:\mathtt{box},(1,\mathtt{this})\cdot\mathtt{f1}\cdot\mathtt{f2}$
\end_inset

.
 
\end_layout

\begin_layout Itemize
\begin_inset Formula $\Delta_{0},\chi_{0},\alpha_{2}\vdash\iota_{19}:\mathtt{val},(1,\mathtt{this})\cdot\mathtt{f10}$
\end_inset

, but also
\begin_inset Newline newline
\end_inset


\begin_inset Formula $\Delta_{0},\chi_{0},\alpha_{1}\vdash\iota_{19}:\mathtt{tag},(1,\mathtt{this})\cdot\mathtt{f1}\cdot\mathtt{f5}\cdot\mathtt{f8}$
\end_inset

.
\end_layout

\begin_layout Standard
\begin_inset Float figure
wide false
sideways false
status open

\begin_layout Plain Layout
\begin_inset Formula $\mathit{WFV}(\Delta,\chi)\,\mathit{iff}$
\end_inset


\end_layout

\begin_layout Plain Layout
\begin_inset Formula $\forall\alpha,\alpha',\iota,\iota'\in\chi.\forall\kappa,\kappa',p,p',\mathtt{t}$
\end_inset

 where 
\begin_inset Formula $\mathit{Stable}(\Delta,\alpha,p)$
\end_inset

 and 
\begin_inset Formula $\mathit{Stable}(\Delta,\alpha,p')$
\end_inset


\end_layout

\begin_layout Enumerate
If 
\begin_inset Formula $\Delta,\chi,\alpha\vdash\iota:\kappa$
\end_inset

 and 
\begin_inset Formula $\Delta,\chi,\alpha'\vdash\iota:\kappa'$
\end_inset

 and 
\begin_inset Formula $\alpha\neq\alpha'$
\end_inset

 then 
\begin_inset Formula $\kappa\sim_{g}\kappa'$
\end_inset


\end_layout

\begin_layout Enumerate
If 
\begin_inset Formula $\Delta,\chi,\alpha\vdash\iota:\kappa,p$
\end_inset

 and 
\begin_inset Formula $\Delta,\chi,\alpha\vdash\iota:\kappa',p'$
\end_inset

 then
\begin_inset Separator latexpar
\end_inset


\end_layout

\begin_deeper
\begin_layout Enumerate
\begin_inset Formula $\chi,\alpha\vdash p\sim p'$
\end_inset

 or 
\end_layout

\begin_layout Enumerate
\begin_inset Formula $\kappa\sim_{\ell}\kappa'$
\end_inset


\end_layout

\end_deeper
\begin_layout Enumerate
If 
\begin_inset Formula $\Delta,\chi,\alpha\vdash\iota:\kappa$
\end_inset

 and 
\begin_inset Formula $\Delta,\chi,\alpha\vdash\iota':\kappa',p'$
\end_inset

 and 
\begin_inset Formula $\Delta,\chi,\iota\vdash\iota':\kappa''$
\end_inset

 and 
\begin_inset Formula $\kappa\in\{\mathtt{iso,trn}\}$
\end_inset

 then
\begin_inset Separator latexpar
\end_inset


\end_layout

\begin_deeper
\begin_layout Enumerate
\begin_inset Formula $\chi,\alpha\vdash\iota\in p'$
\end_inset

 or
\end_layout

\begin_layout Enumerate
\begin_inset Formula $\kappa''\in\{\mathtt{val,box}\}$
\end_inset

 and 
\begin_inset Formula $\kappa'\sim_{g}\mathtt{val}$
\end_inset

 or
\end_layout

\begin_layout Enumerate
\begin_inset Formula $\kappa''\in\{\mathtt{iso,trn,ref}\}$
\end_inset

 and 
\begin_inset Formula $\kappa\sim_{\ell}\kappa'$
\end_inset


\end_layout

\end_deeper
\begin_layout Enumerate
If 
\begin_inset Formula $\Delta(\alpha,i,\mathtt{t})=\mathtt{S}\,\kappa$
\end_inset

 and 
\begin_inset Formula $\kappa\in\{\mathtt{iso,trn}\}$
\end_inset

 and 
\begin_inset Formula $\chi(\alpha,i,\mathtt{t})=\chi(\alpha,p_{1})=\iota$
\end_inset

 then
\begin_inset Separator latexpar
\end_inset


\end_layout

\begin_deeper
\begin_layout Enumerate
\begin_inset Formula $p_{1}=(i,\mathtt{t})$
\end_inset

 or
\end_layout

\begin_layout Enumerate
\begin_inset Formula $\exists\iota',\kappa',p_{2},\mathtt{\overline{f}}$
\end_inset

 such that
\begin_inset Separator latexpar
\end_inset


\end_layout

\begin_deeper
\begin_layout Enumerate
\begin_inset Formula $\kappa\le\kappa'$
\end_inset

 
\end_layout

\begin_layout Enumerate
\begin_inset Formula $\kappa'\in\{\mathtt{iso,trn}\}$
\end_inset


\end_layout

\begin_layout Enumerate
\begin_inset Formula $p_{1}=p_{2}\cdot\mathtt{\overline{f}}$
\end_inset


\end_layout

\begin_layout Enumerate
\begin_inset Formula $\Delta,\chi,\alpha\vdash\iota':\kappa',p_{2}$
\end_inset


\end_layout

\begin_layout Enumerate
\begin_inset Formula $\Delta,\chi,\iota'\vdash\iota:\kappa,\mathtt{\overline{f}}$
\end_inset


\end_layout

\end_deeper
\end_deeper
\begin_layout Plain Layout
\begin_inset Caption Standard

\begin_layout Plain Layout
\begin_inset CommandInset label
LatexCommand label
name "fig:Well-formed-visibility."

\end_inset

Well-formed visibility.
\end_layout

\end_inset


\end_layout

\end_inset


\end_layout

\begin_layout Standard
In figure 
\begin_inset CommandInset ref
LatexCommand ref
reference "fig:Paths"

\end_inset

, two paths are compatible if they share the last step or they are the same
 identifier with no fields, an address 
\begin_inset Formula $\iota$
\end_inset

 is in a path if some prefix of the path points to 
\begin_inset Formula $\iota$
\end_inset

, and a path is stable, 
\begin_inset Formula $\mathit{Stable}(\Delta,\alpha,p)$
\end_inset

, if its initial identifier is not a unique temporary.
 For example, 
\begin_inset Formula $\chi_{0},\alpha_{2}\vdash(1,\mathtt{this})\cdot\mathtt{f10}\sim(1,\mathtt{y1})\cdot\mathtt{f10}$
\end_inset

.
 Also, 
\begin_inset Formula $\mathit{Stable}(\Delta_{0},\alpha_{1},(1,\mathtt{this})\cdot\mathtt{f1}\cdot\mathtt{f4})$
\end_inset

 and 
\begin_inset Formula $\neg\mathit{Stable}(\Delta_{0},\alpha_{1},(2,\mathtt{t2})\cdot\mathtt{f9})$
\end_inset

, even though the two paths are aliases.
\end_layout

\begin_layout Standard
Consistent heap visibility is defined in figure 
\begin_inset CommandInset ref
LatexCommand ref
reference "fig:Well-formed-visibility."

\end_inset

.
 It requires:
\end_layout

\begin_layout Enumerate
Global compatibility.
 Any two distinct actors that can see the same address must see that address
 with globally compatible capabilities.
\end_layout

\begin_layout Enumerate
Local compatibility.
 An actor that sees an address in multiple ways must either see compatible
 paths or locally compatible capabilities.
\end_layout

\begin_layout Enumerate
Containment properties of 
\begin_inset Formula $\mathtt{iso}$
\end_inset

 and 
\begin_inset Formula $\mathtt{trn}$
\end_inset

.
 Given 
\begin_inset Formula $\alpha$
\end_inset

 that sees 
\begin_inset Formula $\iota$
\end_inset

 as some unique 
\begin_inset Formula $\kappa$
\end_inset

 and sees 
\begin_inset Formula $\iota'$
\end_inset

 as 
\begin_inset Formula $\kappa'$
\end_inset

 via some stable 
\begin_inset Formula $p'$
\end_inset

, and given that 
\begin_inset Formula $\iota$
\end_inset

 sees 
\begin_inset Formula $\iota'$
\end_inset

 as 
\begin_inset Formula $\kappa''$
\end_inset

:
\begin_inset Separator latexpar
\end_inset


\end_layout

\begin_deeper
\begin_layout Enumerate
\begin_inset Formula $\iota'$
\end_inset

 must be contained by 
\begin_inset Formula $\iota$
\end_inset

, or
\end_layout

\begin_layout Enumerate
neither 
\begin_inset Formula $\iota$
\end_inset

 nor 
\begin_inset Formula $\alpha$
\end_inset

 can write to 
\begin_inset Formula $\iota'$
\end_inset

, or
\end_layout

\begin_layout Enumerate
\begin_inset Formula $\iota$
\end_inset

 can write to 
\begin_inset Formula $\iota'$
\end_inset

 and 
\begin_inset Formula $\alpha$
\end_inset

 sees 
\begin_inset Formula $\iota'$
\end_inset

 as locally compatible with 
\begin_inset Formula $\kappa$
\end_inset

.
 
\end_layout

\end_deeper
\begin_layout Enumerate
Properties of unique temporary identifiers.
 Given 
\begin_inset Formula $\mathtt{t}$
\end_inset

 that points to 
\begin_inset Formula $\iota$
\end_inset

 , some other path 
\begin_inset Formula $p_{1}$
\end_inset

 to the same 
\begin_inset Formula $\iota$
\end_inset

 must be either:
\begin_inset Separator latexpar
\end_inset


\end_layout

\begin_deeper
\begin_layout Enumerate
also 
\begin_inset Formula $\mathtt{t}$
\end_inset

 or
\end_layout

\begin_layout Enumerate
that path 
\begin_inset Formula $p_{1}$
\end_inset

 must have a prefix 
\begin_inset Formula $p_{2}$
\end_inset

 that sees some 
\begin_inset Formula $\iota'$
\end_inset

 with a unique capability 
\begin_inset Formula $\kappa'$
\end_inset

 less precise than 
\begin_inset Formula $\kappa$
\end_inset

 and 
\begin_inset Formula $\iota'$
\end_inset

 must see 
\begin_inset Formula $\iota$
\end_inset

 as 
\begin_inset Formula $\kappa$
\end_inset

.
\end_layout

\end_deeper
\begin_layout Standard
An implication of well-formed visibility is that if two variables (temporary
 or otherwise) are aliases and one of them has unique type (aliased or unaliased
) then 1) they come from the same actor and 2) they are either the same
 variable or they have locally compatible capabilities, cf.
 lemmas 
\begin_inset CommandInset ref
LatexCommand ref
reference "lem:Temporaries-and-variables"

\end_inset

 and 
\begin_inset CommandInset ref
LatexCommand ref
reference "lem:Isolation-in-well-formed"

\end_inset

.
 Note that 
\begin_inset Formula $\mathit{WFV.1-3}$
\end_inset

 are concerned with stable paths only, while 
\begin_inset Formula $\mathit{WFV.4}$
\end_inset

 is about unstable paths.
 In particular, 
\begin_inset Formula $\mathit{WFV.4}$
\end_inset

 allows a unique temporary to break the requirements from 
\begin_inset Formula $\mathit{WFV.3}$
\end_inset

 and alias something writeable from a unique.
\end_layout

\begin_layout Standard
The heap from figure 
\begin_inset CommandInset ref
LatexCommand ref
reference "fig:Diagrammatic-representation-of"

\end_inset

 has consistent visibility.
 The paths 
\begin_inset Formula $\mathtt{(1,this)\cdot f1\cdot f5\cdot f8}$
\end_inset

 from 
\begin_inset Formula $\alpha_{1}$
\end_inset

 and 
\begin_inset Formula $\mathtt{(1,this)\cdot f10}$
\end_inset

 from 
\begin_inset Formula $\alpha_{2}$
\end_inset

 satisfy 
\begin_inset Formula $\mathit{WFV.1}$
\end_inset

, while 
\begin_inset Formula $\mathtt{(1,x1)\cdot f4}$
\end_inset

 from 
\begin_inset Formula $\alpha_{1}$
\end_inset

 and 
\begin_inset Formula $\mathtt{(2,this)}$
\end_inset

 from 
\begin_inset Formula $\alpha_{1}$
\end_inset

 satisfy 
\begin_inset Formula $\mathit{WFV.2}$
\end_inset

 and 
\begin_inset Formula $\mathit{WFV.3}$
\end_inset

.
 On the other hand, the temporary 
\begin_inset Formula $\mathtt{(2,t2)}$
\end_inset

 is not stable, and therefore not restricted by 
\begin_inset Formula $\mathit{WFV.2}$
\end_inset

 or 
\begin_inset Formula $\mathit{WFV.3}$
\end_inset

, but does adhere to 
\begin_inset Formula $\mathit{WFV.4}$
\end_inset

.
 Finally, the assignment 
\begin_inset Formula $\mathtt{this.f1.f5.f6=this.f1.f5.f7}$
\end_inset

 would break 
\begin_inset Formula $\mathit{WFV.2}$
\end_inset

, while setting 
\begin_inset Formula $\mathtt{t2}$
\end_inset

 to point to 
\begin_inset Formula $\iota_{15}$
\end_inset

 would break 
\begin_inset Formula $\mathit{WFV.4}$
\end_inset

.
\end_layout

\begin_layout Section
\begin_inset CommandInset label
LatexCommand label
name "sec:Soundness-properties"

\end_inset

Soundness
\end_layout

\begin_layout Standard
\begin_inset Float figure
wide false
sideways false
status open

\begin_layout Itemize
\begin_inset Formula $\Delta\vdash\chi\diamond$
\end_inset

 iff 
\begin_inset Formula $\forall\iota,\alpha\in\mathit{dom}(\chi)$
\end_inset

, 
\begin_inset Formula $\chi\vdash\iota\diamond$
\end_inset

 and 
\begin_inset Formula $\Delta,\chi\vdash\alpha\diamond$
\end_inset

 and 
\begin_inset Formula $\mathit{WFV}(\Delta,\chi)$
\end_inset


\end_layout

\begin_layout Itemize
\begin_inset Formula $\chi\vdash\iota\diamond$
\end_inset

 iff 
\begin_inset Formula $\forall\mathtt{f}$
\end_inset

, 
\begin_inset Formula $\mathcal{F}(\chi(\iota)\downarrow_{1},\mathtt{f})=\mathtt{S}\,\kappa$
\end_inset

 implies 
\begin_inset Formula $\chi(\iota,\mathtt{f})\downarrow_{1}=\mathtt{S}$
\end_inset


\end_layout

\begin_layout Itemize
\begin_inset Formula $\Delta,\chi\vdash\alpha\diamond$
\end_inset

 iff 
\begin_inset Formula $\chi(\alpha)=(\_,\_,\bar{\mu},\alpha\cdot\overline{\varphi},\mathtt{e})$
\end_inset

 and 
\begin_inset Formula $\forall i$
\end_inset

, 
\begin_inset Formula $\Delta,\chi,\alpha\vdash\varphi_{i},i\diamond$
\end_inset

 and 
\begin_inset Formula $\forall j$
\end_inset

, 
\begin_inset Formula $\Delta,\chi\vdash\mu_{j},j\diamond$
\end_inset


\end_layout

\begin_layout Itemize
\begin_inset Formula $\Delta,\chi,\alpha\vdash\varphi,i\diamond$
\end_inset

 iff given 
\begin_inset Formula $\varphi=(\mathtt{m},\_,\mathtt{E[\cdot]})$
\end_inset

 and 
\begin_inset Formula $\mathcal{M}(\varphi,\chi)=(\mathtt{T,\overline{x:T},\_,ET})$
\end_inset

 and 
\begin_inset Formula $\Delta(\alpha,i)=\Gamma$
\end_inset

 then
\begin_inset Separator latexpar
\end_inset


\end_layout

\begin_deeper
\begin_layout Enumerate
\begin_inset Formula $\Gamma(\mathtt{this})=\mathtt{T}$
\end_inset

 and 
\begin_inset Formula $\forall j\in1..|\mathtt{\overline{T}}|.\Gamma(\mathtt{x_{j}})=\mathtt{T_{j}}$
\end_inset


\end_layout

\begin_layout Enumerate
\begin_inset Formula $\forall\mathtt{z}\in\varphi$
\end_inset

, 
\begin_inset Formula $\Gamma(\mathtt{z})=\mathtt{S}\,\kappa\,\phi$
\end_inset

 and 
\begin_inset Formula $\chi(\varphi(\mathtt{z}))\downarrow_{1}=\mathtt{S}$
\end_inset


\end_layout

\begin_layout Enumerate
If 
\begin_inset Formula $i=1$
\end_inset

 then 
\begin_inset Formula $\mathtt{E[\cdot]}=\cdot$
\end_inset

 and 
\begin_inset Formula $\varphi(\mathtt{this})=\alpha$
\end_inset


\end_layout

\begin_layout Enumerate
If 
\begin_inset Formula $i>1$
\end_inset

, given 
\begin_inset Formula $\chi(\alpha)\downarrow_{4}=\alpha\cdot\overline{\varphi}$
\end_inset

 and 
\begin_inset Formula $\Gamma'=\Delta(\alpha,i-1)$
\end_inset

 and 
\begin_inset Formula $\mathtt{t}\notin\Gamma'$
\end_inset

 and 
\begin_inset Formula $\Gamma''=\Gamma'[\mathtt{t}\mapsto\mathtt{ET}]$
\end_inset

 then
\begin_inset Separator latexpar
\end_inset


\end_layout

\begin_deeper
\begin_layout Enumerate
\begin_inset Formula $\Gamma''\vdash\mathtt{E[t]}:\mathcal{M}(\varphi_{i-1},\chi)\downarrow_{4}$
\end_inset


\end_layout

\begin_layout Enumerate
\begin_inset Formula $\mathit{WFT}(\Delta[(\alpha,i)\mapsto\Gamma''],\chi,\alpha,i,\mathtt{E[t]})$
\end_inset


\end_layout

\end_deeper
\begin_layout Enumerate
If 
\begin_inset Formula $i=|\chi(\alpha)\downarrow_{4}|$
\end_inset

 then 
\begin_inset Formula $\mathit{WFT}(\Delta,\chi,\alpha,i,\mathtt{e})$
\end_inset

 and 
\begin_inset Formula $\Gamma\vdash\mathtt{e:ET}$
\end_inset


\end_layout

\end_deeper
\begin_layout Itemize
\begin_inset Formula $\Delta,\chi,\alpha\vdash\mu,i\diamond$
\end_inset

 iff given 
\begin_inset Formula $\mu=(\mathtt{b},\overline{v})$
\end_inset

 and 
\begin_inset Formula $v_{j}=\iota$
\end_inset

 and 
\begin_inset Formula $\mathcal{M}(\chi(\alpha)\downarrow_{1},\mathtt{b})=(\_,\mathtt{\overline{x:S\,\kappa}},\_,\_)$
\end_inset

 and 
\begin_inset Formula $\Delta(\alpha,-i)=\Gamma$
\end_inset

 then
\begin_inset Separator latexpar
\end_inset


\end_layout

\begin_deeper
\begin_layout Enumerate
\begin_inset Formula $\chi(\iota)\downarrow_{1}=\mathtt{S_{j}}$
\end_inset


\end_layout

\begin_layout Enumerate
\begin_inset Formula $\Gamma(\mathtt{x_{j}})=\mathtt{S\,\kappa}$
\end_inset


\end_layout

\end_deeper
\begin_layout Plain Layout
\begin_inset Caption Standard

\begin_layout Plain Layout
\begin_inset CommandInset label
LatexCommand label
name "fig:Well-formed-heaps."

\end_inset

Well-formed heaps.
\end_layout

\end_inset


\end_layout

\end_inset


\end_layout

\begin_layout Standard
A heap 
\begin_inset Formula $\chi$
\end_inset

 is well-formed as defined in figure 
\begin_inset CommandInset ref
LatexCommand ref
reference "fig:Well-formed-heaps."

\end_inset

 if all objects in the heap are well-formed, all actors in the heap are
 well-formed, and visibility is well-formed.
 An object is well-formed if all its fields belong to the type defined in
 the object's class.
 An actor is well-formed if its stack frames and messages are well-formed.
 A stack frame is well-formed if 1) its receiver and arguments are well-formed,
 2) all local identifiers are well-formed, 3) if it is the only stack frame,
 it has no continuation and the receiver is the actor, 4) if it is not the
 only stack frame, its return value and temporary identifiers are well-formed
 with regard to the previous frame, and 5) if it is the last frame, temporary
 identifiers are well-formed and the expression has the expected type.
\end_layout

\begin_layout Subsection
Treatment of temporaries
\end_layout

\begin_layout Standard
Temporaries with unique capabilities, 
\begin_inset Formula $\mathtt{iso}$
\end_inset

 or 
\begin_inset Formula $\mathtt{trn}$
\end_inset

, are fragile: on the one hand they may break the encapsulation of other
 
\begin_inset Formula $\mathtt{iso}$
\end_inset

 or 
\begin_inset Formula $\mathtt{trn}$
\end_inset

 objects.
 For example, because 
\begin_inset Formula $\mathtt{iso}\triangleright\mathtt{iso}=\mathtt{iso}$
\end_inset

, a field read (
\noun on
Fld
\noun default
) may return a temporary pointing within the encapsulation of 
\begin_inset Formula $\mathtt{iso}$
\end_inset

.
 On the other hand, an assignment to another field or variable might break
 
\emph on
their
\emph default
 encapsulation.
\end_layout

\begin_layout Standard
To be well-formed, it is required that in a frame, no more than one temporary
 has an 
\begin_inset Formula $\mathtt{iso}$
\end_inset

 or 
\begin_inset Formula $\mathtt{trn}$
\end_inset

 capability, and this temporary appears on a field assignment or a field
 read.
 In addition, any temporaries that appear within a recover expression are
 either inaccessible from any frame or are only accessible through sendable
 local variables.
\end_layout

\begin_layout Definition
Well-formed temporaries.
 
\begin_inset Formula $\mathit{WFT}(\Delta,\chi,\alpha,i,\mathtt{e})$
\end_inset

 iff:
\begin_inset Separator latexpar
\end_inset


\end_layout

\begin_deeper
\begin_layout Enumerate
No temporary appears more than once in 
\emph on

\begin_inset Formula $\mathtt{e}$
\end_inset

.
\end_layout

\begin_layout Enumerate
If 
\begin_inset Formula $\mathcal{T}(\Gamma)\neq\emptyset$
\end_inset

, then 
\begin_inset Formula $\mathtt{e\equiv E[e']}$
\end_inset

, where 
\begin_inset Formula $\mathtt{e'}$
\end_inset

 is a redex of the form 
\begin_inset Formula $\mathtt{t.f}$
\end_inset

 or 
\begin_inset Formula $\mathtt{t.f=y}$
\end_inset

, and 
\begin_inset Formula $\mathcal{T}(\Gamma)=\{\mathtt{t}\}$
\end_inset

, where 
\begin_inset Formula $\Gamma=\Delta(\alpha,i)$
\end_inset

 and 
\begin_inset Formula $\mathcal{T}(\Gamma)\equiv\{\mathtt{t}\,|\,\Gamma(\mathtt{t})=\mathtt{S}\,\kappa\wedge\kappa\in\{\mathtt{iso},\mathtt{trn}\}\}$
\end_inset

.
\end_layout

\begin_layout Enumerate
If 
\begin_inset Formula $\mathtt{e=E[recover\,e']}$
\end_inset

 and 
\begin_inset Formula $\Delta,\chi,\alpha\vdash\iota:\_,(i,\mathtt{t})$
\end_inset

 and 
\begin_inset Formula $\Delta,\chi,\alpha\vdash\iota:\kappa',(i',\mathtt{z})\cdot\mathtt{\overline{f}}$
\end_inset

 where 
\begin_inset Formula $\mathtt{t}$
\end_inset

 is free in 
\begin_inset Formula $\mathtt{e'}$
\end_inset

then either 
\begin_inset Formula $\mathit{Sendable}(\Delta(\alpha,i',\mathtt{z}))$
\end_inset

 or 
\begin_inset Formula $(i,\mathtt{z})=(i',\mathtt{t'})$
\end_inset

 and 
\begin_inset Formula $\mathtt{z}$
\end_inset

 is not free in 
\begin_inset Formula $\mathtt{E[\cdot]}$
\end_inset

.
\end_layout

\end_deeper
\begin_layout Standard
The requirements above do not apply to 
\emph on
unaliased unique
\emph default
 capabilities, e.g.
 
\begin_inset Formula $\mathtt{iso}\circ$
\end_inset

, or 
\begin_inset Formula $\mathtt{trn}\circ$
\end_inset

.
 When proving type preservation, we maintain the property 
\begin_inset Formula $\mathit{WFT}(\Delta,\chi,\alpha,i,\mathtt{e})$
\end_inset

 by turning the types of temporaries with unique capabilities 
\begin_inset Formula $\kappa\in\{\mathtt{iso},\mathtt{trn}\}$
\end_inset

 into their aliases, 
\begin_inset Formula ${\cal A}(\kappa)$
\end_inset

, as soon as the temporary is no longer involved in field reads or updates
 in the current redex.
\end_layout

\begin_layout Definition
We call an expression 
\emph on

\begin_inset Formula $\mathtt{e}$
\end_inset


\emph default
 a 
\emph on
redex
\emph default
 if it has one of the following forms:
\end_layout

\begin_layout Definition
\begin_inset Formula $\begin{array}{ccc}
\mathtt{e} & ::= & \mathtt{z.f\,|\,z.f=y\,|\,z.m(\overline{y})\,|\,z.b(\overline{y})\,|\,S.k(\overline{z}})\end{array}$
\end_inset


\end_layout

\begin_layout Standard
The type of the expression is preserved despite this change, because the
 type rules from fig.
 
\begin_inset CommandInset ref
LatexCommand ref
reference "fig:Expression-typing"

\end_inset

 require the alias of a type (
\begin_inset Formula $\ldots\vdash_{{\cal A}}\ldots$
\end_inset

) in all such situations.
 This is explained further in lemma 
\begin_inset CommandInset ref
LatexCommand ref
reference "lem:Aliasing-and-replaceability."

\end_inset

.
\end_layout

\begin_layout Theorem
\begin_inset CommandInset label
LatexCommand label
name "A-well-formed-heap"

\end_inset

A well-formed heap ensures data race freedom.
\end_layout

\begin_layout Theorem
\begin_inset Formula $\forall\Delta,\chi,\alpha_{1},\alpha_{2},\mathtt{f},\mathtt{g}$
\end_inset

 , if
\begin_inset Separator latexpar
\end_inset


\end_layout

\begin_deeper
\begin_layout Enumerate
\begin_inset Formula $\Delta\vdash\chi\diamond$
\end_inset

, and 
\end_layout

\begin_layout Enumerate
\begin_inset Formula $\chi(\alpha_{1})=(\_,\_,\sigma_{1},\_,\mathtt{E_{1}[z_{1}.f=z_{3}]})$
\end_inset

, and
\end_layout

\begin_layout Enumerate
\begin_inset Formula $\chi(\alpha_{2})=(\_,\_,\sigma_{2},\_,\mathtt{E_{2}[z_{2}.g]})$
\end_inset

 
\end_layout

\end_deeper
\begin_layout Theorem
then 
\begin_inset Formula $\chi(\alpha_{1},|\sigma_{1}|\cdot\mathtt{z_{1}})\ne\chi(\alpha_{2},|\sigma_{2}|\cdot\mathtt{z_{2}})$
\end_inset

.
\end_layout

\begin_layout Proof
Follows from the type system and the application of 
\begin_inset Formula $\mathit{WFV}.1$
\end_inset

 (global consistency).
\end_layout

\begin_layout Theorem
Well-formedness is preserved.
\end_layout

\begin_layout Theorem
\begin_inset Formula $\forall\Delta,\chi$
\end_inset

, if 
\begin_inset Formula $\Delta\vdash\chi\diamond$
\end_inset

 and 
\begin_inset Formula $\chi\rightarrow\chi'$
\end_inset

 then 
\begin_inset Formula $\exists\Delta'.\Delta'\vdash\chi'\diamond$
\end_inset

.
\end_layout

\begin_layout Proof
Follows from lemmas 
\begin_inset CommandInset ref
LatexCommand ref
reference "lem:SL1"

\end_inset

-
\begin_inset CommandInset ref
LatexCommand ref
reference "lem:Type-preservation-upon-1"

\end_inset

.
\end_layout

\begin_layout Subsection
Atomicity
\end_layout

\begin_layout Standard
Because the type of any entity does not change, any readable reference is
 always readable, and so guarantees no other actor can write to it.
 This holds not just for methods, but for behaviours.
 As a result, theorem 
\begin_inset CommandInset ref
LatexCommand ref
reference "A-well-formed-heap"

\end_inset

 guarantees that behaviours are 
\emph on
logically atomic
\emph default
, a stronger guarantee than data-race freedom.
\end_layout

\begin_layout Section
Soundness Argument
\end_layout

\begin_layout Standard
The property central to any soundness argument is the preservation of the
 well-formed visibility property, 
\begin_inset Formula $\mathit{WFV}(\Delta,\chi)$
\end_inset

, and the well-formed temporaries property 
\begin_inset Formula $\mathit{WFT}(\Delta,\chi,\alpha,i,\mathtt{e})$
\end_inset

 for all expressions and continuations.
 To study the former, we need properties about the creation of new paths,
 while for the latter, we need to control the types we assign to the temporaries
 in each step.
\end_layout

\begin_layout Standard
While this section is, by necessity, detailed and somewhat verbose, the
 argument presented is standard and unsurprising.
 Its approach is based on that taken in existing work on the Java type system,
 particularly in 
\begin_inset CommandInset citation
LatexCommand cite
key "drossopoulou1999java"

\end_inset

 and 
\begin_inset CommandInset citation
LatexCommand cite
key "igarashi2001featherweight"

\end_inset

.
 I personally found both works invaluable as aids to both understanding
 and formulating type soundness arguments.
\end_layout

\begin_layout Lemma
Uniqueness of contexts.
\end_layout

\begin_layout Lemma
For any expressions 
\begin_inset Formula $\mathtt{e_{1}}$
\end_inset

, 
\begin_inset Formula $\mathtt{e_{2}}$
\end_inset

 and contexts 
\begin_inset Formula $\mathtt{E_{1}[\cdot]}$
\end_inset

, 
\begin_inset Formula $\mathtt{E_{2}[\cdot]}$
\end_inset

, if 
\begin_inset Formula $\mathtt{E_{1}[e_{2}]\equiv E_{2}[e_{2}]}$
\end_inset

 and 
\begin_inset Formula $\mathtt{e_{1}}$
\end_inset

 and 
\begin_inset Formula $\mathtt{e_{2}}$
\end_inset

 are redexes then 
\begin_inset Formula $\mathtt{E_{1}[\cdot]\equiv E_{2}[\cdot]}$
\end_inset

 and 
\begin_inset Formula $\mathtt{e_{1}\equiv e_{2}}$
\end_inset

.
\end_layout

\begin_deeper
\begin_layout Lemma
\begin_inset CommandInset label
LatexCommand label
name "lem:Context-lemma."

\end_inset

Context lemma.
\end_layout

\begin_layout Enumerate
\begin_inset Formula $\Gamma\vdash\mathtt{E[e]:ET}\Rightarrow\exists\mathtt{ET'}.\Gamma,\mathtt{y}\mapsto\mathtt{ET'}\vdash\mathtt{E[y]:ET}\wedge\Gamma\vdash\mathtt{e:ET'}\wedge\mathtt{y}\notin dom(\Gamma)$
\end_inset

 
\end_layout

\begin_layout Enumerate
\begin_inset Formula $\mathtt{y}\notin\mathit{dom}(\Gamma)\wedge\Gamma,\mathtt{y}\mapsto\mathtt{ET'}\vdash\mathtt{E[y]:ET}\wedge\Gamma\vdash\mathtt{e:ET'}\Rightarrow\Gamma\vdash\mathtt{E[e]:ET}$
\end_inset

 
\end_layout

\begin_layout Lemma
\begin_inset CommandInset label
LatexCommand label
name "lem:pco"

\end_inset

Properties of capability operators.
\end_layout

\begin_layout Lemma
\begin_inset Formula $\forall\kappa,\kappa_{1},\kappa_{2}:$
\end_inset


\end_layout

\begin_layout Enumerate
If 
\begin_inset Formula $\kappa_{1}\sim_{g}\kappa_{2}$
\end_inset

, then 
\begin_inset Formula $\kappa_{1}\sim_{l}\kappa_{2}.$
\end_inset


\end_layout

\begin_layout Enumerate
If 
\begin_inset Formula $\kappa_{1}\le\kappa_{2}$
\end_inset

, then
\begin_inset Separator latexpar
\end_inset


\end_layout

\begin_deeper
\begin_layout Enumerate
\begin_inset Formula $\kappa_{1}\sim_{l}\kappa\Rightarrow\kappa_{2}\sim_{l}\kappa$
\end_inset


\end_layout

\begin_layout Enumerate
\begin_inset Formula $\kappa_{1}\sim_{g}\kappa\Rightarrow\kappa_{2}\sim_{g}\kappa$
\end_inset


\end_layout

\end_deeper
\begin_layout Enumerate
If 
\begin_inset Formula $\kappa_{1}\sim_{l}\kappa_{2}$
\end_inset

, and both 
\begin_inset Formula $\kappa_{1}\triangleright\kappa$
\end_inset

 and 
\begin_inset Formula $\kappa_{2}\triangleright\kappa$
\end_inset

 are defined, then 
\begin_inset Formula $\kappa_{1}\triangleright\kappa\sim_{l}\kappa_{2}\triangleright\kappa$
\end_inset

.
\end_layout

\begin_layout Enumerate
If 
\begin_inset Formula $\kappa_{1}\sim_{g}\kappa_{2}$
\end_inset

, and both 
\begin_inset Formula $\kappa_{1}\triangleright\kappa$
\end_inset

 and 
\begin_inset Formula $\kappa_{2}\triangleright\kappa$
\end_inset

 are defined, then 
\begin_inset Formula $\kappa_{1}\triangleright\kappa\sim_{g}\kappa_{2}\triangleright\kappa$
\end_inset


\end_layout

\begin_layout Enumerate
\begin_inset Formula $\kappa_{2}\le\kappa_{1}\triangleright\kappa_{2}$
\end_inset

 or 
\begin_inset Formula $\kappa_{1}=\mathtt{val}$
\end_inset

 or 
\begin_inset Formula $\kappa_{1}\triangleright\kappa_{2}=\bot$
\end_inset

 
\end_layout

\begin_layout Enumerate
If 
\begin_inset Formula $\mathcal{A}(\kappa_{1})\le\kappa_{2}$
\end_inset

 then
\end_layout

\begin_deeper
\begin_layout Enumerate
\begin_inset Formula $\kappa_{1}\sim_{l}\kappa\Rightarrow\kappa_{2}\sim_{l}\kappa$
\end_inset


\end_layout

\begin_layout Enumerate
\begin_inset Formula $\kappa_{1}\sim_{g}\kappa\Rightarrow\kappa_{1}\sim_{g}\kappa$
\end_inset


\end_layout

\begin_layout Enumerate
\begin_inset Formula $\mathcal{A}(\kappa_{1}\triangleright\kappa)\le\kappa_{2}\triangleright\kappa$
\end_inset


\end_layout

\end_deeper
\begin_layout Enumerate
If 
\begin_inset Formula $\mathcal{A}(\kappa_{1})\le\kappa_{2}$
\end_inset

 and 
\begin_inset Formula $\mathcal{A}(\kappa_{2})\le\kappa_{4}$
\end_inset

 then
\end_layout

\begin_deeper
\begin_layout Enumerate
\begin_inset Formula $\kappa_{1}\sim_{l}\kappa_{2}\Rightarrow\kappa_{3}\sim_{l}\kappa_{4}$
\end_inset


\end_layout

\begin_layout Enumerate
\begin_inset Formula $\kappa_{1}\sim_{g}\kappa_{2}\Rightarrow\kappa_{3}\sim_{g}\kappa_{4}$
\end_inset


\end_layout

\end_deeper
\end_deeper
\begin_layout Proof
By case analysis on 
\begin_inset Formula $\kappa_{1}$
\end_inset

 and 
\begin_inset Formula $\kappa_{2}$
\end_inset

.
\end_layout

\begin_layout Standard
On the other hand, 
\begin_inset Formula $\kappa_{1}\le\kappa_{2}$
\end_inset

does not imply that 
\begin_inset Formula $\kappa\triangleright\kappa_{2}\le\kappa\triangleright\kappa_{2}$
\end_inset

.
 For example, 
\begin_inset Formula $\mathtt{iso}\le\mathtt{trn}$
\end_inset

, but 
\begin_inset Formula $\mathtt{box}\triangleright\mathtt{iso}=\mathtt{tag}\nleq\mathtt{box}\triangleright\mathtt{trn}=\mathtt{box}$
\end_inset

.
 Similarly, 
\begin_inset Formula $\kappa_{1}\le\kappa_{2}$
\end_inset

does not imply that 
\begin_inset Formula $\kappa_{1}\triangleright\kappa\le\kappa_{2}\triangleright\kappa$
\end_inset

; take 
\begin_inset Formula $\mathtt{iso}\triangleright\mathtt{trn}=\mathtt{tag}\nleq\mathtt{trn}\triangleright\mathtt{trn}=\mathtt{trn}.$
\end_inset

 Finally, the 
\begin_inset Formula $\triangleright$
\end_inset

 operator is not associative, i.e.
 
\begin_inset Formula $(\kappa_{1}\triangleright\kappa_{2})\triangleright\kappa_{3}\ne\kappa_{1}\triangleright(\kappa_{2}\triangleright\kappa_{3})$
\end_inset

.
 For example, 
\begin_inset Formula $(\mathtt{iso}\triangleright\mathtt{trn})\triangleright\mathtt{val}=\bot\ne\mathtt{iso}\triangleright(\mathtt{trn}\triangleright\mathtt{val})=\mathtt{val}$
\end_inset

.
\end_layout

\begin_layout Lemma
Properties of deep viewpoint adaptation.
\end_layout

\begin_layout Lemma
\begin_inset Formula $\forall\kappa,\kappa_{1}...,\kappa_{n}$
\end_inset

:
\end_layout

\begin_deeper
\begin_layout Enumerate
If 
\begin_inset Formula $\kappa_{1}\le\kappa_{2}$
\end_inset

then 
\begin_inset Formula $\kappa_{1}\blacktriangleright\kappa\le\kappa_{2}\triangleright\kappa$
\end_inset

, or 
\begin_inset Formula $\kappa_{2}=\mathtt{val}$
\end_inset

.
\end_layout

\begin_layout Enumerate
\begin_inset Formula $\kappa_{1}\blacktriangleright\kappa_{2}=\mathtt{val}$
\end_inset

 iff 
\begin_inset Formula $\kappa_{1}\triangleright\kappa_{2}=\mathtt{val}$
\end_inset

.
\end_layout

\begin_layout Enumerate
\begin_inset Formula $\kappa_{1}\blacktriangleright\kappa_{2}\le\kappa_{1}\triangleright\kappa_{2}$
\end_inset


\end_layout

\begin_layout Enumerate
\begin_inset Formula $(...(\kappa_{1}\blacktriangleright\kappa_{2})\blacktriangleright\kappa_{3}...)\blacktriangleright\kappa_{n}\le(...(\kappa_{1}\triangleright\kappa_{2})\triangleright\kappa_{3}...)\triangleright\kappa_{n}$
\end_inset


\end_layout

\begin_layout Enumerate
\begin_inset Formula $(...(\kappa_{1}\blacktriangleright\kappa_{2})\blacktriangleright\kappa_{3}...)\blacktriangleright\kappa_{n}=\mathtt{val}$
\end_inset

 iff 
\begin_inset Formula $(...(\kappa_{1}\triangleright\kappa_{2})\triangleright\kappa_{3}...)\triangleright\kappa_{n}=\mathtt{val}$
\end_inset


\end_layout

\begin_layout Enumerate
If 
\begin_inset Formula $\kappa_{1}\sim_{l}\kappa_{2}$
\end_inset

and 
\begin_inset Formula $\kappa_{1},\kappa_{2}\ne\mathtt{tag}$
\end_inset

, then 
\begin_inset Formula $\kappa_{1}\blacktriangleright\kappa\sim_{l}\kappa_{2}\blacktriangleright\kappa$
\end_inset

 or 
\begin_inset Formula $\kappa_{1}=\kappa_{2}=\mathtt{ref}$
\end_inset


\end_layout

\begin_layout Enumerate
If 
\begin_inset Formula $\kappa_{1}\sim_{g}\kappa_{2}$
\end_inset

and 
\begin_inset Formula $\kappa_{1},\kappa_{2}\ne\mathtt{tag}$
\end_inset

 then 
\begin_inset Formula $\kappa_{1}\blacktriangleright\kappa\sim_{g}\kappa_{2}\blacktriangleright\kappa$
\end_inset


\end_layout

\begin_layout Enumerate
If 
\begin_inset Formula $\mathcal{A}(\kappa_{1})\le\kappa_{2}$
\end_inset

 and 
\begin_inset Formula $\kappa_{1}\ne\kappa_{2}\ne\mathtt{tag}$
\end_inset

 then 
\begin_inset Formula $\mathcal{A}(\kappa_{1}\blacktriangleright\kappa)\le\kappa_{2}\blacktriangleright\kappa$
\end_inset


\end_layout

\begin_layout Lemma
\begin_inset CommandInset label
LatexCommand label
name "lem:CPP"

\end_inset

Capabilities are preserved along paths.
\end_layout

\begin_layout Lemma
If 
\begin_inset Formula $\Delta,\chi,\alpha\vdash\iota:\kappa,p$
\end_inset

 and 
\begin_inset Formula $\Delta,\chi,\alpha\vdash\iota:\kappa^{\prime},p$
\end_inset

 then 
\begin_inset Formula $\kappa=\kappa^{\prime}$
\end_inset

.
\end_layout

\end_deeper
\begin_layout Proof
By induction over the structure of 
\begin_inset Formula $p$
\end_inset

.
\end_layout

\begin_layout Subsection
New paths
\end_layout

\begin_layout Lemma
\begin_inset CommandInset label
LatexCommand label
name "lem:Simplification."

\end_inset

Simplification.
\end_layout

\begin_layout Lemma
If
\begin_inset Separator latexpar
\end_inset


\end_layout

\begin_deeper
\begin_layout Enumerate
\begin_inset Formula $\mathcal{A}(\kappa_{1}\,\phi)\le\kappa_{2}$
\end_inset


\end_layout

\begin_layout Enumerate
\begin_inset Formula $\kappa_{2}\le\kappa_{3}$
\end_inset


\end_layout

\begin_layout Enumerate
\begin_inset Formula $\kappa_{4}\triangleleft\kappa_{2}$
\end_inset

 or 
\begin_inset Formula $\kappa_{4}\triangleleft\kappa_{3}$
\end_inset


\end_layout

\end_deeper
\begin_layout Lemma
Then
\begin_inset Separator latexpar
\end_inset


\end_layout

\begin_deeper
\begin_layout Enumerate
\begin_inset ERT
status open

\begin_layout Plain Layout

[4.]
\backslash
setcounter{enumi}{4}
\end_layout

\end_inset


\begin_inset Formula $\mathcal{A}(\kappa_{1}\,\phi)\le\kappa_{3}$
\end_inset


\end_layout

\begin_layout Enumerate
\begin_inset Formula $\kappa_{4}\triangleleft\mathcal{A}(\kappa_{1}\,\phi)$
\end_inset

 or 
\begin_inset Formula $\kappa_{4}\triangleleft\kappa_{3}$
\end_inset


\end_layout

\end_deeper
\begin_layout Proof
(4) follows from (1) and (2).
 For (5), if 
\begin_inset Formula $\kappa_{4}\triangleleft\kappa_{3}$
\end_inset

, done.
 Otherwise, 
\begin_inset Formula $\kappa_{2}'=\mathcal{A}(\kappa_{1}\,\phi)$
\end_inset

.
 If 
\begin_inset Formula $\kappa_{4}=\mathtt{ref}$
\end_inset

, then for all 
\begin_inset Formula $\kappa_{1}\,\phi$
\end_inset

, 
\begin_inset Formula $\kappa_{4}\triangleleft\kappa_{2}'$
\end_inset

.
 If 
\begin_inset Formula $\kappa_{4}=\mathtt{trn}$
\end_inset

, then 
\begin_inset Formula $\kappa_{2}\in\{\mathtt{iso,trn,val,tag}\}\not\ni\kappa_{3}$
\end_inset

.
 If 
\begin_inset Formula $\kappa_{2}'\in\{\mathtt{iso,trn,val}\}$
\end_inset

 then 
\begin_inset Formula $\kappa_{1}\,\phi\in\{\mathtt{iso\circ,trn\circ,val}\}$
\end_inset

 and 
\begin_inset Formula $\mathtt{trn}\triangleleft\kappa_{2}'$
\end_inset

.
 If 
\begin_inset Formula $\kappa_{2}'=\mathtt{tag}$
\end_inset

 then 
\begin_inset Formula $\kappa_{3}=\mathtt{tag}$
\end_inset

, which contradicts 
\begin_inset Formula $\kappa_{4}\not\triangleleft\kappa_{3}$
\end_inset

.
 If 
\begin_inset Formula $\kappa_{4}=\mathtt{iso}$
\end_inset

, the same holds, except 
\begin_inset Formula $\kappa_{2}$
\end_inset

 cannot be 
\begin_inset Formula $\mathtt{trn}$
\end_inset

.
\end_layout

\begin_layout Definition
Unaliased types can be treated as base types.
\end_layout

\begin_layout Definition
\begin_inset Formula $\mathtt{ET'}\sqsubseteq\mathtt{ET}$
\end_inset

 iff 
\begin_inset Formula $\mathtt{ET'}=\mathtt{ET}$
\end_inset

, or 
\begin_inset Formula $\mathtt{ET'}=\mathtt{S}\,\kappa\circ$
\end_inset

 and 
\begin_inset Formula $\mathtt{ET}=\mathtt{S}\,\kappa$
\end_inset


\begin_inset Separator latexpar
\end_inset


\end_layout

\begin_deeper
\begin_layout Definition
\begin_inset CommandInset label
LatexCommand label
name "def:An-identifier-"

\end_inset

An identifier 
\begin_inset Formula $\mathtt{z}$
\end_inset

 is 
\emph on
aliased
\emph default
 in a runtime expression 
\begin_inset Formula $\mathtt{e}$
\end_inset

 iff 
\end_layout

\begin_layout Definition
\begin_inset Formula $\exists\mathtt{E[\cdot]},\mathtt{e'},\mathtt{f},\mathtt{\overline{y}},\mathtt{\overline{e}},\mathtt{n},\mathtt{S}$
\end_inset

 such that
\end_layout

\begin_layout Itemize
\begin_inset Formula $\mathtt{e\equiv E[x=z]}$
\end_inset

 or
\end_layout

\begin_layout Itemize
\begin_inset Formula $\mathtt{e\equiv E[e'.f=z]}$
\end_inset

 or
\end_layout

\begin_layout Itemize
\begin_inset Formula $\mathtt{e\equiv E[e'.n(\overline{y},z,\overline{e})]}$
\end_inset

 or
\end_layout

\begin_layout Itemize
\begin_inset Formula $\mathtt{e\equiv E[z.n(\overline{y})]}$
\end_inset

 or
\end_layout

\begin_layout Itemize
\begin_inset Formula $\mathtt{e\equiv E[S.k(\overline{y},z,\overline{e})]}$
\end_inset


\end_layout

\end_deeper
\begin_layout Lemma
\begin_inset CommandInset label
LatexCommand label
name "lem:Inversion."

\end_inset

Inversion.
\end_layout

\begin_layout Lemma
If 
\begin_inset Formula $\Gamma\vdash\mathtt{e:ET}$
\end_inset

 then
\begin_inset Separator latexpar
\end_inset


\end_layout

\begin_deeper
\begin_layout Enumerate
If 
\begin_inset Formula $\mathtt{e\equiv x}$
\end_inset

 then 
\begin_inset Formula $\Gamma(\mathtt{x})\sqsubseteq\mathtt{ET}$
\end_inset


\end_layout

\begin_layout Enumerate
If 
\family typewriter

\begin_inset Formula $\mathtt{e\equiv e_{1}.f}$
\end_inset


\family default
 then 
\begin_inset Formula $\exists\mathtt{S},\mathtt{S'},\kappa,\kappa'$
\end_inset

 such that 
\begin_inset Formula $\Gamma\vdash\mathtt{e_{1}:S\,\kappa}$
\end_inset

 and 
\begin_inset Formula $\mathcal{F}(\mathtt{S,f})=\mathtt{S'\,\kappa'}$
\end_inset

 and 
\begin_inset Formula $\mathtt{ET=S'\,\kappa\triangleright\kappa'}$
\end_inset

.
\end_layout

\begin_layout Enumerate
If 
\begin_inset Formula $\mathtt{e\equiv null}$
\end_inset

 then 
\begin_inset Formula $\exists\mathtt{S}$
\end_inset

 such that 
\begin_inset Formula $\mathtt{S\,iso\circ\sqsubseteq ET}$
\end_inset


\end_layout

\begin_layout Enumerate
If 
\begin_inset Formula $\mathtt{e\equiv e_{1};e_{2}}$
\end_inset

 then 
\begin_inset Formula $\exists\mathtt{ET_{1}}$
\end_inset

 such that 
\begin_inset Formula $\Gamma\vdash\mathtt{e_{1}:ET_{1}}$
\end_inset

 and 
\begin_inset Formula $\Gamma\vdash\mathtt{e_{2}:ET}$
\end_inset


\end_layout

\begin_layout Enumerate
If 
\begin_inset Formula $\mathtt{e\equiv x=e_{1}}$
\end_inset

 then 
\begin_inset Formula $\exists\mathtt{S,\kappa,\kappa',\phi}$
\end_inset

 such that 
\begin_inset Formula $\Gamma(\mathtt{x})=\mathtt{S\,\kappa}$
\end_inset

 and 
\begin_inset Formula $\Gamma\vdash\mathtt{e_{1}:S\,\kappa'\,\phi}$
\end_inset

 and 
\begin_inset Formula $\mathcal{A}(\kappa'\,\phi)\le\kappa$
\end_inset

 and 
\begin_inset Formula $\mathcal{U}(\mathtt{S\,\kappa})\sqsubseteq\mathtt{ET}$
\end_inset


\end_layout

\begin_layout Enumerate
If 
\begin_inset Formula $\mathtt{e\equiv e_{1}.f=e_{2}}$
\end_inset

 then 
\begin_inset Formula $\exists\mathtt{S_{1},S_{2},\kappa_{1},\kappa_{2},\phi}$
\end_inset

 such that
\begin_inset Newline newline
\end_inset


\begin_inset Formula $\Gamma\vdash\mathtt{e_{1}:S_{1}\,\kappa_{1}}$
\end_inset

 and 
\begin_inset Formula $\Gamma\vdash\mathtt{e_{2}:S_{2}\,\kappa_{2}\,\phi}$
\end_inset

 and
\begin_inset Newline newline
\end_inset


\begin_inset Formula $\mathcal{F}(\mathtt{S_{1},f})=\mathtt{S_{2}\,\kappa_{3}}$
\end_inset

 and 
\begin_inset Formula $\mathcal{A}(\kappa_{2}\,\phi)\le\kappa_{3}$
\end_inset

,
\begin_inset Newline newline
\end_inset

either 
\begin_inset Formula $\kappa_{1}\triangleleft\kappa_{3}$
\end_inset

 or 
\begin_inset Formula $\kappa_{1}\triangleleft\mathcal{A}(\kappa_{2}\,\phi)$
\end_inset

,
\begin_inset Newline newline
\end_inset

and 
\begin_inset Formula $\mathcal{U}(\mathtt{S_{2}\,\kappa_{1}\triangleright\kappa_{3}})\sqsubseteq\mathtt{ET}$
\end_inset


\end_layout

\begin_layout Enumerate
If 
\begin_inset Formula $\mathtt{e\equiv e_{0}.m(\overline{e})}$
\end_inset

 then 
\begin_inset Formula $\exists\mathtt{S_{0},\kappa_{0},\kappa_{0}',\phi,\overline{T},\overline{ET},ET'}$
\end_inset

 such that
\begin_inset Newline newline
\end_inset


\begin_inset Formula $\Gamma\vdash\mathtt{e_{0}:S_{0}\,\kappa_{0}\,\phi}$
\end_inset

 and 
\begin_inset Formula $\mathcal{A}(\kappa_{0}\,\phi)\le\kappa_{0}'$
\end_inset

 and
\begin_inset Newline newline
\end_inset


\begin_inset Formula $\mathcal{M}(\mathtt{S_{0},m})=(\mathtt{S_{0}\,\kappa_{0}',\overline{x:T},\_,ET'})$
\end_inset

 and
\begin_inset Newline newline
\end_inset


\begin_inset Formula $\Gamma\vdash\mathtt{e_{i}:ET_{i}}$
\end_inset

 and 
\begin_inset Formula $\mathcal{A}(\mathtt{ET_{i}})\le\mathtt{T_{i}}$
\end_inset

 and 
\begin_inset Formula $\mathtt{ET'\sqsubseteq ET}$
\end_inset


\end_layout

\begin_layout Enumerate
If 
\begin_inset Formula $\mathtt{e\equiv e_{0}.b(\overline{e})}$
\end_inset

 then 
\begin_inset Formula $\exists\mathtt{A,\kappa_{0},\kappa_{0}',\phi,\overline{T}}$
\end_inset

 such that
\begin_inset Newline newline
\end_inset


\begin_inset Formula $\Gamma\vdash\mathtt{e_{0}:A\,\kappa_{0}\,\phi}$
\end_inset

 and 
\begin_inset Formula $\mathcal{A}(\kappa_{0}\,\phi)\le\kappa_{0}'$
\end_inset

 and
\begin_inset Newline newline
\end_inset


\begin_inset Formula $\mathcal{M}(\mathtt{A,b})=(\mathtt{A\,ref,\overline{x:T},\_,A\,tag})$
\end_inset

 and
\begin_inset Newline newline
\end_inset


\begin_inset Formula $\mathit{sendable}(\mathtt{T_{i}})$
\end_inset

 and 
\begin_inset Formula $\Gamma\vdash\mathtt{e_{i}:ET_{i}}$
\end_inset

and 
\begin_inset Formula $\mathcal{A}(\mathtt{ET_{i}})\le\mathtt{T_{i}}$
\end_inset

 and 
\begin_inset Formula $\mathtt{A\,tag=ET}$
\end_inset


\end_layout

\begin_layout Enumerate
If 
\begin_inset Formula $\mathtt{e\equiv C.k(\overline{e})}$
\end_inset

then 
\begin_inset Formula $\exists\mathtt{\overline{ET},\overline{T}}$
\end_inset

 such that
\begin_inset Newline newline
\end_inset


\begin_inset Formula $\mathcal{M}(\mathtt{C,k})=(\mathtt{C\,ref,\overline{x:T},\_,C\,ref\circ})$
\end_inset

 and
\begin_inset Newline newline
\end_inset


\begin_inset Formula $\Gamma\vdash\mathtt{e_{i}:ET_{i}}$
\end_inset

and 
\begin_inset Formula $\mathcal{A}(\mathtt{ET_{i}})\le\mathtt{T_{i}}$
\end_inset

 and 
\begin_inset Formula $\mathtt{C\,ref\circ\sqsubseteq ET}$
\end_inset


\end_layout

\begin_layout Enumerate
If 
\begin_inset Formula $\mathtt{e\equiv A.k(\overline{e})}$
\end_inset

then 
\begin_inset Formula $\exists\mathtt{\overline{ET},\overline{T}}$
\end_inset

 such that
\begin_inset Newline newline
\end_inset


\begin_inset Formula $\mathcal{M}(\mathtt{A,k})=(\mathtt{A\,ref,\overline{x:T},\_,A\,tag})$
\end_inset

 and
\begin_inset Newline newline
\end_inset


\begin_inset Formula $\mathit{sendable}(\mathtt{T_{i}})$
\end_inset

 and 
\begin_inset Formula $\Gamma\vdash\mathtt{e_{i}:ET_{i}}$
\end_inset

and 
\begin_inset Formula $\mathcal{A}(\mathtt{ET_{i}})\le\mathtt{T_{i}}$
\end_inset

 and 
\begin_inset Formula $\mathtt{A\,tag=ET}$
\end_inset


\end_layout

\begin_layout Enumerate
If 
\begin_inset Formula $\mathtt{e\equiv recover\,e'}$
\end_inset

 then 
\begin_inset Formula $\exists\mathtt{ET'}$
\end_inset

 such that
\begin_inset Newline newline
\end_inset


\begin_inset Formula $\Gamma'=\Gamma\backslash\{\mathtt{x}\,|\,\neg\mathit{sendable}(\Gamma(\mathtt{x}))\}$
\end_inset

 and
\begin_inset Newline newline
\end_inset


\begin_inset Formula $\Gamma'\vdash\mathtt{e':ET'}$
\end_inset

 and 
\begin_inset Formula $\mathcal{R}(\mathtt{ET'})\sqsubseteq\mathtt{ET}$
\end_inset


\end_layout

\end_deeper
\begin_layout Proof
By induction on the typing of 
\begin_inset Formula $\Gamma\vdash\mathtt{e:ET}$
\end_inset

.
 For case 6 (field assignment), apply lemma 
\begin_inset CommandInset ref
LatexCommand ref
reference "lem:Simplification."

\end_inset

.
\end_layout

\begin_layout Lemma
\begin_inset CommandInset label
LatexCommand label
name "lem:Temporaries-and-variables"

\end_inset

Temporaries and variables with unique capabilities are unique.
\end_layout

\begin_layout Lemma
If
\begin_inset Separator latexpar
\end_inset


\end_layout

\begin_deeper
\begin_layout Enumerate
\begin_inset Formula $\mathit{WFV}(\Delta,\chi)$
\end_inset


\end_layout

\begin_layout Enumerate
\begin_inset Formula $\chi(\alpha,i,\mathtt{z})=\chi(\alpha',i',\mathtt{z'})=\iota$
\end_inset


\end_layout

\begin_layout Enumerate
\begin_inset Formula $\Delta(\alpha,i,\mathtt{z})=\mathtt{S\,\kappa\,\phi}$
\end_inset


\end_layout

\begin_layout Enumerate
\begin_inset Formula $\kappa\in\{\mathtt{iso,trn}\}$
\end_inset


\end_layout

\begin_layout Enumerate
\begin_inset Formula $\Delta,\chi,\alpha'\vdash\iota:\kappa',(i',\mathtt{z'})$
\end_inset


\end_layout

\end_deeper
\begin_layout Lemma
Then 
\begin_inset Formula $\alpha=\alpha'$
\end_inset

 and either 
\begin_inset Formula $\kappa\sim_{\ell}\kappa'$
\end_inset

 or 
\begin_inset Formula $(i,\mathtt{z})=(i',\mathtt{z'})$
\end_inset

.
\end_layout

\begin_layout Proof
Assume that 
\begin_inset Formula $\alpha\neq\alpha'$
\end_inset

.
 Then, by 
\begin_inset Formula $\mathit{WFV.1}$
\end_inset

, 
\begin_inset Formula $\kappa\sim_{g}\kappa'$
\end_inset

.
 This implies 
\begin_inset Formula $\kappa'=\mathtt{tag}$
\end_inset

, which contradicts 5.
 Therefore, 
\begin_inset Formula $\alpha=\alpha'$
\end_inset

 and 
\begin_inset Formula $\Delta,\chi,\alpha'\vdash\iota:\kappa,(i,\mathtt{z})$
\end_inset

.
 If 
\begin_inset Formula $\mathit{Stable}(\Delta,\alpha,(i,\mathtt{z}))$
\end_inset

 then by 
\begin_inset Formula $\mathit{WFV.2}$
\end_inset

, either 
\begin_inset Formula $\kappa\sim_{\ell}\kappa'$
\end_inset

 (done) or 
\begin_inset Formula $\chi,\alpha\vdash(i,\mathtt{z})\sim(i',\mathtt{z'})$
\end_inset

, which requires 
\begin_inset Formula $(i,\mathtt{z})=(i',\mathtt{z'})$
\end_inset

 (done).
 If 
\begin_inset Formula $\neg\mathit{Stable}(\Delta,\alpha,(i,\mathtt{z}))$
\end_inset

 then 
\begin_inset Formula $\mathtt{z=t}$
\end_inset

 and by 
\begin_inset Formula $\mathit{WFV.4}$
\end_inset

 either 
\begin_inset Formula $(i,\mathtt{z})=(i',\mathtt{z'})$
\end_inset

 (done) or 
\begin_inset Formula $\exists\iota',\kappa'',p',\mathtt{\overline{f}}$
\end_inset

 such that 
\begin_inset Formula $\kappa\le\kappa''$
\end_inset

 and 
\begin_inset Formula $\kappa''\in\{\mathtt{iso,trn}\}$
\end_inset

 and 
\begin_inset Formula $(i',\mathtt{z'})=p'\cdot\mathtt{\overline{f}}$
\end_inset

 and 
\begin_inset Formula $\Delta,\chi,\alpha\vdash\iota':\kappa'',p'$
\end_inset

 and 
\begin_inset Formula $\Delta,\chi,\iota'\vdash\iota:\kappa,(0,\mathtt{this})\cdot\mathtt{\overline{f}}$
\end_inset

, so 
\begin_inset Formula $\mathtt{\overline{f}=\epsilon}$
\end_inset

 and 
\begin_inset Formula $p'=(i',\mathtt{z'})$
\end_inset

 and 
\begin_inset Formula $\iota=\iota'$
\end_inset

.
 This gives us 
\begin_inset Formula $\Delta,\chi,\iota\vdash\iota:\kappa,(0,\mathtt{this})$
\end_inset

, which by the definition of visibility gives us 
\begin_inset Formula $\kappa=\mathtt{ref}$
\end_inset

, which contradicts (4) (done).
\end_layout

\begin_layout Lemma
\begin_inset CommandInset label
LatexCommand label
name "lem:Isolation-in-well-formed"

\end_inset

Isolation in well-formed visibility.
\end_layout

\begin_layout Lemma
If
\begin_inset Separator latexpar
\end_inset


\end_layout

\begin_deeper
\begin_layout Enumerate
\begin_inset Formula $\mathit{WFV}(\Delta,\chi)$
\end_inset


\end_layout

\begin_layout Enumerate
\begin_inset Formula $\Delta(\alpha,i,\mathtt{t})=\mathtt{S\,\kappa\,\phi}$
\end_inset

 and 
\begin_inset Formula $\chi(\alpha,i,\mathtt{t})=\iota$
\end_inset

 and 
\begin_inset Formula $\kappa\in\{\mathtt{iso,trn}\}$
\end_inset


\end_layout

\begin_layout Enumerate
\begin_inset Formula $\Delta,\chi,\alpha'\vdash\iota:\kappa',p$
\end_inset


\end_layout

\end_deeper
\begin_layout Lemma
Then
\begin_inset Separator latexpar
\end_inset


\end_layout

\begin_deeper
\begin_layout Enumerate
\begin_inset ERT
status open

\begin_layout Plain Layout

[4.]
\backslash
setcounter{enumi}{4}
\end_layout

\end_inset

If 
\begin_inset Formula $\kappa\,\phi=\mathtt{iso\circ}$
\end_inset

 then 
\begin_inset Formula $\alpha=\alpha'$
\end_inset

 and 
\begin_inset Formula $p=(i,\mathtt{t})$
\end_inset

.
\end_layout

\begin_layout Enumerate
If 
\begin_inset Formula $\kappa\,\phi=\mathtt{trn}\circ$
\end_inset

 then 
\begin_inset Formula $\alpha=\alpha'$
\end_inset

 and either 
\begin_inset Formula $p=(i,\mathtt{t})$
\end_inset

 or 
\begin_inset Formula $\kappa'=\mathtt{box}$
\end_inset

.
\end_layout

\begin_layout Enumerate
If 
\begin_inset Formula $\kappa\,\phi=\mathtt{iso}$
\end_inset

 then 
\begin_inset Formula $\alpha=\alpha'$
\end_inset

 and either 
\begin_inset Formula $p=(i,\mathtt{t})$
\end_inset

 or 
\begin_inset Formula $\exists\iota',\kappa'',p',\mathtt{\overline{f}}$
\end_inset

 such that 
\begin_inset Formula $\kappa\le\kappa''$
\end_inset

 and 
\begin_inset Formula $\kappa''\in\{\mathtt{iso,trn}\}$
\end_inset

 and 
\begin_inset Formula $p=p'\cdot\mathtt{\overline{f}}$
\end_inset

 and 
\begin_inset Formula $\Delta,\chi,\alpha\vdash\iota':\kappa'',p'$
\end_inset

 and 
\begin_inset Formula $\Delta,\chi,\iota'\vdash\iota:\mathtt{iso},\mathtt{\overline{f}}$
\end_inset

.
\end_layout

\begin_layout Enumerate
If 
\begin_inset Formula $\kappa\,\phi=\mathtt{trn}$
\end_inset

 then 
\begin_inset Formula $\alpha=\alpha'$
\end_inset

 and either 
\begin_inset Formula $p=(i,\mathtt{t})$
\end_inset

 or 
\begin_inset Formula $\kappa'=\mathtt{box}$
\end_inset

 or 
\begin_inset Formula $\exists\iota',p',\mathtt{\overline{f}}$
\end_inset

 such that 
\begin_inset Formula $p=p'\cdot\mathtt{\overline{f}}$
\end_inset

 and 
\begin_inset Formula $\Delta,\chi,\alpha\vdash\iota':\mathtt{trn},p'$
\end_inset

 and 
\begin_inset Formula $\Delta,\chi,\iota'\vdash\iota:\mathtt{trn},\mathtt{\overline{f}}$
\end_inset

.
\end_layout

\end_deeper
\begin_layout Proof
(4) and (5) follow from lemma 
\begin_inset CommandInset ref
LatexCommand ref
reference "lem:Temporaries-and-variables"

\end_inset

.
 (5) and (6) follow from lemma 
\begin_inset CommandInset ref
LatexCommand ref
reference "lem:Temporaries-and-variables"

\end_inset

 and 
\begin_inset Formula $\mathit{WFV.4}$
\end_inset

.
\end_layout

\begin_layout Lemma
\begin_inset CommandInset label
LatexCommand label
name "lem:Aliasing-and-replaceability."

\end_inset

Aliasing and replaceability.
\end_layout

\begin_layout Lemma
If
\begin_inset Separator latexpar
\end_inset


\end_layout

\begin_deeper
\begin_layout Enumerate
\begin_inset Formula $\Gamma\vdash\mathtt{e:ET}$
\end_inset

 and 
\begin_inset Formula $\mathtt{z}$
\end_inset

 is aliased in 
\begin_inset Formula $\mathtt{e}$
\end_inset


\end_layout

\begin_layout Enumerate
\begin_inset Formula $\mathtt{z}$
\end_inset

 does not appear more than once in 
\begin_inset Formula $\mathtt{e}$
\end_inset


\end_layout

\begin_layout Enumerate
\begin_inset Formula $\Gamma(\mathtt{z})$
\end_inset

 is not unaliased
\end_layout

\begin_layout Enumerate
\begin_inset Formula $\Gamma'=\Gamma[\mathtt{z}\mapsto\mathcal{A}(\Gamma(\mathtt{z}))]$
\end_inset


\end_layout

\end_deeper
\begin_layout Lemma
Then 
\begin_inset Formula $\Gamma'\vdash\mathtt{e:ET}$
\end_inset


\end_layout

\begin_layout Proof
By induction over the structure of 
\begin_inset Formula $\mathtt{e}$
\end_inset

.
 We apply lemma 
\begin_inset CommandInset ref
LatexCommand ref
reference "lem:Inversion."

\end_inset

.
 Moreover, we use the fact that 
\begin_inset Formula $\forall\kappa.\mathcal{A}(\mathcal{A}(\kappa))=\mathcal{A}(\kappa)$
\end_inset

.
 The base cases are expressions that can alias 
\begin_inset Formula $\mathtt{z}$
\end_inset

.
\begin_inset Separator latexpar
\end_inset


\end_layout

\begin_deeper
\begin_layout Itemize
If 
\begin_inset Formula $\mathtt{e\equiv x=z}$
\end_inset

 then, by lemma 
\begin_inset CommandInset ref
LatexCommand ref
reference "lem:Inversion."

\end_inset

, we obtain 
\begin_inset Formula $\Gamma(\mathtt{x})=\mathtt{S\,\kappa}$
\end_inset

 and 
\begin_inset Formula $\Gamma(\mathtt{z})=\mathtt{S}\,\kappa'\,\phi$
\end_inset

 and 
\begin_inset Formula $\phi\neq\circ$
\end_inset

 and 
\begin_inset Formula $\mathcal{A}(\kappa')\le\kappa$
\end_inset

.
 Therefore, we have 
\begin_inset Formula $\mathcal{A}(\mathcal{A}(\kappa'))\le\kappa$
\end_inset

 and so 
\begin_inset Formula $\Gamma'\vdash\mathtt{x=z:ET}$
\end_inset

.
\end_layout

\begin_layout Itemize
If 
\begin_inset Formula $\mathtt{e\equiv e'.f=z}$
\end_inset

 then, by lemma 
\begin_inset CommandInset ref
LatexCommand ref
reference "lem:Inversion."

\end_inset

, we obtain 
\begin_inset Formula $\Gamma\vdash\mathtt{e'}:\mathtt{S\,\kappa}$
\end_inset

 and 
\begin_inset Formula $\mathcal{F}(\mathtt{S,f})=\mathtt{S'\,\kappa'}$
\end_inset

 and 
\begin_inset Formula $\Gamma(\mathtt{z})=\mathtt{S'}\,\kappa''\,\phi$
\end_inset

 and 
\begin_inset Formula $\phi\neq\circ$
\end_inset

 and 
\begin_inset Formula $\mathcal{A}(\kappa'')\le\kappa'$
\end_inset

.
 Therefore, we have 
\begin_inset Formula $\mathcal{A}(\mathcal{A}(\kappa''))\le\kappa'$
\end_inset

 and so 
\begin_inset Formula $\Gamma'\vdash\mathtt{e'.f=z:ET}$
\end_inset

.
\end_layout

\begin_layout Itemize
If 
\begin_inset Formula $\mathtt{e\equiv e'.n(\overline{y},z,\overline{e})}$
\end_inset

 then, by lemma 
\begin_inset CommandInset ref
LatexCommand ref
reference "lem:Inversion."

\end_inset

, we obtain 
\begin_inset Formula $\Gamma\vdash\mathtt{e':S\,\kappa}$
\end_inset

 and 
\begin_inset Formula $\mathcal{M}(\mathtt{S,n})=(\_,\mathtt{\overline{x:S\,\kappa}},\_,\_)$
\end_inset

 and 
\begin_inset Formula $\Gamma(\mathtt{z})=\mathtt{S_{i}\,\kappa_{i}'\,\phi}$
\end_inset

 and and 
\begin_inset Formula $\phi\neq\circ$
\end_inset

 and 
\begin_inset Formula $\mathcal{A}(\kappa_{i}')\le\kappa_{i}$
\end_inset

.
 Therefore, we have 
\begin_inset Formula $\mathcal{A}(\mathcal{A}(\kappa_{i}'))\le\kappa_{i}$
\end_inset

 and so 
\begin_inset Formula $\Gamma'\vdash\mathtt{e'.n(\overline{y},z,\overline{e}):ET}$
\end_inset

.
\end_layout

\begin_layout Itemize
If 
\begin_inset Formula $\mathtt{e\equiv z.n(\overline{y})}$
\end_inset

 then, by lemma 
\begin_inset CommandInset ref
LatexCommand ref
reference "lem:Inversion."

\end_inset

, we obtain 
\begin_inset Formula $\Gamma(\mathtt{z})=\mathtt{S\,\kappa\,\phi}$
\end_inset

 and 
\begin_inset Formula $\phi\neq\circ$
\end_inset

 and 
\begin_inset Formula $\mathcal{M}(\mathtt{S,n)}=(\mathtt{S\,\kappa'})$
\end_inset

 and 
\begin_inset Formula $\mathcal{A}(\kappa)\le(\kappa')$
\end_inset

.
 Therefore, we have 
\begin_inset Formula $\mathcal{A}(\mathcal{A}(\kappa))\le\kappa'$
\end_inset

 and so 
\begin_inset Formula $\Gamma'\vdash\mathtt{z.n(\overline{y}):ET}$
\end_inset

.
\end_layout

\begin_layout Itemize
If 
\begin_inset Formula $\mathtt{e\equiv S.k(\overline{y},z,\overline{e})}$
\end_inset

then, by lemma 
\begin_inset CommandInset ref
LatexCommand ref
reference "lem:Inversion."

\end_inset

, we obtain 
\begin_inset Formula $\mathcal{M}(\mathtt{S,k})=(\_,\mathtt{\overline{x:S\,\kappa}},\_,\_)$
\end_inset

 and 
\begin_inset Formula $\Gamma(\mathtt{z})=\mathtt{S_{i}\,\kappa_{i}'\,\phi}$
\end_inset

 and and 
\begin_inset Formula $\phi\neq\circ$
\end_inset

 and 
\begin_inset Formula $\mathcal{A}(\kappa_{i}')\le\kappa_{i}$
\end_inset

.
 Therefore, we have 
\begin_inset Formula $\mathcal{A}(\mathcal{A}(\kappa_{i}'))\le\kappa_{i}$
\end_inset

 and so 
\begin_inset Formula $\Gamma'\vdash\mathtt{S.k(\overline{y},z,\overline{e}):ET}$
\end_inset

.
\end_layout

\end_deeper
\begin_layout Proof
For the inductive step, if 
\begin_inset Formula $\mathtt{e\equiv E[e']}$
\end_inset

and 
\begin_inset Formula $\mathtt{z}$
\end_inset

 is aliased in 
\begin_inset Formula $\mathtt{e}$
\end_inset

, then, by lemma 
\begin_inset CommandInset ref
LatexCommand ref
reference "lem:Context-lemma."

\end_inset

, we obtain that 
\begin_inset Formula $\exists\mathtt{ET',y\notin\Gamma}$
\end_inset

 such that 
\begin_inset Formula $\Gamma\vdash\mathtt{e':ET'}$
\end_inset

 and 
\begin_inset Formula $\Gamma[\mathtt{y}\mapsto\mathtt{ET'}]\vdash\mathtt{E[y]:ET}$
\end_inset

, and so 
\begin_inset Formula $\Gamma'\vdash\mathtt{e':ET'}$
\end_inset

.
 Therefore, by lemma 
\begin_inset CommandInset ref
LatexCommand ref
reference "lem:Context-lemma."

\end_inset

, we obtain 
\begin_inset Formula $\Gamma'\vdash\mathtt{E[e']:ET}$
\end_inset

.
\end_layout

\begin_layout Lemma
Origins of temporary identifiers.
\end_layout

\begin_layout Lemma
If
\begin_inset Separator latexpar
\end_inset


\end_layout

\begin_deeper
\begin_layout Enumerate
\begin_inset Formula $\mathtt{z}$
\end_inset

 appears once in expression 
\begin_inset Formula $\mathtt{e}$
\end_inset


\end_layout

\begin_layout Enumerate
\begin_inset Formula $\mathtt{z}$
\end_inset

 is not aliased in 
\begin_inset Formula $\mathtt{e}$
\end_inset


\end_layout

\end_deeper
\begin_layout Lemma
Then 
\begin_inset Formula $\exists\mathtt{E'}$
\end_inset

 such that
\begin_inset Separator latexpar
\end_inset


\end_layout

\begin_deeper
\begin_layout Enumerate
\begin_inset ERT
status open

\begin_layout Plain Layout

[3.]
\backslash
setcounter{enumi}{3}
\end_layout

\end_inset


\begin_inset Formula $\mathtt{e\equiv E'[z.f]}$
\end_inset

, or
\end_layout

\begin_layout Enumerate
\begin_inset Formula $\mathtt{e\equiv E'[z.f=e']}$
\end_inset

, or
\end_layout

\begin_layout Enumerate
\begin_inset Formula $\mathtt{e\equiv E'[recover\,z]}$
\end_inset

, or
\end_layout

\end_deeper
\begin_layout Proof
By application of definition 
\begin_inset CommandInset ref
LatexCommand ref
reference "def:An-identifier-"

\end_inset

.
\end_layout

\begin_layout Lemma
If 
\begin_inset Formula $\Gamma,\mathtt{x:T_{1}\vdash e:ET_{1}}$
\end_inset

 and 
\begin_inset Formula $\mathcal{A}(\mathtt{T_{2}})\le\mathtt{T_{1}}$
\end_inset

 then 
\begin_inset Formula $\exists\mathtt{ET_{2}}.\Gamma,\mathtt{x:T_{2}\vdash e:ET_{2}}$
\end_inset

 and 
\begin_inset Formula $\mathtt{ET_{1}=ET_{2}}$
\end_inset

 or 
\begin_inset Formula $\mathcal{A}(\mathtt{ET_{2}})\le\mathtt{ET_{1}}$
\end_inset


\end_layout

\begin_layout Proof
By structural induction on the typing and lemma 
\begin_inset CommandInset ref
LatexCommand ref
reference "lem:pco"

\end_inset

.
\end_layout

\begin_layout Lemma
New paths through field read.
\end_layout

\begin_layout Lemma
If
\end_layout

\begin_deeper
\begin_layout Enumerate
\begin_inset Formula $\chi(\alpha,i,\mathtt{z})=\iota$
\end_inset


\end_layout

\begin_layout Enumerate
\begin_inset Formula $\Delta(\alpha,i,\mathtt{z})=\mathtt{S\,\kappa\,\phi}$
\end_inset


\end_layout

\begin_layout Enumerate
\begin_inset Formula $\chi(\iota,\mathtt{f})=\iota'$
\end_inset

 and 
\begin_inset Formula $\mathcal{F}(\mathtt{S,f})=\mathtt{S'\,\kappa'}$
\end_inset


\end_layout

\begin_layout Enumerate
\begin_inset Formula $\mathtt{T=\bot}$
\end_inset

 if 
\begin_inset Formula $\mathtt{z=t'}$
\end_inset

, 
\begin_inset Formula $\mathtt{S\,\kappa}$
\end_inset

 otherwise
\end_layout

\begin_layout Enumerate
\begin_inset Formula $\Delta'=\Delta[(\alpha,i,\mathtt{z})\mapsto\mathtt{T},(\alpha,i,\mathtt{t})\mapsto\mathtt{S'\,\kappa\triangleright\kappa'})]$
\end_inset


\end_layout

\begin_layout Enumerate
\begin_inset Formula $\mathcal{T}(\Delta(\alpha,i))\subseteq\{\mathtt{z}\}$
\end_inset


\end_layout

\end_deeper
\begin_layout Lemma
Then
\begin_inset Separator latexpar
\end_inset


\end_layout

\begin_deeper
\begin_layout Enumerate
\begin_inset ERT
status open

\begin_layout Plain Layout

[7.]
\backslash
setcounter{enumi}{7}
\end_layout

\end_inset


\begin_inset Formula $\forall\alpha',\iota'',\kappa'',p'$
\end_inset

 if 
\begin_inset Formula $\Delta',\chi,\alpha'\vdash\iota'',\kappa'',p'$
\end_inset

 then
\end_layout

\begin_deeper
\begin_layout Enumerate
\begin_inset Formula $\Delta,\chi,\alpha'\vdash\iota'':\kappa'',p'$
\end_inset

 or
\end_layout

\begin_layout Enumerate
\begin_inset Formula $\alpha'=\alpha$
\end_inset

 and 
\begin_inset Formula $\exists\mathtt{\overline{f}},\overline{\kappa}$
\end_inset

 such that
\begin_inset Separator latexpar
\end_inset


\end_layout

\begin_deeper
\begin_layout Enumerate
\begin_inset Formula $p'=(i,\mathtt{t})\cdot\mathtt{\overline{f}}$
\end_inset

 
\end_layout

\begin_layout Enumerate
\begin_inset Formula $\kappa''=\kappa\triangleright\kappa'\overline{\blacktriangleright\kappa}$
\end_inset


\end_layout

\begin_layout Enumerate
\begin_inset Formula $\Delta,\chi,\alpha\vdash\iota'':\kappa\blacktriangleright\kappa'\overline{\blacktriangleright\kappa},(i,\mathtt{z})\cdot\mathtt{f\cdot\overline{f}}$
\end_inset


\end_layout

\end_deeper
\end_deeper
\begin_layout Enumerate
If 
\begin_inset Formula $\mathit{WFV}(\Delta,\chi)$
\end_inset

 then 
\begin_inset Formula $\mathit{WFV}(\Delta',\chi)$
\end_inset

 and 
\begin_inset Formula $\mathcal{T}(\Delta'(\alpha,i))\subseteq\{\mathtt{t}\}$
\end_inset


\end_layout

\begin_layout Lemma
New paths through local assignment.
\end_layout

\begin_layout Lemma
If
\end_layout

\begin_layout Enumerate
\begin_inset Formula $\chi(\alpha,i,\mathtt{z})=\iota$
\end_inset

 and 
\begin_inset Formula $\chi(\alpha,i,\mathtt{x})=\iota'$
\end_inset

 and 
\begin_inset Formula $\mathtt{t}\notin\chi(\alpha,i)$
\end_inset


\end_layout

\begin_layout Enumerate
\begin_inset Formula $\Delta(\alpha,i,\mathtt{z})=\mathtt{S\,\kappa\,\phi}$
\end_inset

 and 
\begin_inset Formula $\Delta(\alpha,i,\mathtt{x})=\mathtt{S\,\kappa'}$
\end_inset


\end_layout

\begin_layout Enumerate
\begin_inset Formula $\chi'=\chi[(\alpha,i,\mathtt{x})\mapsto\iota,(\alpha,i,\mathtt{t})\mapsto\iota']$
\end_inset


\end_layout

\begin_layout Enumerate
\begin_inset Formula $\mathtt{T=\bot}$
\end_inset

 if 
\begin_inset Formula $\mathtt{z=t'}$
\end_inset

, 
\begin_inset Formula $\mathtt{S\,\kappa}$
\end_inset

 otherwise
\end_layout

\begin_layout Enumerate
\begin_inset Formula $\Delta'=\Delta[(\alpha,i,\mathtt{z})\mapsto\mathtt{T},(\alpha,i,\mathtt{t})\mapsto\mathcal{U}(\mathtt{S\,\kappa'})]$
\end_inset


\end_layout

\begin_layout Enumerate
\begin_inset Formula $\mathcal{T}(\Delta(\alpha,i))\subseteq\{\mathtt{z}\}$
\end_inset


\end_layout

\end_deeper
\begin_layout Lemma
Then
\begin_inset Separator latexpar
\end_inset


\end_layout

\begin_deeper
\begin_layout Enumerate
\begin_inset ERT
status open

\begin_layout Plain Layout

[7.]
\backslash
setcounter{enumi}{7}
\end_layout

\end_inset


\begin_inset Formula $\forall\alpha',\iota'',\kappa'',p$
\end_inset

 if 
\begin_inset Formula $\Delta',\chi',\alpha'\vdash\iota'':\kappa'',p$
\end_inset

 then
\begin_inset Separator latexpar
\end_inset


\end_layout

\begin_deeper
\begin_layout Enumerate
\begin_inset Formula $\Delta,\chi,\alpha'\vdash\iota'':\kappa'',p$
\end_inset

 or
\end_layout

\begin_layout Enumerate
\begin_inset Formula $\alpha=\alpha'$
\end_inset

 and 
\begin_inset Formula $\exists\mathtt{\overline{f}},\overline{\kappa}$
\end_inset

 such that
\end_layout

\begin_deeper
\begin_layout Enumerate
\begin_inset Formula $p=(i,\mathtt{x})\cdot\mathtt{\overline{f}}$
\end_inset

 and 
\begin_inset Formula $\kappa''=\kappa'\overline{\blacktriangleright\kappa}$
\end_inset

 and
\begin_inset Newline newline
\end_inset


\begin_inset Formula $\Delta,\chi,\alpha\vdash\iota'':\kappa\overline{\blacktriangleright\kappa},(i,\mathtt{z})\cdot\mathtt{\overline{f}}$
\end_inset

, or
\end_layout

\begin_layout Enumerate
\begin_inset Formula $p=(i\cdot\mathtt{t})\cdot\mathtt{\overline{f}}$
\end_inset

 and 
\begin_inset Formula $\kappa''=\kappa'\overline{\blacktriangleright\kappa}$
\end_inset

 and
\begin_inset Newline newline
\end_inset


\begin_inset Formula $\Delta,\chi,\alpha\vdash\iota'':\kappa'\overline{\blacktriangleright\kappa},(i,\mathtt{x})\cdot\mathtt{\overline{f}}$
\end_inset


\end_layout

\end_deeper
\end_deeper
\begin_layout Enumerate
If 
\begin_inset Formula $\mathcal{A}(\kappa\,\phi)\le\kappa'$
\end_inset

 and 
\begin_inset Formula $\mathit{WFV}(\Delta,\chi)$
\end_inset

 then 
\begin_inset Formula $\mathit{WFV}(\Delta',\chi')$
\end_inset

 and 
\begin_inset Formula $\mathcal{T}(\Delta'(\alpha,i))\subseteq\{\mathtt{t}\}$
\end_inset


\end_layout

\begin_layout Lemma
New paths through field assignment.
\end_layout

\begin_layout Lemma
If
\end_layout

\begin_layout Enumerate
\begin_inset Formula $\chi(\alpha,i,\mathtt{z})=\iota$
\end_inset

 and 
\begin_inset Formula $\chi(\alpha,i,\mathtt{z'})=\iota'$
\end_inset

 
\end_layout

\begin_layout Enumerate
\begin_inset Formula $\Delta(\alpha,i,\mathtt{z})=\mathtt{S\,\kappa\,\phi}$
\end_inset

 and 
\begin_inset Formula $\Delta(\alpha,i,\mathtt{z'})=\mathtt{S'\,\kappa'\,\phi'}$
\end_inset

 
\end_layout

\begin_layout Enumerate
\begin_inset Formula $\chi(\iota,\mathtt{f})=\iota''$
\end_inset

 and 
\begin_inset Formula $\mathcal{F}(\mathtt{S,f})=\mathtt{S'\,\kappa''}$
\end_inset


\end_layout

\begin_layout Enumerate
\begin_inset Formula $\chi'=\chi[(\iota,\mathtt{f})\mapsto\iota',(\alpha,i,\mathtt{t})\mapsto\iota'']$
\end_inset


\end_layout

\begin_layout Enumerate
\begin_inset Formula $\mathtt{T=\bot}$
\end_inset

 if 
\begin_inset Formula $\mathtt{z=t'}$
\end_inset

, 
\begin_inset Formula $\mathtt{S\,\kappa}$
\end_inset

 otherwise
\end_layout

\begin_layout Enumerate
\begin_inset Formula $\mathtt{T'=\bot}$
\end_inset

 if 
\begin_inset Formula $\mathtt{z'=t''}$
\end_inset

, 
\begin_inset Formula $\mathtt{S'\,\kappa'}$
\end_inset

 otherwise
\end_layout

\begin_layout Enumerate
\begin_inset Formula $\Delta'=\Delta[(\alpha,i,\mathtt{z})\mapsto\mathtt{T},(\alpha,i,\mathtt{z'})\mapsto\mathtt{T'},(\alpha,i,\mathtt{t})\mapsto\mathcal{U}(\mathtt{S'\,\kappa\triangleright\kappa''})]$
\end_inset


\end_layout

\begin_layout Enumerate
\begin_inset Formula $\mathcal{T}(\Delta(\alpha,i))\subseteq\{\mathtt{z,z'}\}$
\end_inset


\end_layout

\end_deeper
\begin_layout Lemma
Then
\end_layout

\begin_deeper
\begin_layout Enumerate
\begin_inset ERT
status open

\begin_layout Plain Layout

[9.]
\backslash
setcounter{enumi}{9}
\end_layout

\end_inset


\begin_inset Formula $\forall\alpha',\iota''',\kappa''',p'$
\end_inset

 if 
\begin_inset Formula $\Delta',\chi',\alpha'\vdash\iota''':\kappa''',p'$
\end_inset

 then
\end_layout

\begin_deeper
\begin_layout Enumerate
\begin_inset Formula $\Delta,\chi,\alpha'\vdash\iota''':\kappa''',p'$
\end_inset

 or
\end_layout

\begin_layout Enumerate
\begin_inset Formula $\alpha'=\alpha$
\end_inset

 and 
\begin_inset Formula $\exists\mathtt{\overline{f}},\overline{\kappa}$
\end_inset

 such that
\begin_inset Separator latexpar
\end_inset


\end_layout

\begin_deeper
\begin_layout Enumerate
\begin_inset Formula $\kappa'''=\kappa\blacktriangleright\kappa''\overline{\blacktriangleright\kappa}$
\end_inset

 and 
\begin_inset Formula $p'=(i,\mathtt{z})\cdot\mathtt{f\cdot\overline{f}}$
\end_inset

 and 
\begin_inset Formula $\Delta,\chi,\alpha\vdash\iota''':\kappa'\overline{\blacktriangleright\kappa},(i,\mathtt{z'})\cdot\mathtt{\overline{f}}$
\end_inset

, or
\end_layout

\begin_layout Enumerate
\begin_inset Formula $\kappa'''=\mathcal{U}(\kappa\triangleright\kappa'')\overline{\blacktriangleright\kappa}$
\end_inset

 and 
\begin_inset Formula $p'=(i,\mathtt{t})\cdot\mathtt{\overline{f}}$
\end_inset

 and 
\begin_inset Formula $\Delta,\chi,\alpha\vdash\iota''':\kappa\blacktriangleright\kappa''\overline{\blacktriangleright\kappa},(i,\mathtt{z})\cdot\mathtt{f\cdot\overline{f}}$
\end_inset

, or
\end_layout

\begin_layout Enumerate
\begin_inset Formula $\exists\kappa'''',p\neq(i,\mathtt{z})$
\end_inset

 such that 
\begin_inset Formula $\kappa'''=\kappa''''\blacktriangleright\kappa''\overline{\blacktriangleright\kappa}$
\end_inset

 and 
\begin_inset Formula $p'=p\cdot\mathtt{f\cdot\overline{f}}$
\end_inset

 and 
\begin_inset Formula $\Delta,\chi,\alpha\vdash\iota:\kappa'''',p$
\end_inset


\end_layout

\end_deeper
\end_deeper
\begin_layout Enumerate
If 
\begin_inset Formula $\mathcal{A}(\kappa'\,\phi')\le\kappa''$
\end_inset

 and (
\begin_inset Formula $\kappa\triangleleft\kappa'$
\end_inset

 or 
\begin_inset Formula $\kappa\triangleleft\kappa''$
\end_inset

) and 
\begin_inset Formula $\mathit{WFV}(\Delta,\chi)$
\end_inset

 then 
\begin_inset Formula $\mathit{WFV}(\Delta',\chi')$
\end_inset

 and 
\begin_inset Formula $\mathcal{T}(\Delta'(\alpha,i))=\emptyset$
\end_inset


\end_layout

\begin_layout Lemma
New paths through message passing.
\end_layout

\begin_layout Lemma
If
\end_layout

\begin_layout Enumerate
\begin_inset Formula $\chi(\alpha,i,\mathtt{z})=\iota$
\end_inset

 and 
\begin_inset Formula $\Delta(\alpha,i,\mathtt{z})=\mathtt{S\,\kappa\,\phi}$
\end_inset


\end_layout

\begin_layout Enumerate
\begin_inset Formula $\chi'=\chi[(\alpha',-j,\mathtt{x})\mapsto\iota]$
\end_inset


\end_layout

\begin_layout Enumerate
\begin_inset Formula $\mathtt{T=\bot}$
\end_inset

 if 
\begin_inset Formula $\mathtt{z=t}$
\end_inset

, 
\begin_inset Formula $\mathtt{S\,\kappa}$
\end_inset

 otherwise
\end_layout

\begin_layout Enumerate
\begin_inset Formula $\Delta'=\Delta[(\alpha,i,\mathtt{z})\mapsto\mathtt{T},(\alpha',-j,\mathtt{x})\mapsto\mathtt{S\,\kappa'}]$
\end_inset


\end_layout

\begin_layout Enumerate
\begin_inset Formula $\mathcal{T}(\Delta(\alpha,i))\subseteq\{\mathtt{z}\}$
\end_inset


\end_layout

\end_deeper
\begin_layout Lemma
Then
\begin_inset Separator latexpar
\end_inset


\end_layout

\begin_deeper
\begin_layout Enumerate
\begin_inset ERT
status open

\begin_layout Plain Layout

[6.]
\backslash
setcounter{enumi}{6}
\end_layout

\end_inset


\begin_inset Formula $\forall\alpha'',\iota'',\kappa'',p$
\end_inset

 if 
\begin_inset Formula $\Delta',\chi',\alpha''\vdash\iota'':\kappa'',p$
\end_inset

 then
\end_layout

\begin_deeper
\begin_layout Enumerate
\begin_inset Formula $\Delta,\chi,\alpha''\vdash\iota'':\kappa'',p$
\end_inset

 or
\end_layout

\begin_layout Enumerate
\begin_inset Formula $\alpha''=\alpha'$
\end_inset

 and 
\begin_inset Formula $\exists\mathtt{\overline{f}},\overline{\kappa}$
\end_inset

 such that
\end_layout

\begin_deeper
\begin_layout Enumerate
\begin_inset Formula $p=(-j,\mathtt{x})\cdot\mathtt{\overline{f}}$
\end_inset

 
\end_layout

\begin_layout Enumerate
\begin_inset Formula $\kappa''=\kappa'\overline{\blacktriangleright\kappa}$
\end_inset


\end_layout

\begin_layout Enumerate
\begin_inset Formula $\Delta,\chi,\alpha\vdash\iota'':\kappa\overline{\blacktriangleright\kappa},(i,\mathtt{z})\cdot\mathtt{\overline{f}}$
\end_inset


\end_layout

\end_deeper
\end_deeper
\begin_layout Enumerate
If 
\begin_inset Formula $\mathcal{A}(\kappa\,\phi)\le\kappa'$
\end_inset

 and 
\begin_inset Formula $\mathit{sendable}(\kappa')$
\end_inset

 and 
\begin_inset Formula $\mathit{WFV}(\Delta,\chi)$
\end_inset

 then 
\begin_inset Formula $\mathit{WFV}(\Delta',\chi')$
\end_inset

 and 
\begin_inset Formula $\mathcal{T}(\Delta'(\alpha,i))=\emptyset$
\end_inset


\end_layout

\end_deeper
\begin_layout Subsection
Preservation of well-formedness
\end_layout

\begin_layout Lemma
\begin_inset CommandInset label
LatexCommand label
name "lem:SL1"

\end_inset

Type preservation on same frame.
\end_layout

\begin_layout Lemma
For all heaps 
\begin_inset Formula $\chi$
\end_inset

, actors 
\begin_inset Formula $\alpha$
\end_inset

, global type environments 
\begin_inset Formula $\Delta$
\end_inset

, frames 
\begin_inset Formula $\varphi,$
\end_inset

 stacks 
\begin_inset Formula $\sigma$
\end_inset

 and expressions 
\begin_inset Formula $\mathtt{e}$
\end_inset

, if
\end_layout

\begin_deeper
\begin_layout Enumerate
\begin_inset Formula $\chi(\alpha)=(\_,\_,\_,\alpha\cdot\overline{\varphi}\cdot\varphi,\mathtt{E[e]})$
\end_inset

 and 
\begin_inset Formula $|\bar{\varphi}|=i-1$
\end_inset


\end_layout

\begin_layout Enumerate
\begin_inset Formula $\chi,\alpha\cdot\overline{\varphi}\cdot\varphi,\mathtt{e}\rightsquigarrow\chi'',\alpha\cdot\overline{\varphi}\cdot\varphi',\mathtt{e'}$
\end_inset


\end_layout

\begin_layout Enumerate
\begin_inset Formula $\chi'=\chi''[\alpha\mapsto(\alpha\cdot\overline{\varphi}\cdot\varphi,\mathtt{E[e']})]$
\end_inset


\end_layout

\begin_layout Enumerate
\begin_inset Formula $\Delta(\alpha,i)\vdash\mathtt{e:ET}$
\end_inset


\end_layout

\begin_layout Enumerate
\begin_inset Formula $\Delta\vdash\chi\diamond$
\end_inset


\end_layout

\end_deeper
\begin_layout Lemma
Then 
\begin_inset Formula $\exists\Delta^{\prime}$
\end_inset

 such that
\end_layout

\begin_deeper
\begin_layout Enumerate
\begin_inset Formula $\Delta'(\alpha,i)\vdash\mathtt{e':ET}$
\end_inset


\end_layout

\begin_layout Enumerate
\begin_inset Formula $\Delta'\vdash\chi'\diamond$
\end_inset


\end_layout

\begin_layout Lemma
\begin_inset CommandInset label
LatexCommand label
name "lem:SL2"

\end_inset

Type preservation for method call.
\end_layout

\begin_layout Lemma
For all heaps 
\begin_inset Formula $\chi$
\end_inset

 and actors 
\begin_inset Formula $\alpha$
\end_inset

, if
\end_layout

\begin_layout Enumerate
\begin_inset Formula $\chi(\alpha)=(\_,\_,\_,\sigma\cdot\varphi,\mathtt{E[e]})$
\end_inset


\end_layout

\begin_layout Enumerate
\begin_inset Formula $\chi,\sigma\cdot\varphi,\mathtt{e}\rightsquigarrow\chi'',\sigma\cdot\varphi\cdot\varphi',\mathtt{e'}$
\end_inset


\end_layout

\begin_layout Enumerate
\begin_inset Formula $\chi'=\chi''[\alpha\mapsto(\sigma\cdot\varphi\cdot\varphi',\mathtt{E[e']})]$
\end_inset


\end_layout

\begin_layout Enumerate
\begin_inset Formula $\Delta\vdash\chi\diamond$
\end_inset


\end_layout

\end_deeper
\begin_layout Lemma
Then 
\begin_inset Formula $\exists\Delta^{\prime}$
\end_inset

 such that 
\begin_inset Formula $\Delta'\vdash\chi'\diamond$
\end_inset

.
\end_layout

\begin_deeper
\begin_layout Lemma
\begin_inset CommandInset label
LatexCommand label
name "lem:Type-preservation-upon"

\end_inset

Type preservation upon method return
\end_layout

\begin_layout Lemma
For all heaps 
\begin_inset Formula $\chi$
\end_inset

 and actors 
\begin_inset Formula $\alpha$
\end_inset

, if
\end_layout

\begin_layout Enumerate
\begin_inset Formula $\chi(\alpha)=(\_,\_,\_,\sigma\cdot\varphi\cdot\varphi',\mathtt{z})$
\end_inset


\end_layout

\begin_layout Enumerate
\begin_inset Formula $\mathtt{t}\notin\varphi$
\end_inset

 and 
\begin_inset Formula $\varphi''=\varphi[\mathtt{t}\mapsto\varphi'(\mathtt{z})]$
\end_inset


\end_layout

\begin_layout Enumerate
\begin_inset Formula $\varphi'=(\_,\_,\mathtt{E[\cdot]})$
\end_inset


\end_layout

\begin_layout Enumerate
\begin_inset Formula $\chi'=\chi[\alpha\mapsto(\sigma\cdot\varphi'',\mathtt{E[t]})]$
\end_inset


\end_layout

\begin_layout Enumerate
\begin_inset Formula $\Delta\vdash\chi\diamond$
\end_inset


\end_layout

\end_deeper
\begin_layout Lemma
Then 
\begin_inset Formula $\exists\Delta^{\prime}$
\end_inset

 such that 
\begin_inset Formula $\Delta'\vdash\chi'\diamond$
\end_inset

.
\end_layout

\begin_deeper
\begin_layout Lemma
\begin_inset CommandInset label
LatexCommand label
name "lem:Type-preservation-upon-1"

\end_inset

Type preservation upon message handling.
\end_layout

\begin_layout Lemma
For all heaps 
\begin_inset Formula $\chi$
\end_inset

 and actors 
\begin_inset Formula $\alpha$
\end_inset

, if
\end_layout

\begin_layout Enumerate
\begin_inset Formula $\chi(\alpha)=(\mathtt{A},\mathit{fs},(\mathtt{n}\cdot\bar{v})\cdot\overline{\mu},\alpha,\epsilon)$
\end_inset


\end_layout

\begin_layout Enumerate
\begin_inset Formula $\mathcal{M}(\mathtt{A,n})=(\_,\mathtt{\overline{x:T}},\mathtt{e},\_)$
\end_inset


\end_layout

\begin_layout Enumerate
\begin_inset Formula $\varphi=(\mathtt{n},[\mathtt{this}\mapsto\alpha,\mathtt{\bar{x}}\mapsto\bar{v}],\cdot)$
\end_inset


\end_layout

\begin_layout Enumerate
\begin_inset Formula $\chi'=\chi[\alpha\mapsto(\mathtt{A},\mathit{fs},\overline{\mu},(\alpha\cdot\varphi),\mathtt{e})]$
\end_inset


\end_layout

\begin_layout Enumerate
\begin_inset Formula $\Delta\vdash\chi\diamond$
\end_inset


\end_layout

\end_deeper
\begin_layout Lemma
Then 
\begin_inset Formula $\exists\Delta^{\prime}$
\end_inset

 such that 
\begin_inset Formula $\Delta'\vdash\chi'\diamond$
\end_inset

.
\end_layout

\end_body
\end_document