* Sergey and Clarke (2012) Ilya Sergey and Dave Clarke. 2012.  Gradual Ownership Types. In _Programming Languages and Systems - 21st European Symposium on Programming, ESOP 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, March 24 - April 1, 2012. Proceedings_ _(Lecture Notes in Computer Science, Vol. 7211)_ , Helmut Seidl (Ed.). Springer, 579–599.  https://doi.org/10.1007/978-3-642-28869-2_29
  * Siek and Taha (2006) Jeremy G. Siek and Walid Taha. 2006.  Gradual Typing for Functional Languages. In _IN SCHEME AND FUNCTIONAL PROGRAMMING WORKSHOP_. 81–92.
  * Siek et al. (2015) Jeremy G. Siek, Michael M. Vitousek, Matteo Cimini, and John Tang Boyland. 2015.  Refined Criteria for Gradual Typing. In _1st Summit on Advances in Programming Languages, SNAPL 2015, May 3-6, 2015, Asilomar, California, USA_ _(LIPIcs, Vol. 32)_ , Thomas Ball, Rastislav Bodík, Shriram Krishnamurthi, Benjamin S. Lerner, and Greg Morrisett (Eds.). Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 274–293.  https://doi.org/10.4230/LIPIcs.SNAPL.2015.274
  * Van Cutsem and Miller (2013) Tom Van Cutsem and Mark S. Miller. 2013.  Trustworthy Proxies: Virtualizing Objects with Invariants. In _Proceedings of the 27th European Conference on Object-Oriented Programming_ (Montpellier, France) _(ECOOP’13)_. Springer-Verlag, Berlin, Heidelberg, 154–178.  https://doi.org/10.1007/978-3-642-39038-8_7
  * Westbrook et al. (2012) Edwin M. Westbrook, Jisheng Zhao, Zoran Budimlic, and Vivek Sarkar. 2012.  Practical Permissions for Race-Free Parallelism. In _ECOOP 2012 - Object-Oriented Programming - 26th European Conference, Beijing, China, June 11-16, 2012. Proceedings_ _(Lecture Notes in Computer Science, Vol. 7313)_ , James Noble (Ed.). Springer, 614–639.  https://doi.org/10.1007/978-3-642-31057-7_27
  * Wimmer and Würthinger (2012) Christian Wimmer and Thomas Würthinger. 2012.  Truffle: a self-optimizing runtime system. In _Conference on Systems, Programming, and Applications: Software for Humanity, SPLASH ’12, Tucson, AZ, USA, October 21-25, 2012_ , Gary T. Leavens (Ed.). ACM, 13–14.  https://doi.org/10.1145/2384716.2384723
  * Wright and Felleisen (1994) Andrew K. Wright and Matthias Felleisen. 1994.  A Syntactic Approach to Type Soundness.  _Inf. Comput._ 115, 1 (1994), 38–94.  https://doi.org/10.1006/inco.1994.1093
  * Wrigstad et al. (2009) Tobias Wrigstad, Filip Pizlo, Fadi Meawad, Lei Zhao, and Jan Vitek. 2009.  Loci: Simple Thread-Locality for Java. In _ECOOP 2009 - Object-Oriented Programming, 23rd European Conference, Genoa, Italy, July 6-10, 2009. Proceedings_ _(Lecture Notes in Computer Science, Vol. 5653)_ , Sophia Drossopoulou (Ed.). Springer, 445–469.  https://doi.org/10.1007/978-3-642-03013-0_21
  * Wyatt (2013) Derek Wyatt. 2013\.  _Akka concurrency_.  Artima Incorporation.
  * Zhao and Boyland (2008) Yang Zhao and John Boyland. 2008.  A Fundamental Permission Interpretation for Ownership Types. In _TASE_. 65–72.

##  Appendix A Expression Rules Producing Errors

Fig. 12 shows all the expression rules producing errors.

${\begin{array}[]{c}\textsc{({{E-NoSuchField}})}\\\ {}\hfil\\\ H(x.f)=\bot\\\
\hline\cr\raisebox{-1.0pt}{$H;E[x.f]\rightsquigarrow
H;\textmd{Err}_{N}$}\end{array}\qquad\begin{array}[]{c}\textsc{({{E-NoSuchMethod}})}\\\
H(x)=\iota\quad
H(\iota)=\\_\,\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{obj}}}}}}\,\\{\\_\,\overline{M}\\}\\\
m\not\in\textit{names}(\overline{M})\\\
\hline\cr\raisebox{-1.0pt}{$H;E[x.m(v)]\rightsquigarrow
H;\textmd{Err}_{N}$}\end{array}\qquad\begin{array}[]{c}\textsc{({{E-NoSuchFieldAssign}})}\\\
{}\hfil\\\ H(x.f)=\bot\\\
\hline\cr\raisebox{-1.0pt}{$H;E[x.f=v]\rightsquigarrow
H;\textmd{Err}_{N}$}\end{array}$

${{{{\begin{array}[]{c}\textsc{({{E-SendBadTargetOrArgument}})}\\\
H(\iota)=\\_\,\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{obj}}}}}}\,\\{\\_\,\\_\\}\lor
H(\iota^{\prime})=\,\\!\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{chan}}}}}}\,\\{\\_\\}\\\
\hline\cr\raisebox{-1.0pt}{$H;E[\iota\leftarrow\iota^{\prime}],T\rightsquigarrow
H;\textmd{Err}_{N}$}\end{array}\quad\begin{array}[]{c}\textsc{({{E-RecvBadTarget}})}\\\
H(\iota)=\\_\,\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{obj}}}}}}\,\\{\\_\,\\_\\}\\\
\hline\cr\raisebox{-1.0pt}{$H;E[\ \leftarrow\iota]\rightsquigarrow
H;\textmd{Err}_{N}$}\end{array}\quad\begin{array}[]{c}\textsc{({{E-CastError}})}\\\
H(\iota)=K^{\prime}\,\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{obj}}}}}}\,\\{\\_\,\\_\\}\quad
K^{\prime}\neq K\\\
\hline\cr\raisebox{-1.0pt}{$H;E[(K)~{}\iota]\rightsquigarrow
H;\textmd{Err}_{C}$}\end{array}$

${\begin{array}[]{c}\textsc{({{E-AbsentVar}})}\\\ H(x)=\top\\\
\hline\cr\raisebox{-1.0pt}{$H;E[x]\rightsquigarrow
H;\textmd{Err}_{A}$}\end{array}\quad\begin{array}[]{c}\textsc{({{E-Consume}})}\\\
H(x)=\top\\\
\hline\cr\raisebox{-1.0pt}{$H;E[\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{consume}}}}}}\
x]\rightsquigarrow
H;\textmd{Err}_{A}$}\end{array}\quad\begin{array}[]{c}\textsc{({{E-AbsentTarget}})}\\\
H(x)=\top\\\ \hline\cr\raisebox{-1.0pt}{$H;E[x.m(v)]\rightsquigarrow
H;\textmd{Err}_{A}$}\end{array}$

${\begin{array}[]{c}\textsc{({{E-AbsentTargetAccess}})}\\\ H(x)=\top\\\
\hline\cr\raisebox{-1.0pt}{$H;E[x.f]\rightsquigarrow
H;\textmd{Err}_{A}$}\end{array}\qquad\begin{array}[]{c}\textsc{({{E-AbsentFieldAssign}})}\\\
H(x)=\top\\\ \hline\cr\raisebox{-1.0pt}{$H;E[x.f=v]\rightsquigarrow
H;\textmd{Err}_{A}$}\end{array}\qquad\begin{array}[]{c}\textsc{({{E-AbsentCopyTarget}})}\\\
H(x)=\top\\\ \hline\cr\raisebox{-1.0pt}{$H;E[K\
\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{copy}}}}}}\
x]\rightsquigarrow H;\textmd{Err}_{A}$}\end{array}$

${\begin{array}[]{c}\textsc{({{E-AliasIso}})}\\\ H(x)=\iota\\\
\textsf{isIso}(H,\iota)\\\ \hline\cr\raisebox{-1.0pt}{$H;E[x]\rightsquigarrow
H;\textmd{Err}_{P}$}\end{array}\qquad\begin{array}[]{c}\textsc{({{E-IsoField}})}\\\
H(x)=\iota^{\prime}\quad H(x.f)=\iota\\\
\textsf{localOwner}(H,i,\iota^{\prime})\quad\textsf{isIso}(H,\iota)\\\
\hline\cr\raisebox{-1.0pt}{$H;E[x.f]^{i}\rightsquigarrow
H;\textmd{Err}_{P}$}\end{array}\qquad\begin{array}[]{c}\textsc{({{E-BadInstantiation}})}\\\
\exists v\in\overline{v}.\\\
\neg\textsf{OkRef}(H,K,v)\lor\textsf{notLocalOwner}(H,i,v)\\\
\hline\cr\raisebox{-1.0pt}{$H;E[K\,\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{obj}}}}}}\,\\{\overline{f=v}\,\overline{M}\\}]^{i}\rightsquigarrow
H;\textmd{Err}_{P}$}\end{array}$

${\begin{array}[]{c}\textsc{({{E-BadFieldAssign}})}\\\ H(x)=\iota\quad
H(\iota)=K\,\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{obj}}}}}}\,\\{\\_\
f=v^{\prime}\,\overline{M}\\}\\\
\textsf{isImm}(H,\iota)\lor\neg\textsf{OkRef}(H,K,v)\lor\textsf{notLocalOwner}(H,i,\iota)\lor(\textsf{isLocal}(H,\iota)\land\textsf{isOwner}(H,i,\iota)\land\textsf{notLocalOwner}(H,i,v))\\\
\hline\cr\raisebox{-1.0pt}{$H;E[x.f=v]^{i}\rightsquigarrow
H;\textmd{Err}_{P}$}\end{array}$

${\begin{array}[]{c}\textsc{({{E-CopyTarget}})}\\\
H(x)\neq\top\quad\textsf{notLocalOwner}(H,i,H(x))\\\
\hline\cr\raisebox{-1.0pt}{$H;E[K\
\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{copy}}}}}}\
x]^{i}\rightsquigarrow
H;\textmd{Err}_{P}$}\end{array}\quad\begin{array}[]{c}\textsc{({{E-LocalField}})}\\\
H(x)=\iota\quad H(x.f)=v\qquad\textsf{notLocalOwner}(H,i,\iota)\\\
\hline\cr\raisebox{-1.0pt}{$H;E[x.f]^{i}\rightsquigarrow
H;\textmd{Err}_{P}$}\end{array}$

Figure 12. Expression rules producing errors. To reduce clutter, we write
$H(x.f)=v$ when ${H(x)=\iota\land
H(\iota)=\\_\,\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{obj}}}}}}\,\\{F\,\\_\\}$
and $f=v\in F$, and $H(x.f)=\bot$ when ${H(x)=\iota\land
H(\iota)=\\_\,\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{obj}}}}}}\,\\{F\,\\_\\}$
and $f\not\in\textit{dom}(F)$, and
$\textsf{notLocalOwner}(H,i,v)=\textsf{isLocal}(H,v)\land\neg\textsf{isOwner}(H,i,v)$.

##  Appendix B Definition, Lemmas, and Proofs

###### Definition B.1 (Initial Configuration).

An initial configuration is a closed term with empty heap, $\epsilon;t$.

###### Definition B.2 (Terminal Configuration).

A well-formed configuration $\Gamma\vdash H;\overline{T}$ is terminal if it
contains zero threads ($\overline{T}=\epsilon$), it is an error
($\overline{T}=\textit{Err}$), or if it is a deadlock configuration
($\textsf{Deadlock}(\Gamma\vdash H;\overline{T})$).

###### Definition B.3 (Deadlock Configuration).

A deadlocked configuration is a well-formed configuration where all threads
are blocked on sends and receives.

$\displaystyle\textsf{Deadlock}(\Gamma\vdash H;\overline{T})\iff$
${{{\displaystyle\overline{T}\neq\epsilon\land\forall
T^{\prime}\in\overline{T}.\lor\left\\{\begin{array}[]{l}T^{\prime}=E[\
\leftarrow\iota]\land
H(\iota)=\,\\!\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{chan}}}}}}\,\\{\\_,\varnothing\\}\\\
T^{\prime}=E[x\leftarrow\\_]\land
H(\iota)=\,\\!\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{chan}}}}}}\,\\{\\_,v\\}\\\
T^{\prime}=E[\blacksquare_{\\_}i\,\iota]\land
H(\iota)=\,\\!\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{chan}}}}}}\,\\{i,\\_\\}\end{array}\right.$

###### Definition B.4 (Data Race).

To formally define a data race, we introduce the notion of a trace $R$, which
is an ordered sequence of reductions $r_{\\_}1$, $r_{\\_}2$… in the evaluation
of a program $P$. We only concern ourselves with traces that do not evaluate
to a permission or cast error.

We define the precedes relation $<$ on reductions thus: If
$R=r_{\\_}1,R^{\prime}$, then $r_{\\_}1<r_{\\_}2$ for all $r_{\\_}2\in
R^{\prime}$. Recall that threads have unique ids.

We are now ready to formally define a data race in Dalarna. A program has a
data race if it may give rise to at least one (non-erring) trace with a data
race. A trace $R$ has a data race if it contains steps $r_{\\_}1<r_{\\_}2$
such that

  1. a)

$r_{\\_}1=H_{\\_}1;E[x.f=\\_]^{i}$, and $H_{\\_}1(x)=l$ (thread $i$ writes
$l.f$)

  2. b)

$r_{\\_}2=H_{\\_}2;E[y.f=\\_]^{j}$ or $r_{\\_}2=H_{\\_}2;E[y.f]^{j}$, and
$H_{\\_}2(y)=l$ (thread $j$ reads or writes $l.f$)

  3. c)

$i\neq j$ (the conflicting accesses take place in different threads

and there does not exist $r_{\\_}3,r_{\\_}4\in R$ such that

  1. i

$r_{\\_}1<r_{\\_}3<r_{\\_}4<r_{\\_}2$,

  2. ii

$r_{\\_}3=H_{\\_}3;E[\\_\leftarrow v_{\\_}1]^{i}$ and $l\in ROG(H,v_{\\_}1)$
(thread $i$ sends $l$ somewhere)

  3. iii

$r_{\\_}4=H_{\\_}4;[\leftarrow v_{\\_}2]^{j}$ and $l\in ROG(H,v_{\\_}2)$
(thread $j$ receives $l$ from somewhere)

where $ROG(H,v)$ denotes the transitive closure of objects (the Reachable
Object Graph) in $H$ rooted in $v$.

###### Definition B.5 (Trace).

Define a trace $\mathcal{T}$ as a list of pairs containing the reduction rules
and thread ids.

###### Definition B.6 (Trace Of A Program).

Define the trace $\mathcal{T}$ of a program $P$ as the accumulation of pairs
of reduction rules and thread ids on which the reduction rules take place,
e.g., $\epsilon;P\rightsquigarrow^{*}H^{\prime};\overline{T^{\prime}}$
produces trace $\mathcal{T}$.

###### Definition B.7 (Trace Reduction Replay).

Define a trace replay reduction relation
$(\mathcal{T:T^{\prime}});H;\overline{T}\rightsquigarrow{}\mathcal{T^{\prime}};H^{\prime};\overline{T^{\prime}}$
as the reduction relation that executes the first item of the trace
$\mathcal{T:T^{\prime}}$ at a time, returning the trace list without the first
item ($\mathcal{T}$), a new heap ($H^{\prime}$), and a new thread
configuration ($\overline{T^{\prime}}$).

Definition B.8 states that if an object is reachable from threads $t$ and
$t^{\prime}$ then either $t=t^{\prime}$ or the object is not local or the
object can only be dereference in a single thread (via ownership check). Thus,
thread-local objects are not reachable by multiple threads. The helper
function $\textsf{ROG}(H,t)$ returns the set of objects in $H$ reachable from
$t$ by traversing variables and fields (a reflexive transitive closure of
objects).

###### Definition B.8 (Thread-Local Objects).

A configuration satisfies object “thread-locality” if no object with a local
capability is reachable from more than one thread.

$\displaystyle\textsf{Local}(H,\overline{T})\iff\forall t^{i},t^{\prime
j}\in\overline{T}.$
$\displaystyle\qquad\qquad\iota\in(\textsf{ROG}(H,t^{i})\cap\textsf{ROG}(H,t^{\prime
j}))\Rightarrow$ ${{\displaystyle\qquad\qquad(t=t^{\prime}\land
i=j)\lor(H(\iota)=K\,\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{obj}}}}}}\,\\{\\_\,\\_\\}\land
K\neq\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{local}}}}}}{})\lor$
$\displaystyle\qquad\qquad(t\neq t^{\prime}\land i\neq
j\land(\textsf{isLocal}(H,\iota)$
$\displaystyle\qquad\qquad\Rightarrow\textsf{isOwner}(H,i,\iota)\land\neg\textsf{isOwner}(H,j,\iota))$

Object isolation (Definition B.9) states that all isolated objects have a
single reference to them, from the heap or stack, modulo borrowing. Borrowing
allows calling methods on isolated objects without consuming the target,
leading to (temporal) aliases which are all on the stack of the same thread.
We forbid consuming self, thus aliases of isolated objects (and self) are only
introduced through method calls. After a method call, the alias is buried and
non-accessible.

###### Definition B.9 (Object Isolation).

A configuration satisfies object isolation if no objects with an iso
capability have more than one incoming pointer from the stack and heap, modulo
borrowing.

$\displaystyle\textsf{Isolated}(H,\overline{T})\iff$
$\displaystyle\quad\forall\iota\in\textsf{Isos}(H)\,.\,|\textsf{Inc}(H,\overline{T},\iota)\cup\textsf{Inc}(H,\iota)|>1\Rightarrow$
$\displaystyle\quad\quad\exists
t\in\overline{T}\,.\,\textsf{Inc}(H,\overline{T},\iota)=\textsf{Inc}(H,t,\iota)\land\textsf{Inc}(H,\iota)=\emptyset$

where Inc collects the set of variables and fields aliasing a particular
location: ${\textsf{Inc}(H,v)=\\{\iota.f\,|\,\iota\in\textit{dom}(H)\land
H(\iota.f)=v\\}\cup\\{\iota\,|\,\iota\in\textit{dom}(H)\land
H(\iota)=\,\\!\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{chan}}}}}}\,\\{i,v\\}\\}$,
$\textsf{Inc}(H,\overline{T},v)=\bigcup_{\\_}{t\in\overline{T}}\textsf{Inc}(H,t,v)$,
$\textsf{Inc}(H,t,v)=\\{x\,|\,x\in\textsf{FreeVars}(t)\land
H(x)=v\\}\cup\\{v\mid v\in t\\}$, and $\textsf{FreeVars}(t)$ is the set of all
free variables in $t$.

###### Definition B.10 (Object’s Owner).

Define the predicate $\textsf{isOwner}(H,i,v)$ for a heap ($H$), owner ($i$),
and value ($v$) as:

${\displaystyle\textsf{isOwner}(H,i,v)\iff
H(\iota)=K^{i}\,\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{obj}}}}}}\,\\{\\_\,\\_\\},$
$\displaystyle\qquad\textit{where}\ v=\iota\land\iota\in\textit{dom}(H)$

###### Definition B.11 (Safe Erasure).

Define the function safe erasure, e, as the function that replaces safe
capabilities to unsafe capability as follows:

${\displaystyle(\Gamma,x:K)^{e}=(\Gamma)^{e},x:\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{unsafe}}}}}}$
${\displaystyle(\Gamma,\iota:K)^{e}=(\Gamma)^{e},\iota:\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{unsafe}}}}}}$
$\displaystyle(H,x\mapsto\iota)^{e}=(H)^{e},x\mapsto\iota$
${{\displaystyle(H,\iota\mapsto\,\\!\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{chan}}}}}}\,\\{i,v\\})^{e}=(H)^{e},\iota\mapsto\,\\!\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{chan}}}}}}\,\\{i,v\\}$
${{{\displaystyle(H,\iota\mapsto
K\,\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{obj}}}}}}\,\\{\\_\,\\_\\})^{e}=(H)^{e},\iota\mapsto\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{unsafe}}}}}}\,\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{obj}}}}}}\,\\{\\_\,\\_\\}$
$\displaystyle(t\ \overline{T})^{e}=(t)^{e}\ (\overline{T})^{e}$
${{{{{{{{{{{{{{{\displaystyle(t)^{e}=\begin{cases}\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{unsafe}}}}}}{}\,\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{obj}}}}}}\,\\{\overline{f=(v)^{e}}\,\overline{(M)^{e}}\\},&t=K\,\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{obj}}}}}}\,\\{\overline{f=v}\,\overline{M}\\}\\\
(\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{unsafe}}}}}})~{}\iota,&t=(K)~{}\iota\\\
\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{unsafe}}}}}}\
\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{copy}}}}}}\
x,&t=K\
\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{copy}}}}}}\
x\\\
\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{let}}}}}}~{}x~{}=~{}(e)^{e}~{}\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{in}}}}}}~{}(t)^{e},&t=\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{let}}}}}}~{}x~{}=~{}e~{}\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{in}}}}}}~{}t\\\
\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{spawn}}}}}}~{}(x)~{}\\{(t)^{e}\\},&t=\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{spawn}}}}}}~{}(x)~{}\\{t\\}\\\
\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{method}}}}}}~{}m(x)~{}\\{(t)^{e}\\},&t=\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{method}}}}}}~{}m(x)~{}\\{t\\}\\\
t,&\textit{otherwise}\end{cases}$

###### Definition B.12 (Capability Extraction).

${{{Cap(H,x)=\begin{cases}K,&H(x)=\iota\land
H(\iota)=K\,\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{obj}}}}}}\,\\{\\_\,\\_\\}\\\
\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{local}}}}}}{},&H(x)=\iota\land
H(\iota)=\,\\!\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{chan}}}}}}\,\\{\\_,\\_\\}\\\
K,&H(x)=\top,\textit{ for some }K\end{cases}$

###### Definition B.13 (Thread’s Variables).

The variables of a thread are all variables used in the thread.

${{\displaystyle\textsf{Vars}(\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{let}}}}}}~{}x~{}=~{}e~{}\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{in}}}}}}~{}t)=\\{x\\}\cup\textsf{Vars}(e)\cup\textsf{Vars}(t)$
${{\displaystyle\textsf{Vars}(x)=\textsf{Vars}(\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{consume}}}}}}\
x)=\textsf{Vars}(x.f)=\textsf{Vars}(K\
\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{copy}}}}}}\
x)=\\{x\\}$
$\displaystyle\textsf{Vars}(x.f=e)=\textsf{Vars}(x.m(e))=\\{x\\}\cup\textsf{Vars}(e)$
$\displaystyle\textsf{Vars}(e\leftarrow
e^{\prime})=\textsf{Vars}(e)\cup\textsf{Vars}(e^{\prime})$
$\displaystyle\textsf{Vars}((K)~{}e)=\textsf{Vars}(\ \leftarrow
e)=\textsf{Vars}(e)$
${\displaystyle\textsf{Vars}(K\,\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{obj}}}}}}\,\\{\overline{f=w}\,\\_\\})=\textsf{Vars}(\overline{w})$
${\displaystyle\textsf{Vars}(\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{spawn}}}}}}~{}(x)~{}\\{t\\})=\textsf{Vars}(\\_)=\epsilon$

###### Definition B.14 (Reachable Object Graph).

Define the helper function $\textsf{ROG}(H,t)$ and $\textsf{ROG}(H,\iota)$ as
the function that returns the transitive closure of objects reachable from
term $t$ and location $\iota$.

$\displaystyle\textsf{ROG}(H,t)$
$\displaystyle=\bigcup_{\\_}{x\in\textsf{DefVar}(H,t)}\textsf{ROG}(H,H(x))\cup\\{\textsf{ROG}(H,\iota)\mid\iota\in
t\\}$ $\displaystyle\textsf{ROG}(H,v^{\prime})$
${\displaystyle=\begin{cases}\bigcup_{\\_}{f=v\in\overline{F}}\,\textsf{ROG}(H,v)\cup\\{\iota\\},&v^{\prime}=\iota\land
H(\iota)=K\,\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{obj}}}}}}\,\\{\overline{F}\,\overline{M}\\}\\\
\emptyset,&\textit{otherwise}\end{cases}$ $\displaystyle\textsf{DefVar}(H,t)$
$\displaystyle=\\{x\mid x\in t\land x\in\textit{dom}(H)\\}$

###### Lemma B.15 (Well-formed Values Are Not Absent (Or Null)).

$\Gamma\vdash H;E[v]\Rightarrow v\neq\varnothing\land v\neq\top$

###### Proof.

By induction on the well-formedness of the configuration. ∎

###### Lemma B.16 (Fresh Variables).

${{\displaystyle\Gamma\vdash
H;\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{let}}}}}}~{}x~{}=~{}e~{}\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{in}}}}}}~{}t\Rightarrow
x\notin\textit{dom}(\Gamma)\land x\notin\textit{dom}(H)$
${\displaystyle\Gamma\vdash
H;\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{spawn}}}}}}~{}(x)~{}\\{t\\}\Rightarrow
x\notin\textit{dom}(\Gamma)\land x\notin\textit{dom}(H)$

Explanation. When a term or expression introduces a new variable, the variable
is new to $\Gamma$ and $H$.

###### Proof.

Immediate by definition of well-formed configuration. ∎

###### Lemma B.17 (Store Contains Top-Level Variables).

${{\displaystyle\Gamma\vdash
H;\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{let}}}}}}~{}x~{}=~{}e~{}\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{in}}}}}}~{}t\Rightarrow\textsf{FreeVars}(e)\cup\textsf{FreeLoc}(e)\subseteq\textit{dom}(H)$

Explanation. Given a thread
${{T=\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{let}}}}}}~{}x~{}=~{}e~{}\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{in}}}}}}~{}t$,
the free variables and locations of the expression $e$ are in the domain of
the store.

###### Proof.

Immediate from definition of well-formed configuration. ∎

###### Lemma B.18 (Weakened Well-formed Environment).

$\Gamma\vdash H\land x\notin\textit{dom}(\Gamma)\Rightarrow\Gamma,x:K\vdash H$

Explanation. If the store is a well-formed w.r.t. an environment, then
extending the environment cannot contradict this fact.

###### Proof.

Straightforward induction on the well-formedness rules. ∎

###### Lemma B.19 (Typing Permutation).

$\Gamma\vdash t\land\Delta\textit{ is a permutation of
}\Gamma\Rightarrow\Delta\vdash t$

###### Proof.

By induction on the typing derivation $\Gamma\vdash t$. ∎

###### Lemma B.20 (Weakening Typing Environment).

(1) $\displaystyle\Gamma\vdash t\land x\notin\textit{dom}(\Gamma)\land
x\notin\textsf{Vars}(t)\Rightarrow\Gamma,x:K\vdash t$ (2)
$\displaystyle\Gamma\vdash
t\land\iota\notin\textit{dom}(\Gamma)\Rightarrow\Gamma,\iota:K\vdash t$ (3)
$\displaystyle\Gamma\vdash e\land x\notin\Gamma\Rightarrow\Gamma,x:K\vdash e$

###### Proof.

By induction over the term well-formedness. There are multiple cases to
handle. We show the case when
${{t=\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{let}}}}}}~{}y~{}=~{}e~{}\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{in}}}}}}~{}t^{\prime}$
which is the more interesting one. Case
${{t=\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{let}}}}}}~{}y~{}=~{}e~{}\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{in}}}}}}~{}t^{\prime}$.
By the initial assumptions:

(4)
${{\displaystyle\Gamma\vdash\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{let}}}}}}~{}y~{}=~{}e~{}\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{in}}}}}}~{}t^{\prime}$
(5) $\displaystyle x\notin\textit{dom}(\Gamma)$ (6) $\displaystyle
x\notin\textsf{Vars}(t)$

Need to show

${{\Gamma,x:K\vdash\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{let}}}}}}~{}y~{}=~{}e~{}\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{in}}}}}}~{}t^{\prime}$

We prove each of the components of rule WF-Let.

  1. (1)

By the initial assumption
${{\Gamma\vdash\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{let}}}}}}~{}y~{}=~{}e~{}\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{in}}}}}}~{}t^{\prime}$
(4) and WF-Let, $y\notin\textit{dom}(\Gamma)$.

  2. (2)

By 1 and 6, we can conclude that $y\notin\textit{dom}(\Gamma,x:K)$.

  3. (3)

For any $e$, we must prove that $\Gamma,x:K\vdash e$ is well-formed. We apply
the induction hypothesis (Eq. 3), and conclude that $\Gamma,x:K\vdash e$ is
well-formed

  4. (4)

We need to show that $\Gamma,x:K,y:K^{\prime}\vdash t^{\prime}$. By the
initial hypothesis
${{\Gamma\vdash\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{let}}}}}}~{}y~{}=~{}e~{}\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{in}}}}}}~{}t^{\prime}$
(4). As part of the assumptions $\Gamma,y:K^{\prime}\vdash t^{\prime}$ holds.
By the induction hypothesis Eq. 1, we conclude that
$\Gamma,x:K,y:K^{\prime}\vdash t^{\prime}$.

  5. (5)

From 3 and 4 and by typing rule WF-Let, we can conclude
${{\Gamma,x:K\vdash\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{let}}}}}}~{}y~{}=~{}e~{}\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{in}}}}}}~{}t^{\prime}$.

The proof of Eqs. 2 and 3 follow the same proof strategy. ∎

###### Lemma B.21 (Weakening).

$\displaystyle\Gamma\vdash
H;t\land\Gamma^{\prime}=\Gamma,\Gamma^{\prime\prime}\land(\textit{dom}(\Gamma^{\prime\prime})\cap\textit{dom}(\Gamma)\cap\textsf{Vars}(t)=\epsilon)\land
H^{\prime}\supseteq H$ $\displaystyle\qquad\land\Gamma^{\prime}\vdash
H^{\prime}\Rightarrow\Gamma^{\prime}\vdash H^{\prime};t$

###### Proof.

By induction on the shape of $t$. The most interesting case is
${{t=\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{let}}}}}}~{}x~{}=~{}e~{}\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{in}}}}}}~{}t^{\prime}$
and the others follow the same proof technique. We need to prove:

${{\displaystyle\Gamma\vdash
H;\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{let}}}}}}~{}x~{}=~{}e~{}\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{in}}}}}}~{}t^{\prime}\land\Gamma^{\prime}=\Gamma\cup\Gamma^{\prime}\land\Gamma^{\prime}\supseteq\Gamma\land
H^{\prime}\supseteq H$
${{\displaystyle\qquad\land\Gamma^{\prime\prime}\cap\Gamma\cap\textsf{Vars}(\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{let}}}}}}~{}x~{}=~{}e~{}\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{in}}}}}}~{}t^{\prime})=\epsilon\land\Gamma^{\prime}\vdash
H^{\prime}$ ${{\displaystyle\qquad\Rightarrow\Gamma^{\prime}\vdash
H^{\prime};\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{let}}}}}}~{}x~{}=~{}e~{}\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{in}}}}}}~{}t^{\prime}$

We prove that if all components are well-formed, then by rule WF-Term
${{\Gamma^{\prime}\vdash
H^{\prime};\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{let}}}}}}~{}x~{}=~{}e~{}\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{in}}}}}}~{}t^{\prime}$.

  1. (1)

From the assumptions, $\Gamma^{\prime}\vdash H^{\prime}$.

  2. (2)

We want to prove that
${{\Gamma^{\prime}\vdash\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{let}}}}}}~{}x~{}=~{}e~{}\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{in}}}}}}~{}t^{\prime}$.
From the initial assumptions,
${{\Gamma\vdash\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{let}}}}}}~{}x~{}=~{}e~{}\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{in}}}}}}~{}t^{\prime}$
and $x\notin\textit{dom}(\Gamma)$ and $x\notin\textsf{Vars}(t)$ and
$\Gamma^{\prime}\supseteq\Gamma$. By multiple applications of Lemma B.20, we
conclude
${{\Gamma^{\prime}\vdash\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{let}}}}}}~{}x~{}=~{}e~{}\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{in}}}}}}~{}t^{\prime}$.

  3. (3)

From 1 and 2, and by application of WF-Term, conclude ${{\Gamma^{\prime}\vdash
H^{\prime};\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{let}}}}}}~{}x~{}=~{}e~{}\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{in}}}}}}~{}t^{\prime}$.

∎

###### Lemma B.22 (Weakening Maintains Thread Locality).

$\displaystyle\overline{T}\equiv t\
\overline{T^{\prime}}\land\textsf{Local}(H,\overline{T})\land\iota\in\textsf{ROG}(H,t)$
$\displaystyle\quad\land\textsf{isLocal}(H,\iota)\land
x\notin\textit{dom}(H)\Rightarrow\textsf{Local}((H,x\mapsto\iota),t\
\overline{T^{\prime}})$

Explanation. Extending the heap with new variables does not affect thread-
local objects.

###### Proof.

Trivially satisfied by induction on the definition of
$\textsf{Local}(H,\overline{T})$. ∎

###### Lemma B.23 (Binding Isolate Locations Maintain Isolatedness).

$\displaystyle\overline{T}\equiv t\
\overline{T^{\prime}}\land\textsf{Isolated}(H,\overline{T})\land\iota\in
t\land\textsf{isIso}(H,\iota)\Rightarrow\textsf{Isolated}((H,x\mapsto\iota),\overline{t\
T^{\prime}})$

Explanation. Extending the heap with a stack variable over an isolated
location maintains isolation.

###### Proof.

Trivially satisfied by induction on the definition of
$\textsf{Isolated}(H,\overline{T})$. ∎

###### Lemma B.24 (Thread-Local Term Substitution Maintains Locatity).

$\displaystyle t^{\prime}\subseteq t$ $\displaystyle\land\textsf{Local}(H,t\
\overline{T})\land\iota\in\textsf{ROG}(H,t)\land\textsf{isLocal}(H,\iota)$
$\displaystyle\land
x\notin\textit{dom}(H)\land\textsf{FreeVar}(t^{\prime})\subseteq\textsf{FreeVar}(t)\cup\\{x\\}$
$\displaystyle\Rightarrow\textsf{Local}((H,x\mapsto\iota),t^{\prime}\
\overline{T})$

Explanation. If an object $\iota$ is thread-local to term $t$, there is a
subterm $t^{\prime}$ of $t$, and we extend the heap to map a stack variable to
$\iota$, then replacement of $t$ by $t^{\prime}$ maintains thread-locality
under the modified heap.

###### Proof.

By induction on the shape of $t^{\prime}$. $t^{\prime}$ can only use free
variables available in $t$ and the other threads cannot point to the
introduced variable $x$ as $x\notin\textit{dom}(H)$. Hence, thread-locality is
maintained for object in $\iota$. ∎

###### Lemma B.25 (Deterministic Evaluation).

If $H;T\ \overline{T}\rightsquigarrow H^{\prime};\overline{T^{\prime}}\
\overline{T}$ and $H;T\ \overline{T}\rightsquigarrow
H^{\prime\prime};\overline{T^{\prime\prime}}\ \overline{T}$, then
$\overline{T^{\prime}}\equiv\overline{T^{\prime\prime}}$

###### Proof.

By induction on a derivation of $H;T\ \overline{T}\rightsquigarrow
H^{\prime};\overline{T^{\prime}}\ \overline{T}$. ∎

###### Lemma B.26 (Capability Stripping Preserves Terms and Expressions).

${(t^{i})^{e}=t^{i}[K/\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{unsafe}}}}}}]$
Explanation: A capability stripped term is equivalent to a replacement of its
capabilities $K$ by unsafe, i.e., preserves the terms and expressions.

###### Proof.

By induction on the term structure. ∎

See 5.3

###### Proof.

By induction on the thread structure. Assume we are deadling with thread local
objects. The only way to create a thread local object with a reference to a
thread local object with different owner is by rule R-FieldUpdate. But this
rule does not satisfy the premises when the owner of the target and source
objects have different owners. Instead, rule E-BadFieldAssign applies and
throws a permission error. ∎

###### Lemma B.27 (Unsafe Programs Do Not Raise Permission Errors).

If $\Gamma^{e}\vdash(H;\overline{T})^{e}$ and
$(H;\overline{T})^{e}\rightsquigarrow H^{\prime};\overline{T^{\prime}}$, then
$\textmd{Err}_{C}\not\equiv\overline{T^{\prime}}\not\equiv\textmd{Err}_{P}{}$.

###### Proof.

By induction on a derivation of the reduction derivation and the thread
configuration. Trivially, configurations that do not throw runtime errors
satisfy the inductive hypothesis; configurations where
$T^{\prime}\equiv\textmd{Err}_{N}$ or $T^{\prime}\equiv\textmd{Err}_{C}$
trivially satisfy the hypothesis; from the reduction rules that throw
permission errors: E-AliasIso, E-IsoField, E-BadFieldAssign, E-CopyTarget,
E-BadInstantiation and E-LocalField require safe capabilities to throw a
permission error but by the initial assumptions, we have stripped the safe
capabilities. Thus, these errors cannot happen. Reduction rule
E-BadInstantiation cannot happen because all capabilities are unsafe and
$\textsf{OkRef}(...)$ is trivially satisfied. ∎

See 5.1

###### Proof.

Assumptions $\Gamma\vdash H;\overline{T}$.

We start by induction on the shape of $\overline{T}$.

  1. (1)

$\overline{T}\equiv\textit{Err}$. Progress holds trivially.

  2. (2)

$\overline{T}\equiv\epsilon$. Progress holds trivially.

  3. (3)

$\overline{T}\equiv T\ \overline{T^{\prime}}$. Induction hypothesis:

IH1:

$T=\textit{Err}\lor\textsf{Deadlock}(\Gamma\vdash H;T)\lor T=\epsilon\lor
H;T\rightsquigarrow H^{\prime};\overline{T^{\prime\prime}}$

IH2:

$\overline{T^{\prime}}=\textit{Err}\lor\textsf{Deadlock}(\Gamma\vdash
H;\overline{T^{\prime}})\lor\overline{T^{\prime}}=\epsilon\lor
H;\overline{T^{\prime}}\rightsquigarrow
H^{\prime};\overline{T^{\prime\prime}}$

IH3:

$\textsf{Deadlock}(\Gamma\vdash H;T\ \overline{T^{\prime}})$

We continue by case analysis over IH1.

    1. (a)

$T\equiv\textit{Err}\ \overline{T^{\prime}}$. By the equivalence rules,
$T\equiv\textit{Err}$ and is a terminal configuration.

    2. (b)

$T\equiv\epsilon$, then we continue by IH2.

    3. (c)

$H;T\rightsquigarrow H^{\prime};\overline{T^{\prime\prime}}$ by C-Eval.

    4. (d)

$\textsf{Deadlock}(\Gamma\vdash H;T)$. We continue by case analysis over IH2:

      1. (i)

$\overline{T^{\prime}}\equiv\textit{Err}$. By the equivalence rules, $T\
\textit{Err}\equiv\textit{Err}$ and is a terminal configuration.

      2. (ii)

$\overline{T^{\prime}}=\epsilon$. Then $\Gamma\vdash H;T$ is a terminal
configuration.

      3. (iii)

$H;\overline{T^{\prime}}\rightsquigarrow
H^{\prime};\overline{T^{\prime\prime}}$, the configuration steps to $H;T\
\overline{T^{\prime}}\rightsquigarrow H^{\prime};T\
\overline{T^{\prime\prime}}$ by rule C-Eval.

      4. (iv)

$\textsf{Deadlock}(\Gamma\vdash H;\overline{T^{\prime}})$, then we proceed by
IH3, $\textsf{Deadlock}(\Gamma\vdash H;T\ \overline{T^{\prime}})$, and
progress holds trivially.

  4. (4)

$\overline{T}\equiv t$. By the induction hypothesis either $\Gamma\vdash H;t$
is a terminal configuration or it can make progress.

A1:

$\textsf{Deadlock}(\Gamma\vdash H;t)\lor H;t\rightsquigarrow
H^{\prime};\overline{T^{\prime}}$

We continue by case analysis over A1.

     * •

$\textsf{Deadlock}(\Gamma\vdash H;t)$. Progress holds trivially.

     * •

$H;t\rightsquigarrow H^{\prime};\overline{T^{\prime}}$.

From the initial assumption and WF-Configuration:

(7) $\displaystyle\Gamma\vdash H$ (8) $\displaystyle\Gamma\vdash H;t$ (9)
$\displaystyle\forall t^{\prime}\in\overline{T}.\ \Gamma\vdash H;t^{\prime}$

We proceed by induction over the shape of $t$, and assume that all
subexpressions were reduced using the evaluation context $E$ rules. We prove
all the inductive cases where the evaluation context reduces an expression to
a value.

       1. (a)

$t=\varnothing$. This cannot happen, follows from Lemma B.15 with Eq. 8.

       2. (b)

${{t\equiv\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{let}}}}}}~{}x~{}=~{}v~{}\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{in}}}}}}~{}t^{\prime}$.

         1. (i)

$x\notin\textit{dom}(H)$ from Lemma B.16

         2. (ii)

By R-Let with (4(b)i) the configuration steps to $H,x\mapsto v;t^{\prime}$.

       3. (c)

$t\equiv v$. By the equivalence rules (LABEL:fig:_configconcurrency),
$H;v\equiv H;\epsilon$ and we apply the induction hypothesis to this
configuration.

       4. (d)

$t\equiv E[x]$.

         1. (i)

$x\in\textit{dom}(H)$ by Lemma B.17.

         2. (ii)

$x\mapsto v\in H$ by assumption Eq. 7 with Item 4(d)i.

         3. (iii)

From Item 4(d)ii we proceed by case analysis on the shape of $v$:

            * –

$H(x)=\top$. By E-AbsentVar the configuration steps to $H;\textmd{Err}_{A}$.

            * –

$H(x)=\varnothing$. This cannot happen, follows from Lemma B.15 with Eq. 8..

            * –

$H(x)=\iota$. $\iota\in\textit{dom}(H)$ by assumption Eq. 7. There are two
cases to consider, whether the location is to an isolated object or not.

              * *

$\neg\textsf{isIso}(H,\iota)$. By R-Var the configuration steps to
$H;E[\iota]$.

              * *

$\textsf{isIso}(H,\iota)$. By E-AliasIso the configuration steps to
$H;\textmd{Err}_{P}$.

       5. (e)

${t\equiv
E[\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{consume}}}}}}\
x]$.

         1. (i)

$x\in\textit{dom}(H)$ by Lemma B.17.

         2. (ii)

$x\mapsto v\in H$ by assumption Eq. 7 with Item 4(e)i.

         3. (iii)

From Item 4(e)ii we proceed by case analysis on the shape of $v$:

            * –

$v=\top$. By E-Consume the configuration steps to $H;\textmd{Err}_{A}$.

            * –

$v=\varnothing$. This cannot happen, follows from Lemma B.15 with Eq. 8..

            * –

$v=\iota$. $\iota\in\textit{dom}(H)$ by assumption Eq. 7, and
${H;E[\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{consume}}}}}}\
x]\rightsquigarrow H[x\mapsto\top];E[\iota]$ by R-Consume.

       6. (f)

$t\equiv E[(K)~{}\iota]$.

         1. (i)

$\iota\in\textit{dom}(H)$ by Lemma B.17

         2. (ii)

We proceed by case analysis on the object capability of the location $\iota$,
checking whether the object capability matches the casted capability.

            * –

${H(\iota)=K\,\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{obj}}}}}}\,\\{\\_\,\\_\\}$.
By R-CastLoc the configuration steps to $H;E[\iota]$.

            * –

${H(\iota)=K^{\prime}\,\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{obj}}}}}}\,\\{\\_\,\\_\\}\land
K\neq K^{\prime}$. By E-CastError the configuration steps to
$H;\textmd{Err}_{A}$.

       7. (g)

$t\equiv E[x.f]$. There are multiple cases to handle, depending on the value
of $x$ and its field $f$.

         1. (i)

$x\in\textit{dom}(H)$ by Lemma B.17.

         2. (ii)

$x\mapsto v\in H$ by assumption Eq. 7 with Item 4(g)i.

         3. (iii)

$v=\top\lor\iota\lor\varnothing$. We proceed by case analysis over $v$:

            * –

$v=\varnothing$. This cannot happen. By assumption (7),
$x\mapsto\varnothing\in H$ is not well-formed.

            * –

$v=\top$. By E-AbsentTargetAccess the configuration steps to
$H;\textmd{Err}_{A}$.

            * –

$v=\iota$. By the assumption Eq. 7,
${\iota\mapsto\\_\,\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{obj}}}}}}\,\\{\\_\,\\_\\}\in
H$. We proceed by case analysis on the field.

              * *

${H(\iota)=\\_\,\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{obj}}}}}}\,\\{\overline{F}\,\overline{M}\\},f\notin\textit{dom}(\overline{F})$.
By E-NoSuchField the configuration steps to $H;\textmd{Err}_{N}$.

              * *

${H(\iota)=\\_\,\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{obj}}}}}}\,\\{\\_f=v\,\overline{M}\\}$,
$\neg\textsf{isIso}(H,\iota),\textsf{localOwner}(H,i,\iota)$. By R-Field the
configuration steps to $H;v$.

              * *

${H(\iota)=\\_\,\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{obj}}}}}}\,\\{\\_f=v\,\overline{M}\\}$,
$\textsf{isIso}(H,\iota),\textsf{localOwner}(H,i,\iota)$. By E-IsoField the
configuration steps to $H;\textmd{Err}_{P}$.

              * *

${H(\iota)=\\_\,\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{obj}}}}}}\,\\{\\_f=v\,\overline{M}\\}$,
$\textsf{noLocalOwner}(H,i,\iota)$. By E-LocalField the configuration steps to
$H;\textmd{Err}_{P}$..

       8. (h)

$t\equiv E[x.f=v]$ There are multiple cases to handle, depending on the value
of $x$ and its field $f$.

         1. (i)

$x\in\textit{dom}(H)$ by Lemma B.17.

         2. (ii)

$x\mapsto v^{\prime}\in H$ by assumption Eq. 7 with Item 4(h)i.

         3. (iii)

$v=\top\lor\iota\lor\varnothing$. We proceed by case analysis over
$v^{\prime}$ and $v$:

            * –

$v^{\prime}=\varnothing$. This cannot happen. By assumption (7),
$x\mapsto\varnothing\in H$ is not well-formed.

            * –

$v^{\prime}=\top$. By E-AbsentFieldAssign the configuration steps to
$H;\textmd{Err}_{A}$..

            * –

$v^{\prime}=\iota^{\prime}$. By the assumption Eq. 7,
${\iota\mapsto\\_\,\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{obj}}}}}}\,\\{\\_\,\\_\\}\in
H$. There are multiple cases to handle. We start by case analysis on the value
of $v$, and then continue by case analysis on field $f$:

              * *

$v=\varnothing$. This cannot happen, follows from Lemma B.15 with Eq. 8..

              * *

$v=\top$. This cannot happen, by Lemma B.15 with Eq. 8..

              * *

$v=\iota$. We proceed by case analysis over field $f$ below:

              * *

${H(\iota^{\prime})=\\_\,\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{obj}}}}}}\,\\{\overline{F}\,\overline{M}\\},f\notin\textit{dom}(\overline{F})$.
By E-NoSuchFieldAssign the configuration steps to $H;\textmd{Err}_{N}$..

              * *

${{H(\iota^{\prime})=K\,\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{obj}}}}}}\,\\{\\_f=v\,\overline{M}\\}\land
K=\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{imm}}}}}}{}$.
By E-BadFieldAssign the configuration steps to $H;\textmd{Err}_{P}$.

              * *

${{H(\iota)=K\,\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{obj}}}}}}\,\\{\\_f=v^{\prime\prime}\,\overline{M}\\}\land
K\neq\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{imm}}}}}}{},v^{\prime\prime}=\iota^{\prime\prime}$.
If the object location $\iota^{\prime\prime}$ has a capability $K^{\prime}$,
s.t. $K,K^{\prime}\leq$ and the source and target are owned by the current
thread, then we conclude by direct application of R-FieldAssign. If the object
location $\iota^{\prime\prime}$ has a capability $K^{\prime}$ s.t. $K\nleq
K^{\prime}$ or if the current thread does not own the target or if the current
thread is the owner of the target but not of the source, then we conclude by
direct application of E-BadFieldAssign, which reduces to $H;\textmd{Err}_{P}$.

       9. (i)

$t\equiv E[v\leftarrow v^{\prime}]$ Reminder. We are under the assumption that
$\neg\textsf{Deadlock}(\Gamma\vdash H;t\ \overline{T^{\prime}})$, so $t$ may
be blocked but there is no deadlock in the global configuration
($\overline{T^{\prime}}$). We proceed by case analysis on the shape of $v$ and
$v^{\prime}$.

         1. (i)

$v=\varnothing\lor v^{\prime}=\varnothing$. This cannot happen, follows from
Lemma B.15 with Eq. 8..

         2. (ii)

$v=\top\lor v^{\prime}=\top$. This cannot happen, follows from Lemma B.15 with
Eq. 8..

         3. (iii)

$v=\iota\land v^{\prime}=\iota^{\prime}$. There are multiple cases to handle,
depending on the shape of the objects pointed by $\iota$ and $\iota^{\prime}$.

            * –

${H(\iota)=\\_\,\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{obj}}}}}}\,\\{\\_\,\\_\\}$.
By E-SendBadTargetOrArgument the configuration steps to $H;\textmd{Err}_{N}$.

            * –

${H(\iota^{\prime})=\,\\!\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{chan}}}}}}\,\\{\\_,\\_\\}$.
By E-SendBadTargetOrArgument the configuration steps to $H;\textmd{Err}_{N}$.

            * –

${H(\iota)=\,\\!\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{chan}}}}}}\,\\{\\_,\varnothing\\}$,
by R-SendBlock the configuration steps.

       10. (j)

$t\equiv E[\ \leftarrow\iota]$. By Lemma B.17, $\iota\in\textit{dom}(H)$.
There are two cases to handle, when $\iota$ maps to an object and to a
channel.

          * –

${\iota\mapsto\\_\,\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{obj}}}}}}\,\\{\\_\,\\_\\}$.
By E-RecvBadTarget the configuration steps to $H;\textmd{Err}_{N}$.

          * –

${\iota\mapsto\,\\!\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{chan}}}}}}\,\\{\\_,v\\}$.
$v=\iota^{\prime}$ by assumption (7) and the assumption that it takes a
reduction step (the deadlock was handled before)
${\iota\mapsto\,\\!\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{chan}}}}}}\,\\{\\_,\iota^{\prime}\\}$.
By R-Recv the configuration steps to
${H[\iota\mapsto\,\\!\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{chan}}}}}}\,\\{\\_,\varnothing\\}];E[\iota^{\prime}]$..

       11. (k)

$t\equiv E[x.m(v)]$

         1. (i)

$x\in\textit{dom}(H)$ by Lemma B.17.

         2. (ii)

Given (4(k)i), we do case analysis on the shape of the value pointed by $x$ in
the store.

            * –

$x\mapsto\top$. By E-AbsentTarget the configuration steps to
$H;\textmd{Err}_{A}$.

            * –

$x\mapsto\iota$. By the assumptions of WF-Configuration,
$\iota\in\textit{dom}(H)$ (with WF-H-Var). We proceed by case analysis on
whether $m$ exists in $\overline{M}$:

              * *

$m\notin\textsf{names}(\overline{M})$. we conclude with E-NoSuchMethod and
$H;\textmd{Err}_{N}$.

              * *

$m\in\textsf{names}(\overline{M})$. we conclude by direct application of
R-Call, ${H,x^{\prime}\mapsto\iota,y^{\prime}\mapsto
v;E[t[\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{self}}}}}}=x^{\prime}][y=y^{\prime}]]$,
where $x^{\prime},y^{\prime}$ are fresh variables and $t$ is the method body
of $m$.

       12. (l)

${t\equiv E[K\
\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{copy}}}}}}\
x]$.

         1. (i)

$x\in\textit{dom}(H)$, by Lemma B.17.

         2. (ii)

By assumption (7), $x\mapsto v$ and $v=\top$ or $v=\iota$ and
$\iota\in\textit{dom}(H)$. We proceed by case analysis on $v$:

            * –

$x\mapsto\top\in H$. By E-AbsentCopyTarget the configuration steps to
$H;\textmd{Err}_{A}$..

            * –

$x\mapsto\iota\in H\land\textsf{notLocalOwner}(H,i,\iota)$. By E-CopyTarget
the configuration steps to $H;\textmd{Err}_{P}$..

            * –

$x\mapsto\iota\in H\land\textsf{localOwner}(H,i,\iota)$ By WF-Copy,
${\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{iso}}}}}}{}\neq
K$. By R-Copy the configuration steps to $H^{\prime};E[\iota]$. where
$\textsf{OkDup}(H,K,\iota)=(H^{\prime},\iota^{\prime})$ where $\iota^{\prime}$
is the fresh location to the duplicated object graph and $H^{\prime}$ is the
new store containing the duplicated object graph.

       13. (m)

${t\equiv
E[\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{spawn}}}}}}~{}(x)~{}\\{t^{\prime}\\}]$.
By well-formed configuration (WF-Configuration) with WF-Spawn,
$x\notin\textit{dom}(\Gamma)$ and
$\textsf{FreeVar}(t^{\prime})\subseteq\\{x\\}$. By Lemma B.16,
$x\notin\textit{dom}(H)$ either. We conclude by direct application of R-Spawn,
${H,x\mapsto\iota,\iota\mapsto\,\\!\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{chan}}}}}}\,\\{i,\varnothing\\};E[\iota]\
t$ where $\iota,i$ are fresh, and $t$ is a new spawned thread.

       14. (n)

$t\equiv E[\blacksquare_{\\_}i\,\iota]$. By Lemma B.17, $\iota$ in
$\textit{dom}(H)$. By well-formed configuration (WF-Configuration), we can
further assume
${\iota\mapsto\,\\!\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{chan}}}}}}\,\\{i^{\prime},v\\}$
(WF-Term). We proceed by case analysis on the index $i$ and value $v$.

          * –

$i=i^{\prime},v=\varnothing$, then by R-SendUnblock we conclude with
$H;E[\iota]$.

          * –

$i=i^{\prime},v\neq\varnothing$, then the configuration is blocked. By the
assumption of well-formed configuration WF-Configuration there is a
$t^{\prime}\in\overline{T}$ that such that it is not deadlocked. We conclude
by induction on the set of threads $\overline{T}$.

          * –

$i\neq i^{\prime},\textit{any}\ v$. By R-SendUnblock the configuration steps
to $H;\iota$..

       15. (o)

${t\equiv
E[K\,\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{obj}}}}}}\,\\{\overline{f=v}\,\overline{M}\\}]$.
We proceed by case analysis on the compatibility of the capability $K$ and the
object capability of each value, $\overline{v}$, and $\textsf{OkRef}(H,K,v)$.

          * –

$\forall v\in\overline{v}.\ \textsf{OkRef}(H,K,v)$. We proceed by case
analysis over $K$

            1. (i)

${K=\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{local}}}}}}{}$.
If all values are owned by the current thread, by R-New the configuration
steps to ${H,\iota\mapsto
K\,\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{obj}}}}}}\,\\{\overline{f=v}\,\overline{M}\\};E[\iota]$
where $\iota$ is fresh. If a value is not owned by the current thread, by
E-BadInstantiation the configuration reduces to $H;\textmd{Err}_{P}$.

            2. (ii)

${K\neq\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{local}}}}}}{}$,
by R-New the configuration steps to ${H,\iota\mapsto
K\,\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{obj}}}}}}\,\\{\overline{f=v}\,\overline{M}\\};E[\iota]$
where $\iota$ is fresh.

          * –

$\exists v\in\overline{v}.\ \neg\textsf{OkRef}(H,K,v)$ by E-BadInstantiation
the configuration reduces to $H;\textmd{Err}_{P}$.

∎

See 5.2

###### Proof.

Initial Assumptions:

$\displaystyle\Gamma\vdash H;t\ \overline{T}$ WF-Configuration

Step:

$\displaystyle H;t\ \overline{T}\rightsquigarrow
H^{\prime};\overline{T^{\prime}}\ \overline{T}$ C-Eval

Need to show:

$\displaystyle\Gamma\vdash H;\overline{T^{\prime}}\ \overline{T}$

By induction on the shape of the term $t$. If it holds for one thread, then it
will hold for all thread configurations. We use the rule C-Eval to reduce a
single thread $t$ from the bunch of threads $t\ \overline{T}$.

  1. (1)

${{t=\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{let}}}}}}~{}x~{}=~{}v~{}\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{in}}}}}}~{}t^{\prime}$.
By the induction hypothesis, with rule R-Let

${{\displaystyle
H;\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{let}}}}}}~{}x~{}=~{}v~{}\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{in}}}}}}~{}t^{\prime}\
\ \overline{T}\rightsquigarrow H^{\prime};t^{\prime}\ \overline{T}$
$\displaystyle\qquad\Rightarrow\exists\Gamma^{\prime}.\Gamma^{\prime}\supseteq\Gamma,\Gamma^{\prime};H,x\mapsto
v\vdash t^{\prime}\ \overline{T}$

From initial assumption of well-formedness and WF-Configuration:

(10) $\displaystyle\textit{dom}(\Gamma)=\textit{dom}(H)$ (11)
$\displaystyle\Gamma\vdash H$ (12) ${{\displaystyle\forall
t^{\prime\prime}\in\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{let}}}}}}~{}x~{}=~{}v~{}\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{in}}}}}}~{}t^{\prime}\
\overline{T}.\ \ \Gamma\vdash H;t^{\prime\prime}$ (13)
${{\displaystyle\textsf{Local}(H,\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{let}}}}}}~{}x~{}=~{}v~{}\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{in}}}}}}~{}t^{\prime}\
\overline{T})$ (14)
${{\displaystyle\textsf{Isolated}(H,\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{let}}}}}}~{}x~{}=~{}v~{}\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{in}}}}}}~{}t^{\prime}\
\overline{T})$

Need to show

$\exists\Gamma^{\prime}.\Gamma^{\prime}\supseteq\Gamma\land\Gamma^{\prime}\vdash
H^{\prime};t^{\prime}\ \overline{T},\textit{ where }H^{\prime}=H,x\mapsto v$

The strategy of the proof is to show that all components are well-formed. By
rule WF-Configuration, we need to show:

(15) $\displaystyle\Gamma^{\prime}\supseteq\Gamma$ (16)
$\displaystyle\textit{dom}(\Gamma^{\prime})=\textit{dom}(H^{\prime})$ (17)
$\displaystyle\Gamma^{\prime}\vdash H,x\mapsto v$ (18) $\displaystyle\forall
t^{\prime\prime}\in t^{\prime}\ \overline{T}.\Gamma^{\prime};H,x\mapsto
v\vdash t^{\prime\prime}$ (19)
$\displaystyle\textsf{Local}(H^{\prime},t^{\prime}\ \overline{T})$ (20)
$\displaystyle\textsf{Isolated}(H^{\prime},t^{\prime}\ \overline{T})$

We pick $\Gamma^{\prime}=\Gamma,x:Cap(H,x)$, and $H^{\prime}=H,x\mapsto v$. We
now proof each of the components:

     * •

We picked $\Gamma^{\prime}=\Gamma,x:Cap(H,x)$, this trivially satisfies (15),
$\Gamma^{\prime}\supseteq\Gamma$.

     * •

Show that $\textit{dom}(\Gamma^{\prime})=\textit{dom}(H^{\prime})$. We know
that $\Gamma^{\prime}=\Gamma,x:Cap(H,x)$ and $H^{\prime}=H,x\mapsto v$. To
show $\textit{dom}(\Gamma,x:Cap(H,x))=\textit{dom}(H,x\mapsto v)$:

       1. (a)

$\textit{dom}(\Gamma)=\textit{dom}(H)$ by assumption (10).

       2. (b)

Trivially, $x\in\textit{dom}(\Gamma,x:Cap(H,x))$ and
$x\in\textit{dom}(H,x\mapsto v)$.

From (1a) and (1b), we conclude that
$\textit{dom}(\Gamma^{\prime})=\textit{dom}(H^{\prime})$.

     * •

Show $\Gamma,x:Cap(H,x)\vdash H,x\mapsto v$ (17). We proceed by case analysis
on the shape of $v$.

       * –

$v=\iota$ (and by our pick of $\Gamma^{\prime}$ we have $x:Cap(H,x)$). We
proceed by checking that the environment $\Gamma^{\prime}$ is well-formed
w.r.t. $H^{\prime}$.

         1. (a)

From the assumption of well-formed threads (Eq. 12) and typing rule WF-Let:
$x\notin\textit{dom}(\Gamma)$

         2. (b)

We prove that $\iota\in\textit{dom}(H^{\prime})$

           1. (i)

From thread well-formedness assumption Eq. 12, $\Gamma\vdash
H;t^{\prime\prime}$ for all threads $t^{\prime\prime}\in t\ \overline{T}$.
From this fact and by rule WF-Term,
${{\Gamma\vdash\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{let}}}}}}~{}x~{}=~{}\iota~{}\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{in}}}}}}~{}t^{\prime}$.

           2. (ii)

By Lemma B.17 with Item 1(b)i, $\iota\in\textit{dom}(\Gamma)$.

           3. (iii)

From the initial assumption, $\textit{dom}(\Gamma)=\textit{dom}(H)$.

           4. (iv)

From Item 1(b)ii and Eq. 10 we conclude that $\iota\in\textit{dom}(H)$.

           5. (v)

From $\Gamma^{\prime}=\Gamma,x:\\_\supseteq\Gamma$ and the proved step
$\textit{dom}(\Gamma^{\prime})=\textit{dom}(H^{\prime})$, we can conclude that
$\iota\in\textit{dom}(H^{\prime})$ as $H^{\prime}\supseteq H$ and $\iota\in H$
by 1(b)iv.

         3. (c)

From the assumption $\Gamma\vdash H$, by rule WF-H-Object any
$\iota\in\textit{dom}(H)$ with capability $K$ must have had $\Gamma(\iota)=K$.
By our pick of $\Gamma^{\prime}$ where $x:Cap(H,\iota)$ and by definition of
$Cap(H,\iota)$, it follows that $\Gamma(x)=\Gamma(\iota)=K$.

         4. (d)

From assumption (11), $\Gamma\vdash H$.

From steps (1a) – (1d) and by rule WF-H-Var, we conclude that
$\Gamma,x:Cap(H,x)\vdash H,x\mapsto v$.

       * –

$v=\top$. We need to show that $x\in\textit{dom}(\Gamma)$ and
$\Gamma^{\prime}\vdash H$.

         1. (a)

By our pick of $\Gamma^{\prime}$, trivially
$x\in\textit{dom}(\Gamma^{\prime})$,

         2. (b)

By our assumption that $\Gamma\vdash H$ (11) and
$\Gamma^{\prime}\supseteq\Gamma$ and direct application of Lemma B.18,
$\Gamma^{\prime}\vdash H$

         3. (c)

From 1a and 1b and by application of rule WF-H-Absent, we conclude that
$\Gamma^{\prime}\vdash H^{\prime}$.

     * •

Show $\forall t^{\prime\prime}\in t^{\prime}\
\overline{T}.\Gamma^{\prime};H,x\mapsto v\vdash t^{\prime\prime}$. There are
multiple cases to consider. For all $t^{\prime\prime}\in\overline{T}$ and by
Lemma B.21, extending the environment and heap do not affect the well-
formedness of a thread. For the case where $t^{\prime\prime}=t^{\prime}$, we
proceed by case analysis on the shape of $t^{\prime}$.

       * –

$t^{\prime}=x$.

         1. (a)

We just proved $\Gamma,x:Cap(H,x)\vdash H,x\mapsto v$ (17).

         2. (b)

Since $x\in\textit{dom}(\Gamma,x:Cap(H,x))$ and by our assumptions of well-
formedness $\vdash\Gamma$ and $x\notin\Gamma$, by direct application of WF-
Env-Var, $\vdash\Gamma,x:Cap(H,x)$.

         3. (c)

From 1b and direct application of WF-Var, $\Gamma,x:Cap(H,x)\vdash x$.

         4. (d)

From 1a and 1c and by application of WF-Term, we conclude
$\Gamma^{\prime};H,x\mapsto v\vdash x$ which is what we had to show.

       * –

${{t^{\prime}=\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{let}}}}}}~{}x~{}=~{}e~{}\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{in}}}}}}~{}t^{\prime\prime\prime}$.
Follows the same steps as the prove for $t^{\prime}=x$.

       * –

${t^{\prime}=\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{consume}}}}}}\
x$. Follows the same steps as the prove for $t^{\prime}=x$.

       * –

$t^{\prime}=(K)~{}w$. Follows the same steps as the prove for $t^{\prime}=x$.

     * •

Show $\textsf{Local}(H^{\prime},t^{\prime}\ \overline{T})$ (19). There are
multiple cases to consider, depending on whether there is a local variable and
if this one belongs to $t^{\prime}$ or $\overline{T}$

       1. (a)

No local variables. Then the induction hypothesis is vacuously satisfied,
since there is no location to which we can apply it.

       2. (b)

$\iota\in\textsf{ROG}(H^{\prime},t^{\prime})\land\textsf{isLocal}(H,\iota)$.

         1. (i)

From the initial assumptions (13) and the $\textsf{Local}(H,t\ \overline{T})$
and $x\notin\textit{dom}(H)$ and $\iota$ is local to $t$ and
$H^{\prime}=H,x\mapsto\iota$ and by direct application of Lemma B.22,
extending the heap with a fresh variable does not affect other threads. Thus,
$\textsf{Local}(H^{\prime},\overline{T})$. With this, we know that $x$ and
$\iota$ is still not reachable from other threads.

         2. (ii)

Now, we need to show that $t^{\prime}$ maintains the thread-locality of $t$
and extending the heap does not allow to reach to local variables from other
threads.

We need to show that $\textsf{Local}(H^{\prime},t^{\prime}\ \overline{T})$.
Clearly $t^{\prime}\subseteq t$, $t^{\prime}$ only has access to the free
variables available in $t$, by the assumptions of the case, 1(b)i and by
direct application of Lemma B.24, we conclude
$\textsf{Local}(H^{\prime},t^{\prime}\ \overline{T})$.

       3. (c)

$\iota\notin\textsf{ROG}(H^{\prime},t^{\prime})\land\textsf{isLocal}(H,\iota)$.
It must be the case that $\iota$ is local to some other thread. By application
of Lemma B.22, we can conclude that $\textsf{Local}(H^{\prime},t^{\prime}\
\overline{T})$.

Thus, we can conclude that $\textsf{Local}(H^{\prime},t^{\prime}\
\overline{T})$.

     * •

Show $\textsf{Isolated}(H^{\prime},t^{\prime}\ \overline{T})$, (20). From the
initial assumption
${{\textsf{Isolated}(H,\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{let}}}}}}~{}x~{}=~{}v~{}\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{in}}}}}}~{}t\
\overline{T})$ (14), an isolate location can either be in a field or multiple
times in the stack accesible to a single thread. If there are multiple
references to it, then it must be on the stack. We consider the case where
there are multiple references, as the predicate is vacuously isolated
otherwise.

       1. (a)

Assume $\textsf{isIso}(H,v)$. Since there are multiple references we need to
further assume its owner. Assume $v$ is only accesible from
${{\textsf{Isolated}(H,\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{let}}}}}}~{}x~{}=~{}v~{}\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{in}}}}}}~{}t)$.
Then, extending the environment with a stack variable cannot break isolation,
Lemma B.23.

  2. (2)

$t=E[x]$. By the induction hypothesis,

$H;E[x]\ \overline{T}\rightsquigarrow H;\overline{T^{\prime}}\
\overline{T}\Rightarrow\exists\Gamma^{\prime}.\Gamma^{\prime}\supseteq\Gamma\land\Gamma^{\prime}\vdash
H^{\prime};\overline{T^{\prime}}\ \overline{T}$

We proceed by case analysis over the step.

R-Var:

, $H;E[x]\rightsquigarrow H;E[v]$.

From initial assumption and WF-Configuration:

(21) $\displaystyle\Gamma\vdash H;E[x]$ (22) $\displaystyle\Gamma\vdash H$
(23) $\displaystyle\forall t^{\prime}\in E[x]\ \overline{T}.\ \ \Gamma\vdash
H;t^{\prime}$ (24) $\displaystyle\textsf{Local}(H,E[x]\ \overline{T})$ (25)
$\displaystyle\textsf{Isolated}(H,E[x]\ \overline{T})$

Need to show

$\exists\Gamma^{\prime}.\Gamma^{\prime}\supseteq\Gamma\land\Gamma^{\prime}\vdash
H^{\prime};E[v]\ \overline{T},\textit{ where }H^{\prime}=H$

The strategy of the proof is to show that all components are well-formed. By
rule WF-Configuration and IH, we need to show:

(26) $\displaystyle\Gamma^{\prime}\supseteq\Gamma$ (27)
$\displaystyle\Gamma^{\prime}\vdash H^{\prime};E[v]$ (28)
$\displaystyle\Gamma^{\prime}\vdash H$ (29) $\displaystyle\forall
t^{\prime\prime}\in E[v]\ \overline{T}.\Gamma^{\prime}\vdash
H;t^{\prime\prime}$ (30) $\displaystyle\textsf{Local}(H^{\prime},E[v]\
\overline{T})$ (31) $\displaystyle\textsf{Isolated}(H^{\prime},E[v]\
\overline{T})$

We pick $\Gamma^{\prime}=\Gamma$ and $H^{\prime}=H$ by R-Var. We now proof
each of the components of the configuration:

     * •:

We picked $\Gamma^{\prime}=\Gamma,x:K$, this trivially satisfies (26).

     * •:

Show that $\Gamma^{\prime}\vdash H^{\prime};E[v]$ (27).

       1. (a):

By (21), with WF-Let and WF-Loc, we conclude that $\Gamma^{\prime}\vdash E[v]$
is well-formed

       2. (b):

By WF-Term-Let with (2a), we conclude that $\Gamma^{\prime}\vdash
H^{\prime};E[v]$.

     * •:

Show $\Gamma^{\prime}\vdash H$ (28). Trivially satisfied from (22).

     * •:

Show $\forall t^{\prime\prime}\in E[v]\ \overline{T}.\Gamma^{\prime}\vdash
H;t^{\prime\prime}$. The case for $\overline{T}$ is trivially from (23). The
case for $E[v]$ was shown in above (27).

     * •:

Show $\textsf{Local}(H^{\prime},t^{\prime}\ \overline{T})$ (30). This is
trivially satisfied from (24).

     * •:

Show $\textsf{Isolated}(H^{\prime},t^{\prime}\ \overline{T})$, (31). This is
trivially satisfied from (25).

By WF-Configuration, we conclude that $\Gamma\vdash H;E[v]\ \overline{T}$

E-AbsentVar:

$H;E[x]\rightsquigarrow H;\textmd{Err}_{A}$. From initial assumption and WF-
Configuration:

(32) $\displaystyle\Gamma\vdash H;E[x]$ (33) $\displaystyle\Gamma\vdash H$

By the equivalence rules, we immediately reduce $\textmd{Err}_{A}\
\overline{T}\equiv\textmd{Err}_{A}$.

Need to show

$\exists\Gamma^{\prime}.\Gamma^{\prime}\supseteq\Gamma\land\Gamma^{\prime}\vdash
H^{\prime};\textmd{Err}_{A},\textit{ where }H^{\prime}=H$

The strategy of the proof is to show that all components are well-formed. By
rule WF-Configuration and IH, we need to show:

(34) $\displaystyle\Gamma^{\prime}\supseteq\Gamma$ (35)
$\displaystyle\Gamma^{\prime}\vdash H^{\prime}$

We pick $\Gamma^{\prime}=\Gamma$ and $H^{\prime}=H$ by R-AbsentVar. We now
proof each of the components of the configuration:

     * •:

We picked $\Gamma^{\prime}=\Gamma$, this is trivially satisfied by (34).

     * •:

Show that $\Gamma^{\prime}\vdash H^{\prime};\textmd{Err}_{A}$. Given that
$\Gamma^{\prime}=\Gamma$ and $H=H$, this is trivially satisfied from (33).

We conclude by direct application of WF-Configuration that $\Gamma\vdash
H;\textmd{Err}_{A}$ is well-formed.

E-AliasIso:

$H;E[x]\rightsquigarrow H;\textmd{Err}_{P}$. From initial assumption and WF-
Configuration:

(37) $\displaystyle\Gamma\vdash H$

By the equivalence rules, we immediately reduce $\textmd{Err}_{P}\
\overline{T}\equiv\textmd{Err}_{P}$.

Need to show

$\exists\Gamma^{\prime}.\Gamma^{\prime}\supseteq\Gamma\land\Gamma^{\prime}\vdash
H^{\prime};\textmd{Err}_{P},\textit{ where }H^{\prime}=H$

The strategy of the proof is to show that all components are well-formed. By
rule WF-Configuration and IH, we need to show:

(38) $\displaystyle\Gamma^{\prime}\supseteq\Gamma$ (39)
$\displaystyle\Gamma^{\prime}\vdash H^{\prime}$

We pick $\Gamma^{\prime}=\Gamma$ and $H^{\prime}=H$ by R-AliasIso. We now
proof each of the components of the configuration:

     * •:

We picked $\Gamma^{\prime}=\Gamma$, this is trivially satisfied from (38).

     * •:

Show that $\Gamma^{\prime}\vdash H^{\prime};\textmd{Err}_{A}$. Given that
$\Gamma^{\prime}=\Gamma$ and $H=H$, this is trivially satisfied from (37).

We conclude by direct application of WF-Configuration that $\Gamma\vdash
H;\textmd{Err}_{P}$ is well-formed.

  3. (3)

${t=E[\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{consume}}}}}}\
x]$. By the induction hypothesis,

$\displaystyle H;E[x]\ \overline{T}\rightsquigarrow H;E[v]\ \overline{T}$
$\displaystyle\qquad\Rightarrow\exists\Gamma^{\prime}.\Gamma^{\prime}\supseteq\Gamma\land\Gamma^{\prime}\vdash
H^{\prime};E[v]\ \overline{T}$

There are two rules, which depend on whether $x$ is $\top$ or not.

R-Consume:

,
${H;E[\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{consume}}}}}}\
x]\rightsquigarrow H;E[v]$. From initial assumption and WF-Configuration:

(40) ${\displaystyle\Gamma\vdash
H;E[\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{consume}}}}}}\
x]$ (41) $\displaystyle\Gamma\vdash H$ (42) ${\displaystyle\forall
t^{\prime}\in
E[\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{consume}}}}}}\
x]\ \overline{T}.\ \ \Gamma\vdash H;t^{\prime}$ (43)
${\displaystyle\textsf{Local}(H,E[\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{consume}}}}}}\
x]\ \overline{T})$ (44)
${\displaystyle\textsf{Isolated}(H,E[\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{consume}}}}}}\
x]\ \overline{T})$

Need to show:

$\exists\Gamma^{\prime}.\Gamma^{\prime}\supseteq\Gamma\land\Gamma^{\prime}\vdash
H^{\prime};E[v]\ \overline{T}$

The strategy of the proof is to show that all components are well-formed. By
rule WF-Configuration and IH, we need to show:

(45) $\displaystyle\Gamma^{\prime}\supseteq\Gamma$ (46)
$\displaystyle\Gamma^{\prime}\vdash H^{\prime};E[v]$ (47)
$\displaystyle\Gamma^{\prime}\vdash H$ (48) $\displaystyle\forall
t^{\prime\prime}\in E[v]\ \overline{T}.\Gamma^{\prime}\vdash
H;t^{\prime\prime}$ (49) $\displaystyle\textsf{Local}(H^{\prime},E[v]\
\overline{T})$ (50) $\displaystyle\textsf{Isolated}(H^{\prime},E[v]\
\overline{T})$

We pick $\Gamma^{\prime}=\Gamma$ and $H^{\prime}=H$ by R-Consume. We now proof
each of the components of the configuration:

     * •:

We picked $\Gamma^{\prime}=\Gamma$, this trivially satisfies (45).

     * •:

Show that $\Gamma^{\prime}\vdash H^{\prime};E[v]$ (46).

       1. (a):

By WF-Let and WF-Loc with (40) we conclude that $\Gamma^{\prime}\vdash E[v]$
is well-formed.

       2. (b):

We need to show that $v=\iota\Rightarrow v\in\textit{dom}(H)$. This was part
of the initial assumptions in (40), where $x\mapsto\iota\in\textit{dom}(H)$.

       3. (c):

By WF-Term-Let with (3a) and (3b), we can conclude we conclude that
$\Gamma^{\prime}\vdash H^{\prime};E[v]$ is well-formed.

     * •:

Show $\Gamma^{\prime}\vdash H$ (47). Trivially satisfied by (41).

     * •:

Show $\forall t^{\prime\prime}\in E[v]\ \overline{T}.\Gamma^{\prime}\vdash
H;t^{\prime\prime}$. The case for $\overline{T}$ is trivially satisfied by
(42). The case for $E[v]$ was shown in above (46).

     * •:

Show $\textsf{Local}(H^{\prime},t^{\prime}\ \overline{T})$ (49). This is
trivially satisfied by (43).

     * •:

Show $\textsf{Isolated}(H^{\prime},t^{\prime}\ \overline{T})$, (50). This is
trivially satisfied by (44).

By WF-Configuration, we conclude that $\Gamma\vdash H;E[v]\ \overline{T}$

E-Consume:

${H;E[\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{consume}}}}}}\
x]\rightsquigarrow H;\textmd{Err}_{A}$ The proof follows the same steps as
E-AliasIso.

  4. (4)

$t=E[x.f]$. By the induction hypothesis,

$\displaystyle H;E[x.f]\ \overline{T}\rightsquigarrow H;\overline{T^{\prime}}\
\overline{T}$
$\displaystyle\qquad\Rightarrow\exists\Gamma^{\prime}.\Gamma^{\prime}\supseteq\Gamma\land\Gamma^{\prime}\vdash
H^{\prime};\overline{T^{\prime}}\ \overline{T}$

There are multiple reductions rules based on whether $x$ maps to $\top$ value
(E-AbsentTarget), field $f$ does not exist in the object pointed by $x$
(E-NoSuchField), when the field access is to an isolate E-IsoField and when
the field access is not to an isolate (R-Field). We proceed by case analysis
on the step.

R-Field:

, $H;E[x.f]\rightsquigarrow H;E[v]$. From initial assumption and WF-
Configuration:

(51) $\displaystyle x\mapsto\iota\in H$ (52) ${\displaystyle
H(\iota)=\\_\,\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{obj}}}}}}\,\\{\\_\
f=v\,\overline{M}\\}$ (53) $\displaystyle\neg\textsf{isIso}(H,v)$ (54)
$\displaystyle\Gamma\vdash H;E[x.f]$ (55) $\displaystyle\Gamma\vdash H$ (56)
$\displaystyle\forall t^{\prime}\in E[x.f]\ \overline{T}.\ \ \Gamma\vdash
H;t^{\prime}$ (57) $\displaystyle\textsf{Local}(H,E[x.f]\ \overline{T})$ (58)
$\displaystyle\textsf{Isolated}(H,E[x.f]\ \overline{T})$

Need to show:

$\exists\Gamma^{\prime}.\Gamma^{\prime}\supseteq\Gamma\land\Gamma^{\prime}\vdash
H^{\prime};E[v]\ \overline{T}$

The strategy of the proof is to show that all components are well-formed. By
rule WF-Configuration and IH, we need to show:

(59) $\displaystyle\Gamma^{\prime}\supseteq\Gamma$ (60)
$\displaystyle\Gamma^{\prime}\vdash H^{\prime};E[v]$ (61)
$\displaystyle\Gamma^{\prime}\vdash H$ (62) $\displaystyle\forall
t^{\prime\prime}\in E[v]\ \overline{T}.\Gamma^{\prime}\vdash
H;t^{\prime\prime}$ (63) $\displaystyle\textsf{Local}(H^{\prime},E[v]\
\overline{T})$ (64) $\displaystyle\textsf{Isolated}(H^{\prime},E[v]\
\overline{T})$

We pick $\Gamma^{\prime}=\Gamma$ and $H^{\prime}=H$ by R-Field. We now proof
each of the components of the configuration:

     * •:

We picked $\Gamma^{\prime}=\Gamma$, this trivially satisfies (59).

     * •:

Show that $\Gamma^{\prime}\vdash H^{\prime};E[v]$ (60).

       1. (a):

By WF-Let and WF-Loc with (54), we conclude that $\Gamma^{\prime}\vdash E[v]$
is well-formed.

       2. (b):

By initial assumptions (51), (52), (53), we have that $x\mapsto\iota\in H$ and
$\iota\in\textit{dom}(H)$ and $H(x.f)=v$ and $v$ is not isolated.

       3. (c):

By WF-Term-Let with (4a) and (4b), we can conclude we conclude that
$\Gamma^{\prime}\vdash H^{\prime};E[v]$ is well-formed.

     * •:

Show $\Gamma^{\prime}\vdash H$ (61). Trivially satisfied by (55).

     * •:

Show $\forall t^{\prime\prime}\in E[v]\ \overline{T}.\Gamma^{\prime}\vdash
H;t^{\prime\prime}$. The case for $\overline{T}$ is trivially saitisfied by
(56). The case for $E[v]$ was shown in above (60).

     * •:

Show $\textsf{Local}(H^{\prime},E[v]\ \overline{T})$ (63). This is trivially
satisfied by (57).

     * •:

Show $\textsf{Isolated}(H^{\prime},E[v]\ \overline{T})$, (64). This is
vacuously satisfied by (58) and (53), since $H(x.f)=v$ and $v$ is not an
isolate.

By WF-Configuration, we conclude that $\Gamma\vdash H;E[v]\ \overline{T}$ is
well-formed.

E-NoSuchField:

$H;E[x.f]\rightsquigarrow H;\textmd{Err}_{N}$

From initial assumption and WF-Configuration:

(65) $\displaystyle f\textit{ does not exist in the object}$ (66)
$\displaystyle\Gamma\vdash H$

By the equivalence rules, we immediately reduce $\textmd{Err}_{N}\
\overline{T}\equiv\textmd{Err}_{N}$. Need to show

$\exists\Gamma^{\prime}.\Gamma^{\prime}\supseteq\Gamma\land\Gamma^{\prime}\vdash
H^{\prime};\textmd{Err}_{N},\textit{ where }H^{\prime}=H$

The strategy of the proof is to show that all components are well-formed. By
rule WF-Configuration and IH, we need to show:

(67) $\displaystyle\Gamma^{\prime}\supseteq\Gamma$ (68)
$\displaystyle\Gamma^{\prime}\vdash H^{\prime}$

We pick $\Gamma^{\prime}=\Gamma$ and $H^{\prime}=H$ by E-NoSuchField. We now
proof each of the components of the configuration:

     * •:

We picked $\Gamma^{\prime}=\Gamma$, this is trivially satisfied by (67).

     * •:

Show that $\Gamma^{\prime}\vdash H^{\prime};\textmd{Err}_{N}$. Given that
$\Gamma^{\prime}=\Gamma$ and $H=H$, this is trivially satisfied from initial
assumption (66).

We conclude by direct application of WF-Configuration that $\Gamma\vdash
H;\textmd{Err}_{N}$ is well-formed.

E-AbsentTargetAccess:

, $H;E[x.f]\rightsquigarrow H;\textmd{Err}_{A}$. From initial assumption and
WF-Configuration:

(70) $\displaystyle H(x)=\top$ (71) $\displaystyle\Gamma\vdash H$

By the equivalence rules, we immediately reduce $\textmd{Err}_{A}\
\overline{T}\equiv\textmd{Err}_{A}$. Need to show

$\exists\Gamma^{\prime}.\Gamma^{\prime}\supseteq\Gamma\land\Gamma^{\prime}\vdash
H^{\prime};\textmd{Err}_{A},\textit{ where }H^{\prime}=H$

The strategy of the proof is to show that all components are well-formed. By
rule WF-Configuration and IH, we need to show:

(72) $\displaystyle\Gamma^{\prime}\supseteq\Gamma$ (73)
$\displaystyle\Gamma^{\prime}\vdash H^{\prime}$

We pick $\Gamma^{\prime}=\Gamma$ and $H^{\prime}=H$ by E-AbsentTargetAccess.
We now proof each of the components of the configuration:

     * •:

We picked $\Gamma^{\prime}=\Gamma$, this trivially satisfies (72).

     * •:

Show that $\Gamma^{\prime}\vdash H^{\prime};\textmd{Err}_{A}$. Given that
$\Gamma^{\prime}=\Gamma$ and $H=H$, this is trivially satisfied with (71).

We conclude by direct application of WF-Configuration that $\Gamma\vdash
H;\textmd{Err}_{A}$ is well-formed.

E-LocalField:

, $H;E[x.f]^{i}\rightsquigarrow H;\textmd{Err}_{P}$. From initial assumption
and WF-Configuration:

(74) $\displaystyle H(x.f)=\iota$ (75)
$\displaystyle\textsf{notLocalOwner}(H,i,\iota)$ (76)
$\displaystyle\Gamma\vdash H$

By the equivalence rules, we immediately reduce $\textmd{Err}_{P}\
\overline{T}\equiv\textmd{Err}_{P}$. Need to show

$\exists\Gamma^{\prime}.\Gamma^{\prime}\supseteq\Gamma\land\Gamma^{\prime}\vdash
H^{\prime};\textmd{Err}_{P},\textit{ where }H^{\prime}=H$

The strategy of the proof is to show that all components are well-formed. By
rule WF-Configuration and IH, we need to show:

(77) $\displaystyle\Gamma^{\prime}\supseteq\Gamma$ (78)
$\displaystyle\Gamma^{\prime}\vdash H^{\prime}$

We pick $\Gamma^{\prime}=\Gamma$ and $H^{\prime}=H$ by E-LocalField. We now
proof each of the components of the configuration:

     * •:

We picked $\Gamma^{\prime}=\Gamma$, this is trivially satisfied by (77).

     * •:

Show that $\Gamma^{\prime}\vdash H^{\prime};\textmd{Err}_{P}$. Given that
$\Gamma^{\prime}=\Gamma$ and $H=H$, this is trivially satisfied by (76).

We conclude by direct application of WF-Configuration that $\Gamma\vdash
H;\textmd{Err}_{P}$ is well-formed.

E-IsoField:

, $H;E[x.f]\rightsquigarrow H;\textmd{Err}_{P}$. From initial assumption and
WF-Configuration:

(79) $\displaystyle H(x.f)=\iota$ (80) $\displaystyle\textsf{isIso}(H,\iota)$
(81) $\displaystyle\Gamma\vdash H$

By the equivalence rules, we immediately reduce $\textmd{Err}_{P}\
\overline{T}\equiv\textmd{Err}_{P}$. Need to show

$\exists\Gamma^{\prime}.\Gamma^{\prime}\supseteq\Gamma\land\Gamma^{\prime}\vdash
H^{\prime};\textmd{Err}_{P},\textit{ where }H^{\prime}=H$

The strategy of the proof is to show that all components are well-formed. By
rule WF-Configuration and IH, we need to show:

(82) $\displaystyle\Gamma^{\prime}\supseteq\Gamma$ (83)
$\displaystyle\Gamma^{\prime}\vdash H^{\prime}$

We pick $\Gamma^{\prime}=\Gamma$ and $H^{\prime}=H$ by E-IsoField. We now
proof each of the components of the configuration:

     * •:

We picked $\Gamma^{\prime}=\Gamma$, this is trivially satisfied by (82).

     * •:

Show that $\Gamma^{\prime}\vdash H^{\prime};\textmd{Err}_{P}$. Given that
$\Gamma^{\prime}=\Gamma$ and $H=H$, this is trivially satisfied by (81).

We conclude by direct application of WF-Configuration that $\Gamma\vdash
H;\textmd{Err}_{P}$ is well-formed.

  5. (5)

$t=E[x.f=v]$. By the induction hypothesis,

$\displaystyle H;E[x.f=v]\ \overline{T}\rightsquigarrow
H;\overline{T^{\prime}}\ \overline{T}$
$\displaystyle\qquad\Rightarrow\exists\Gamma^{\prime}.\Gamma^{\prime}\supseteq\Gamma\land\Gamma^{\prime}\vdash
H^{\prime};\overline{T^{\prime}}\ \overline{T}$

There are multiple cases to handle, depending on whether the variable $x$ is
$\top$ (E-AbsentFieldAssign), whether field $f$ exists (E-NoSuchFieldAssign),
whether $x$ is immutable or the capability of $x$ is compatible with the
capability of the value $v$ (E-BadFieldAssign), and finally the case where $x$
is not immutable and the capability of $v$ is compatible with the capability
of $x$ (R-FieldAssign). We proceed by case analysis over the step.

E-AbsentFieldAssign:

, $H;E[x.f=v]\rightsquigarrow H;\textmd{Err}_{A}$.

From initial assumption and WF-Configuration:

(84) $\displaystyle H(x)=\top$ (85) $\displaystyle\Gamma\vdash H$

By the equivalence rules, we immediately reduce $\textmd{Err}_{A}\
\overline{T}\equiv\textmd{Err}_{A}$. Need to show

$\exists\Gamma^{\prime}.\Gamma^{\prime}\supseteq\Gamma\land\Gamma^{\prime}\vdash
H^{\prime};\textmd{Err}_{A},\textit{ where }H^{\prime}=H$

The strategy of the proof is to show that all components are well-formed. By
rule WF-Configuration and IH, we need to show:

(86) $\displaystyle\Gamma^{\prime}\supseteq\Gamma$ (87)
$\displaystyle\Gamma^{\prime}\vdash H^{\prime}$

We pick $\Gamma^{\prime}=\Gamma$ and $H^{\prime}=H$ by E-AbsentFieldAssign. We
now proof each of the components of the configuration:

     * •:

We picked $\Gamma^{\prime}=\Gamma$, which trivially satisfies (86).

     * •:

Show that $\Gamma^{\prime}\vdash H^{\prime};\textmd{Err}_{A}$. Given that
$\Gamma^{\prime}=\Gamma$ and $H=H$, this is trivially satisfied with (85).

We conclude by direct application of WF-Configuration that $\Gamma\vdash
H;\textmd{Err}_{A}$ is well-formed.

E-BadFieldAssign:

, $H;E[x.f=v]\rightsquigarrow H;\textmd{Err}_{P}$.

Assumptions: From initial assumption and WF-Configuration:

(88) $\displaystyle H(x)=\iota$ (89) ${\displaystyle
H(\iota)=K\,\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{obj}}}}}}\,\\{\\_f=v\,\overline{M}\\}$
(90) $\displaystyle\textsf{isImm}(H,\iota)\lor\neg\textsf{OkRef}(H,K,v)$ (91)
$\displaystyle\Gamma\vdash H$

By the equivalence rules, we immediately reduce $\textmd{Err}_{P}\
\overline{T}\equiv\textmd{Err}_{P}$. Need to show

$\exists\Gamma^{\prime}.\Gamma^{\prime}\supseteq\Gamma\land\Gamma^{\prime}\vdash
H^{\prime};\textmd{Err}_{P},\textit{ where }H^{\prime}=H$

The strategy of the proof is to show that all components are well-formed. By
rule WF-Configuration and IH, we need to show:

(92) $\displaystyle\Gamma^{\prime}\supseteq\Gamma$ (93)
$\displaystyle\Gamma^{\prime}\vdash H^{\prime}$

We pick $\Gamma^{\prime}=\Gamma$ and $H^{\prime}=H$ by E-BadFieldAssign. We
now proof each of the components of the configuration:

     * •:

We picked $\Gamma^{\prime}=\Gamma$, this trivially satisfies (92).

     * •:

Show that $\Gamma^{\prime}\vdash H^{\prime};\textmd{Err}_{P}$. Given that
$\Gamma^{\prime}=\Gamma$ and $H=H$, this is trivially satisfied by the
assumption (91).

We conclude by direct application of WF-Configuration that $\Gamma\vdash
H;\textmd{Err}_{P}$ is well-formed.

E-NoSuchFieldAssign:

, $H;E[x.f=v]\rightsquigarrow H;\textmd{Err}_{N}$.

From initial assumption and WF-Configuration:

(94) $\displaystyle f\textit{ does not exist in the object}$ (95)
$\displaystyle\Gamma\vdash H$

By the equivalence rules, we immediately reduce $\textmd{Err}_{N}\
\overline{T}\equiv\textmd{Err}_{N}$. Need to show

$\exists\Gamma^{\prime}.\Gamma^{\prime}\supseteq\Gamma\land\Gamma^{\prime}\vdash
H^{\prime};\textmd{Err}_{N},\textit{ where }H^{\prime}=H$

The strategy of the proof is to show that all components are well-formed. By
rule WF-Configuration and IH, we need to show:

(96) $\displaystyle\Gamma^{\prime}\supseteq\Gamma$ (97)
$\displaystyle\Gamma^{\prime}\vdash H^{\prime}$

We pick $\Gamma^{\prime}=\Gamma$ and $H^{\prime}=H$ by E-NoSuchFieldAssign. We
now proof each of the components of the configuration:

     * •:

We picked $\Gamma^{\prime}=\Gamma$, this trivially satisfies (96).

     * •:

Show that $\Gamma^{\prime}\vdash H^{\prime};\textmd{Err}_{N}$. Given that
$\Gamma^{\prime}=\Gamma$ and $H=H$, this is trivially satisfied by the
assumption (95).

We conclude by direct application of WF-Configuration that $\Gamma\vdash
H;\textmd{Err}_{N}$ is well-formed.

R-FieldAssign:

, $H;E[x.f=v]\rightsquigarrow H;E[v^{\prime}]$.

From initial assumption and WF-Configuration:

(98) $\displaystyle x\mapsto\iota\in H$ (99) ${\displaystyle
H(\iota)=K\,\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{obj}}}}}}\,\\{\\_\
f=v^{\prime}\,\overline{M}\\}$ (100)
$\displaystyle\neg\textsf{isImm}(H,\iota)$ (101)
$\displaystyle\textsf{OkRef}(H,K,v)$ (102) $\displaystyle\Gamma\vdash
H;E[x.f=v]$ (103) $\displaystyle\Gamma\vdash H$ (104) $\displaystyle\forall
t^{\prime}\in E[x.f=v]\ \overline{T}.\ \ \Gamma\vdash H;t^{\prime}$ (105)
$\displaystyle\textsf{Local}(H,E[x.f=v]\ \overline{T})$ (106)
$\displaystyle\textsf{Isolated}(H,E[x.f=v]\ \overline{T})$

Need to show:

$\exists\Gamma^{\prime}.\Gamma^{\prime}\supseteq\Gamma\land\Gamma^{\prime}\vdash
H^{\prime};E[v^{\prime}]\ \overline{T}$

The strategy of the proof is to show that all components are well-formed. By
rule WF-Configuration and IH, we need to show:

(107) $\displaystyle\Gamma^{\prime}\supseteq\Gamma$ (108)
$\displaystyle\Gamma^{\prime}\vdash H$ (109)
$\displaystyle\Gamma^{\prime}\vdash H^{\prime};E[v^{\prime}]$ (110)
$\displaystyle\forall t^{\prime\prime}\in E[v^{\prime}]\
\overline{T}.\Gamma^{\prime}\vdash H;t^{\prime\prime}$ (111)
$\displaystyle\textsf{Local}(H^{\prime},E[v^{\prime}]\ \overline{T})$ (112)
$\displaystyle\textsf{Isolated}(H^{\prime},E[v^{\prime}]\ \overline{T})$

We pick $\Gamma^{\prime}=\Gamma$ and ${H^{\prime}=H[\iota\mapsto
K\,\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{obj}}}}}}\,\\{\\_f=v^{\prime}\,\overline{M}\\}]$
by R-FieldAssign. We now proof each of the components of the configuration:

     * •:

We picked $\Gamma^{\prime}=\Gamma$, this trivially satisfies (107).

     * •:

Show $\Gamma^{\prime}\vdash H^{\prime}$ (108). To do this, it amounts to
showing that the object is still well-formed after field substitution.

       1. (a):

Show that substituting
${K\,\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{obj}}}}}}\,\\{\\_\
f=v^{\prime}\,\overline{M}\\}$ by
${K\,\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{obj}}}}}}\,\\{\\_\
f=v\,\overline{M}\\}$ maintains well-formedness. To do this, we first show
that all fields in the object satisfy
$\textsf{OkRefEnv}(\Gamma^{\prime},K,v)$. For all fields where $v\neq
v^{\prime}$, this is satisfied by the assumption (102). When $f=v$, with (103)
guarantees that $\Gamma(l)=K$, the assumptions of the reduction rule (101)
guarantees that $\textsf{OkRef}(H,K,v)$, and by WF-H-Object with
$\textsf{OkRefEnv}(\Gamma,K,v)$, we can conclude that ${\Gamma\vdash
H,\iota\mapsto
K\,\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{obj}}}}}}\,\\{\\_f=v\,\overline{M}\\}$
is well-formed.

       2. (b):

By the well-formed configuration rules with (5a), we conclude that
$\Gamma^{\prime}\vdash H^{\prime}$.

     * •:

Show that $\Gamma^{\prime}\vdash H^{\prime};E[v]$ (109).

       1. (a):

By the assumption WF-Let and WF-Loc with (102), we conclude that
$\Gamma^{\prime}\vdash E[v]$ is well-formed.

       2. (b):

By the initial assumptions (98), (99), (100), then $x\mapsto\iota\in H$ and
$\iota\in\textit{dom}(H)$ and $H(x.f)=v^{\prime}$ and $K$ is not immutable.

       3. (c):

By WF-Term-Let with (5a) and (5b), we can conclude we conclude that
$\Gamma^{\prime}\vdash H^{\prime};E[v^{\prime}]$ is well-formed.

     * •:

Show $\forall t^{\prime\prime}\in E[v^{\prime}]\
\overline{T}.\Gamma^{\prime}\vdash H;t^{\prime\prime}$. The case for
$\overline{T}$ is trivially saitisfied by the assumptions, (104). The case for
$E[v]$ was shown above (109).

     * •:

Show $\textsf{Local}(H^{\prime},E[v^{\prime}]\ \overline{T})$ (111). This is
trivially satisfied by the assumption (105).

     * •:

Show $\textsf{Isolated}(H^{\prime},E[v^{\prime}]\ \overline{T})$, (112). This
is vacuously satisfied by the assumption (106).

By WF-Configuration, we conclude that $\Gamma\vdash H;E[v^{\prime}]\
\overline{T}$ is well-formed.

  6. (6)

$t=E[(K)~{}\iota]$. By the induction hypothesis,

$\displaystyle H;E[(K)~{}\iota]\ \overline{T}\rightsquigarrow
H;\overline{T^{\prime}}\ \overline{T}$
$\displaystyle\qquad\Rightarrow\exists\Gamma^{\prime}.\Gamma^{\prime}\supseteq\Gamma\land\Gamma^{\prime}\vdash
H^{\prime};\overline{T^{\prime}}\ \overline{T}$

There are multiple cases to handle, depending on whether the location matches
the casted capability or not. We proceed by case analysis over the step.

R-CastLoc:

, $H;E[(K)~{}\iota]\rightsquigarrow H;E[\iota]$.

From initial assumption and WF-Configuration:

(113) ${\displaystyle
H(\iota)=K\,\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{obj}}}}}}\,\\{\\_\,\\_\\}$
(114) $\displaystyle\Gamma\vdash H;E[(K)~{}\iota]$ (115) $\displaystyle\forall
t^{\prime}\in E[(K)~{}\iota]\ \overline{T}.\ \ \Gamma\vdash H;t^{\prime}$
(116) $\displaystyle\textsf{Local}(H,E[(K)~{}\iota]\ \overline{T})$ (117)
$\displaystyle\textsf{Isolated}(H,E[(K)~{}\iota]\ \overline{T})$

Need to show:

$\exists\Gamma^{\prime}.\Gamma^{\prime}\supseteq\Gamma\land\Gamma^{\prime}\vdash
H^{\prime};\overline{T^{\prime}}\ \overline{T}$

The strategy of the proof is to show that all components are well-formed. By
rule WF-Configuration and IH, we need to show:

(118) $\displaystyle\Gamma^{\prime}\supseteq\Gamma$ (119)
$\displaystyle\Gamma^{\prime}\vdash H$ (120)
$\displaystyle\Gamma^{\prime}\vdash H^{\prime};E[v^{\prime}]$ (121)
$\displaystyle\forall t^{\prime\prime}\in E[v^{\prime}]\
\overline{T}.\Gamma^{\prime}\vdash H;t^{\prime\prime}$ (122)
$\displaystyle\textsf{Local}(H^{\prime},E[v^{\prime}]\ \overline{T})$ (123)
$\displaystyle\textsf{Isolated}(H^{\prime},E[v^{\prime}]\ \overline{T})$

We pick $\Gamma^{\prime}=\Gamma$, and $H^{\prime}=H$ and
$\overline{T^{\prime}}=E[\iota]$ by R-CastLoc. We now proof each of the
components of the configuration:

     * •:

We picked $\Gamma^{\prime}=\Gamma$, this trivially satisfies (118).

     * •:

Show $\Gamma^{\prime}\vdash H^{\prime}$ (119). This is trivially satisfied
from (114).

     * •:

Show that $\Gamma^{\prime}\vdash H^{\prime};E[\iota]$ (120). This is trivially
satisfied from assumption (114).

     * •:

Show $\forall t^{\prime\prime}\in E[\iota]\ \overline{T}.\Gamma^{\prime}\vdash
H;t^{\prime\prime}$. The case for $\overline{T}$ is trivially satisfied by the
assumptions, (115). The case for $E[\iota]$ was shown above (120).

     * •:

Show $\textsf{Local}(H^{\prime},E[\iota]\ \overline{T})$ (122). This is
trivially satisfied from (116).

     * •:

Show $\textsf{Isolated}(H^{\prime},E[\iota]\ \overline{T})$, (123). This is
vacuously satisfied from (117).

By WF-Configuration, we conclude that $\Gamma\vdash H;E[\iota]\ \overline{T}$
is well-formed.

E-CastError:

, $H;E[(K)~{}\iota]\rightsquigarrow H;\textmd{Err}_{C}$.

From initial assumption and WF-Configuration:

(124) ${\displaystyle
H(\iota)=K^{\prime}\,\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{obj}}}}}}\,\\{\\_\,\\_\\}\
\quad\textit{where }K\neq K^{\prime}$ (125) $\displaystyle\Gamma\vdash H$

By the equivalence rules, we immediately reduce $\textmd{Err}_{C}\
\overline{T}\equiv\textmd{Err}_{C}$. Need to show

$\exists\Gamma^{\prime}.\Gamma^{\prime}\supseteq\Gamma\land\Gamma^{\prime}\vdash
H^{\prime};\textmd{Err}_{N},\textit{ where }H^{\prime}=H$

The strategy of the proof is to show that all components are well-formed. By
rule WF-Configuration and IH, we need to show:

(126) $\displaystyle\Gamma^{\prime}\supseteq\Gamma$ (127)
$\displaystyle\Gamma^{\prime}\vdash H^{\prime}$

We pick $\Gamma^{\prime}=\Gamma$ and $H^{\prime}=H$ by E-CastError. We now
proof each of the components of the configuration:

     * •:

We picked $\Gamma^{\prime}=\Gamma$, this trivially satisfies (126).

     * •:

Show that $\Gamma^{\prime}\vdash H^{\prime};\textmd{Err}_{C}$. Given that
$\Gamma^{\prime}=\Gamma$ and $H=H$, this is trivially satisfied by the
assumption (125).

We conclude by direct application of WF-Configuration that $\Gamma\vdash
H;\textmd{Err}_{C}$ is well-formed.

  7. (7)

${t=E[K\,\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{obj}}}}}}\,\\{\overline{f=v}\,\overline{M}\\}]$.
By the induction hypothesis,

${\displaystyle
H;E[K\,\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{obj}}}}}}\,\\{\overline{f=v}\,\overline{M}\\}]\
\overline{T}\rightsquigarrow H;\overline{T^{\prime}}\ \overline{T}$
$\displaystyle\qquad\Rightarrow\exists\Gamma^{\prime}.\Gamma^{\prime}\supseteq\Gamma\land\Gamma^{\prime}\vdash
H^{\prime};\overline{T^{\prime}}\ \overline{T}$

There are multiple cases to handle, depending on whether object fields are
compatible (R-New) or not (E-BadInstantiation). We proceed by case analysis
over the step.

R-New:

,
${H;E[K\,\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{obj}}}}}}\,\\{\overline{f=v}\,\overline{M}\\}]\rightsquigarrow
H^{\prime};E[\iota]$.

From initial assumption and WF-Configuration:

(128) ${\displaystyle\Gamma\vdash
H;E[K\,\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{obj}}}}}}\,\\{\overline{f=v}\,\overline{M}\\}]$
(129) $\displaystyle\forall v\in\overline{v}.\ \textsf{OkRef}(H,K,v)$ (130)
${\displaystyle\forall t^{\prime}\in
E[K\,\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{obj}}}}}}\,\\{\overline{f=v}\,\overline{M}\\}]\
\overline{T}.\ \ \Gamma\vdash H;t^{\prime}$ (131)
${\displaystyle\textsf{Local}(H,E[K\,\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{obj}}}}}}\,\\{\overline{f=v}\,\overline{M}\\}]\
\overline{T})$ (132)
${\displaystyle\textsf{Isolated}(H,E[K\,\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{obj}}}}}}\,\\{\overline{f=v}\,\overline{M}\\}]\
\overline{T})$

Need to show:

$\exists\Gamma^{\prime}.\Gamma^{\prime}\supseteq\Gamma\land\Gamma^{\prime}\vdash
H^{\prime};\overline{T^{\prime}}\ \overline{T}$

The strategy of the proof is to show that all components are well-formed. By
rule WF-Configuration and IH, we need to show:

(133) $\displaystyle\Gamma^{\prime}\supseteq\Gamma$ (134)
$\displaystyle\Gamma^{\prime}\vdash H$ (135)
$\displaystyle\Gamma^{\prime}\vdash H^{\prime};E[\iota]$ (136)
$\displaystyle\forall t^{\prime\prime}\in E[\iota]\
\overline{T}.\Gamma^{\prime}\vdash H;t^{\prime\prime}$ (137)
$\displaystyle\textsf{Local}(H^{\prime},E[\iota]\ \overline{T})$ (138)
$\displaystyle\textsf{Isolated}(H^{\prime},E[\iota]\ \overline{T})$

We pick $\Gamma^{\prime}=\Gamma,\iota:K$, and ${H^{\prime}=H,\iota\mapsto
K\,\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{obj}}}}}}\,\\{\overline{f=v}\,\overline{M}\\}$
and $\overline{T^{\prime}}=E[\iota]$ by R-New. We now proof each of the
components of the configuration:

     * •:

We picked $\Gamma^{\prime}=\Gamma,\iota:K$, this trivially satisfies (133).

     * •:

Show $\Gamma^{\prime}\vdash H^{\prime}$ (134). To show that
${\Gamma,\iota:K\vdash H,\iota\mapsto
K\,\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{obj}}}}}}\,\\{\overline{f=v}\,\overline{M}\\}$,
we proceed by proving well-formedness from each component in rule WF-H-Object.

       1. (a):

By assumption 129 values are compatible with the object capability.

       2. (b):

By assumption 128, all values are in $\Gamma$.

       3. (c):

From our choosing of $\Gamma^{\prime}$, $\Gamma^{\prime}(\iota)=K$.

       4. (d):

By WF-H-Object and Helper-OkRefEnv with (7a) and (7b), we conclude that
$\Gamma^{\prime}\vdash H^{\prime}$.

     * •:

Show that $\Gamma^{\prime}\vdash H^{\prime};E[\iota]$ (135). This is trivially
satisfied from assumption (128) with (134).

     * •:

Show $\forall t^{\prime\prime}\in E[\iota]\ \overline{T}.\Gamma^{\prime}\vdash
H;t^{\prime\prime}$. The case for $\overline{T}$ is trivially satisfied by the
assumptions, (130). The case for $E[\iota]$ was shown above (135).

     * •:

Show $\textsf{Local}(H^{\prime},E[\iota]\ \overline{T})$ (137). This is
trivially satisfied by the assumptions (131).

     * •:

Show $\textsf{Isolated}(H^{\prime},E[\iota]\ \overline{T})$, (138). This is
satisfied by the assumptions, (132).

By WF-Configuration, we conclude that $\Gamma\vdash H;E[\iota]\ \overline{T}$
is well-formed.

E-BadInstantiation:

,
${H;E[K\,\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{obj}}}}}}\,\\{\overline{f=v}\,\overline{M}\\}]\rightsquigarrow
H;\textmd{Err}_{P}$.

From initial assumption and WF-Configuration:

(139) $\displaystyle\Gamma\vdash H$

By the equivalence rules, we immediately reduce $\textmd{Err}_{P}\
\overline{T}\equiv\textmd{Err}_{P}$. Need to show

$\exists\Gamma^{\prime}.\Gamma^{\prime}\supseteq\Gamma\land\Gamma^{\prime}\vdash
H^{\prime};\textmd{Err}_{P},\textit{ where }H^{\prime}=H$

The strategy of the proof is to show that all components are well-formed. By
rule WF-Configuration and IH, we need to show:

(140) $\displaystyle\Gamma^{\prime}\supseteq\Gamma$ (141)
$\displaystyle\Gamma^{\prime}\vdash H^{\prime}$

We pick $\Gamma^{\prime}=\Gamma$ and $H^{\prime}=H$ by E-BadInstantiation. We
now proof each of the components of the configuration:

     * •:

We picked $\Gamma^{\prime}=\Gamma$, this is trivially satisfied by (140).

     * •:

Show that $\Gamma^{\prime}\vdash H^{\prime};\textmd{Err}_{P}$. Given that
$\Gamma^{\prime}=\Gamma$ and $H=H$, this is trivially satisfied by the
assumption (139).

We conclude by direct application of WF-Configuration that $\Gamma\vdash
H;\textmd{Err}_{P}$ is well-formed.

  8. (8)

$t=E[x.m(v)]$. By the induction hypothesis,

$\displaystyle H;E[x.m(v)]\ \overline{T}\rightsquigarrow
H;\overline{T^{\prime}}\ \overline{T}$
$\displaystyle\qquad\Rightarrow\exists\Gamma^{\prime}.\Gamma^{\prime}\supseteq\Gamma\land\Gamma^{\prime}\vdash
H^{\prime};\overline{T^{\prime}}\ \overline{T}$

There are multiple cases to handle, depending on whether object exists
(R-Call) or not (E-AbsentTarget) and whether $m$ is a valid method name We
proceed by case analysis over the step.

R-Call:

, ${H;E[x.m(v)]\rightsquigarrow
H;E[t[\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{self}}}}}}{}=x^{\prime}][y=y^{\prime}]]$.
From initial assumption and WF-Configuration:

(142) ${\displaystyle H(x)=\iota\land
H(\iota)=K\,\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{obj}}}}}}\,\\{\\_\,\overline{M}\\}\land
m\in\overline{M}$ (143) $\displaystyle\Gamma\vdash H;E[x.m(v)]$ (144)
$\displaystyle\forall t^{\prime}\in E[x.m(v)]\ \overline{T}.\ \ \Gamma\vdash
H;t^{\prime}$ (145) $\displaystyle\textsf{Local}(H,E[x.m(v)]\ \overline{T})$
(146) $\displaystyle\textsf{Isolated}(H,E[x.m(v)]\ \overline{T})$

Need to show:

$\exists\Gamma^{\prime}.\Gamma^{\prime}\supseteq\Gamma\land\Gamma^{\prime}\vdash
H^{\prime};\overline{T^{\prime}}\ \overline{T}$

The strategy of the proof is to show that all components are well-formed. By
rule WF-Configuration and IH, we need to show:

(147) $\displaystyle\Gamma^{\prime}\supseteq\Gamma$ (148)
$\displaystyle\Gamma^{\prime}\vdash H$ (149)
${\displaystyle\Gamma^{\prime}\vdash
H^{\prime};E[t[\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{self}}}}}}{}=x^{\prime}][y=y^{\prime}]]$
(150) ${\displaystyle\forall t^{\prime\prime}\in
E[t[\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{self}}}}}}{}=x^{\prime}][y=y^{\prime}]]\
\overline{T}.\Gamma^{\prime}\vdash H;t^{\prime\prime}$ (151)
${\displaystyle\textsf{Local}(H^{\prime},E[t[\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{self}}}}}}{}=x^{\prime}][y=y^{\prime}]]\
\overline{T})$ (152)
${\displaystyle\textsf{Isolated}(H^{\prime},E[t[\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{self}}}}}}{}=x^{\prime}][y=y^{\prime}]]\
\overline{T})$

We pick $\Gamma^{\prime}=\Gamma,x^{\prime}:K,y^{\prime}:\Gamma(v)$, and
$H^{\prime}=H,x^{\prime}\mapsto\iota,y^{\prime}\mapsto v$ and
${\overline{T^{\prime}}=E[t[\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{self}}}}}}{}=x^{\prime}][y=y^{\prime}]]$
by R-Call. We now proof each of the components of the configuration:

     * •:

We picked $\Gamma^{\prime}=\Gamma,,x^{\prime}:K,y^{\prime}:\Gamma(v)$, this
trivially satisfies (147).

     * •:

Show $\Gamma^{\prime}\vdash H^{\prime}$ (148). To show that
$\Gamma,x^{\prime}:K,y^{\prime}:\Gamma(v)\vdash H,x^{\prime}\mapsto\iota
y^{\prime}\mapsto v$, it suffices to show that their capabilities match. By
the assumptions (143), $x$ and $\iota$ have capability $K$, and from WF-H-Var,
we conclude that $\Gamma^{\prime}\vdash H,x^{\prime}\mapsto\iota$. Repeating
these steps for $y$, lets us conclude $\Gamma^{\prime}\vdash H^{\prime}$.

     * •:

Show that ${\Gamma^{\prime}\vdash
H^{\prime};E[t[\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{self}}}}}}{}=x^{\prime}][y=y^{\prime}]]$
(149). This is trivially satisfied from assumption (143) with (148).

     * •:

Show ${\forall t^{\prime\prime}\in
E[t[\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{self}}}}}}{}=x^{\prime}][y=y^{\prime}]]\
\overline{T}.\Gamma^{\prime}\vdash H;t^{\prime\prime}$. The case for
$\overline{T}$ is trivially satisfied by the assumptions, (144). The case for
${E[t[\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{self}}}}}}{}=x^{\prime}][y=y^{\prime}]]$
was shown above (149).

     * •:

Show
${\textsf{Local}(H^{\prime},E[t[\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{self}}}}}}{}=x^{\prime}][y=y^{\prime}]]\
\overline{T})$ (151). This is trivially satisfied by the assumptions (145).

     * •:

Show
${\textsf{Isolated}(H^{\prime},E[t[\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{self}}}}}}{}=x^{\prime}][y=y^{\prime}]]\
\overline{T})$, (152). This is satisfied by the assumptions, (146). Lets
proceed by case analysis over the isolated assumptions and show that it
maintains isolateness.

       * –:

$\neg\textsf{isIso}(H,x)$. Thus, by the assumptions (146), this is trivially
satisfied.

       * –:

$\textsf{isIso}(H,x)\land x\mapsto\iota\in H^{\prime}$. Lets proceed by case
analysis over the incoming references being greater than 1, or not.

         * *:

${|\textsf{Inc}(H,E[t[\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{self}}}}}}{}=x^{\prime}][y=y^{\prime}]]\
\overline{T},\iota)\cup|\textsf{Inc}(H,\iota)|\leq 1$. Cannot happen, as
$x\mapsto\iota\in H$ already guarantees that the incoming references
${|\textsf{Inc}(H,E[t[\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{self}}}}}}{}=x^{\prime}][y=y^{\prime}]]\
\overline{T},\iota)|\geq 1$

         * *:

${|\textsf{Inc}(H,E[t[\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{self}}}}}}{}=x^{\prime}][y=y^{\prime}]]\
\overline{T},\iota)\cup|\textsf{Inc}(H,\iota)|\geq 1$. Proceed by case
analysis over the possible incoming references. We know that
${|\textsf{Inc}(H,E[t[\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{self}}}}}}{}=x^{\prime}][y=y^{\prime}]]\
\overline{T},\iota)|\geq 1$ since $x\mapsto\iota\in H$ and $\iota$ is isolated
and we assume (146).

           * ·:

$|\textsf{Inc}(H,\iota)|\geq 1$. Cannot happen, by assumption (146) that
violates $\textsf{Inc}(H,\iota)=\emptyset$.

           * ·:

${|\textsf{Inc}(H,E[t[\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{self}}}}}}{}=x^{\prime}][y=y^{\prime}]]\
\overline{T},\iota)|\geq 1$. We pick the thread
${E[t[\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{self}}}}}}{}=x^{\prime}][y=y^{\prime}]]$
and show that it trivially satisfies that
${{\textsf{Inc}(H,E[t[\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{self}}}}}}{}=x^{\prime}][y=y^{\prime}]]\
\overline{T},\iota)=\textsf{Inc}(H,E[t[\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{self}}}}}}{}=x^{\prime}][y=y^{\prime}]],\iota)$,
by the assumption (146), and maintains that
$\textsf{Inc}(()H^{\prime},\iota)=\emptyset$. Thus,
${\textsf{Isolated}(H^{\prime},E[t[\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{self}}}}}}{}=x^{\prime}][y=y^{\prime}]]\
\overline{T})$.

By WF-Configuration, we conclude that ${\Gamma\vdash
H;E[t[\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{self}}}}}}{}=x^{\prime}][y=y^{\prime}]]\
\overline{T}$ is well-formed.

E-NoSuchMethod:

, $H;E[x.m(v)]\rightsquigarrow H;\textmd{Err}_{N}$. This proceeds in the same
fashion as E-NoSuchField

E-AbsentTarget:

, $H;E[x.m(v)]\rightsquigarrow H;\textmd{Err}_{A}$. This proceeds in the same
fashion as E-AbsentVar

  9. (9)

${t=E[\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{spawn}}}}}}~{}(x)~{}\\{t^{\prime}\\}]$.
By the induction hypothesis,

${\displaystyle
H;E[\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{spawn}}}}}}~{}(x)~{}\\{t^{\prime}\\}]\
\overline{T}\rightsquigarrow H;\overline{T^{\prime}}\ \overline{T}$
$\displaystyle\qquad\Rightarrow\exists\Gamma^{\prime}.\Gamma^{\prime}\supseteq\Gamma\land\Gamma^{\prime}\vdash
H^{\prime};\overline{T^{\prime}}\ \overline{T}$

There is only a single reduction rule.

R-Spawn:

,
${H;E[\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{spawn}}}}}}~{}(x)~{}\\{t^{\prime}\\}]\rightsquigarrow
H;E[\iota]\ t^{\prime}$. From initial assumption and WF-Configuration:

(153) ${\displaystyle\Gamma\vdash
H;E[\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{spawn}}}}}}~{}(x)~{}\\{t^{\prime}\\}]\overline{T}$
(154) ${\displaystyle\forall t^{\prime}\in
E[\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{spawn}}}}}}~{}(x)~{}\\{t^{\prime}\\}]\
\overline{T}.\ \ \Gamma\vdash H;t^{\prime}$ (155)
${\displaystyle\textsf{Local}(H,E[\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{spawn}}}}}}~{}(x)~{}\\{t^{\prime}\\}]\
\overline{T})$ (156)
${\displaystyle\textsf{Isolated}(H,E[\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{spawn}}}}}}~{}(x)~{}\\{t^{\prime}\\}]\
\overline{T})$

Need to show:

$\exists\Gamma^{\prime}.\Gamma^{\prime}\supseteq\Gamma\land\Gamma^{\prime}\vdash
H^{\prime};\overline{T^{\prime}}\ \overline{T}$

The strategy of the proof is to show that all components are well-formed. By
rule WF-Configuration and IH, we need to show:

(157) $\displaystyle\Gamma^{\prime}\supseteq\Gamma$ (158)
$\displaystyle\Gamma^{\prime}\vdash H^{\prime}$ (159)
$\displaystyle\Gamma^{\prime}\vdash H^{\prime};E[\iota]\ t^{\prime}$ (160)
$\displaystyle\forall t^{\prime\prime}\in E[\iota]\ t^{\prime}\
\overline{T}.\Gamma^{\prime}\vdash H;t^{\prime\prime}$ (161)
$\displaystyle\textsf{Local}(H^{\prime},E[\iota]\ t^{\prime}\ \overline{T})$
(162) $\displaystyle\textsf{Isolated}(H^{\prime},E[\iota]\ t^{\prime}\
\overline{T})$

We pick
${{\Gamma^{\prime}=\Gamma,\iota:\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{local}}}}}}{},x:\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{local}}}}}}{}$,
and
${H^{\prime}=H,x^{\prime}\mapsto\iota,\iota\mapsto\,\\!\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{chan}}}}}}\,\\{i,\varnothing\\}$
and $\overline{T^{\prime}}=E[\iota]\ t^{\prime}$ by R-Spawn. We now proof each
of the components of the configuration:

     * •:

We picked
${{\Gamma^{\prime}=\Gamma,\iota:\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{local}}}}}}{},x:\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{local}}}}}}{}$,
this trivially satisfies (157).

     * •:

Show $\Gamma^{\prime}\vdash H^{\prime}$ (158). By the assumption (153), we
have $\Gamma\vdash H$. We proceed by proving that each component is well-
formed.

       1. (a):

${Gamma(x)=\Gamma(\iota)=\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{local}}}}}}{}$

       2. (b):

By WF-H-Var with (9a), we conclude that $\Gamma^{\prime}\vdash
H,x\mapsto\iota$

       3. (c):

By WF-H-Chain with (9a) and (9b), we conclude that $\Gamma^{\prime}\vdash
H^{\prime}$.

     * •:

Show that $\Gamma^{\prime}\vdash H^{\prime};E[\iota]\ t^{\prime}$ (159). This
is trivially satisfied from assumption (153) with (158), given that it is part
of the assumptions that t’ is well-formed from WF-Term-Let.

     * •:

Show $\forall t^{\prime\prime}\in E[\iota]\ t^{\prime}\
\overline{T}.\Gamma^{\prime}\vdash H;t^{\prime\prime}$. The case for
$\overline{T}$ is trivially satisfied by the assumptions, (154). The case for
$E[\iota]$ was shown above (159).

     * •:

Show $\textsf{Local}(H^{\prime},E[\iota]\ t^{\prime}\ \overline{T})$ (161).
This is vacuously satisfied by the assumption (155).

     * •:

Show $\textsf{Isolated}(H^{\prime},E[\iota]\ t^{\prime}\overline{T})$, (162).
This is satisfied by the assumption (156), since spawning a thread does not
affect the Isolated predicate.

By WF-Configuration, we conclude that $\Gamma\vdash H;E[\iota]\ t^{\prime}\
\overline{T}$ is well-formed.

  10. (10)

$t=E[\ \leftarrow\iota]$. By the induction hypothesis,

$\displaystyle H;E[\ \leftarrow\iota]\ \overline{T}\rightsquigarrow
H;\overline{T^{\prime}}\ \overline{T}$
$\displaystyle\qquad\Rightarrow\exists\Gamma^{\prime}.\Gamma^{\prime}\supseteq\Gamma\land\Gamma^{\prime}\vdash
H^{\prime};\overline{T^{\prime}}\ \overline{T}$

There are multiple rules, depending on whether the location maps to an object
E-RecvBadTarget or to a channel (R-Recv).

R-RecvBadTarget:

, $H;E[\ \leftarrow\iota]\rightsquigarrow H;\textmd{Err}_{N}$. This proof is
similar to E-AbsentVar, except that $H(\iota)$ maps to an object, instead of
to $\top$.

R-Recv:

, $H;E[\ \leftarrow\iota]\rightsquigarrow H;E[\iota^{\prime}]$. From initial
assumption and WF-Configuration:

(163) $\displaystyle\Gamma\vdash H;E[\ \leftarrow\iota]\overline{T}$ (164)
$\displaystyle\forall t^{\prime}\in E[\ \leftarrow\iota]\ \overline{T}.\ \
\Gamma\vdash H;t^{\prime}$ (165) $\displaystyle\textsf{Local}(H,E[\
\leftarrow\iota]\ \overline{T})$ (166) $\displaystyle\textsf{Isolated}(H,E[\
\leftarrow\iota]\ \overline{T})$

Need to show:

$\exists\Gamma^{\prime}.\Gamma^{\prime}\supseteq\Gamma\land\Gamma^{\prime}\vdash
H^{\prime};\overline{T^{\prime}}\ \overline{T}$

The strategy of the proof is to show that all components are well-formed. By
rule WF-Configuration and IH, we need to show:

(167) $\displaystyle\Gamma^{\prime}\supseteq\Gamma$ (168)
$\displaystyle\Gamma^{\prime}\vdash H^{\prime}$ (169)
$\displaystyle\Gamma^{\prime}\vdash H^{\prime};E[\iota^{\prime}]$ (170)
$\displaystyle\forall t^{\prime\prime}\in E[\iota^{\prime}]\
\overline{T}.\Gamma^{\prime}\vdash H;t^{\prime\prime}$ (171)
$\displaystyle\textsf{Local}(H^{\prime},E[\iota^{\prime}]\ \overline{T})$
(172) $\displaystyle\textsf{Isolated}(H^{\prime},E[\iota^{\prime}]\
\overline{T})$

We pick $\Gamma^{\prime}=\Gamma$, and
${H^{\prime}=H[\iota\mapsto\,\\!\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{chan}}}}}}\,\\{i,\varnothing\\}]$
and $\overline{T^{\prime}}=E[\iota^{\prime}]$ by R-Recv. We now proof each of
the components of the configuration:

     * •:

We picked $\Gamma^{\prime}=\Gamma$, this trivially satisfies (167).

     * •:

Show $\Gamma^{\prime}\vdash H^{\prime}$ (168). By (163), all the locations and
variables match the expected capability and are defined in $\Gamma$ and $H$.
By WF-H-Class with initial assumptions, we conclude $\Gamma^{\prime}\vdash
H^{\prime}$ is well-formed.

     * •:

Show that $\Gamma^{\prime}\vdash H^{\prime};E[\iota^{\prime}]$ (169). By WF-
Term-Let with (163) and (168) where $\iota^{\prime}\in\textit{dom}(H)$, we
conclude $\Gamma^{\prime}\vdash H^{\prime};E[\iota^{\prime}]$.

     * •:

Show $\forall t^{\prime\prime}\in E[\iota^{\prime}]\
\overline{T}.\Gamma^{\prime}\vdash H;t^{\prime\prime}$. The case for
$\overline{T}$ is trivially satisfied from (164). The case for $E[\iota]$ was
shown above (169).

     * •:

Show $\textsf{Local}(H^{\prime},E[\iota^{\prime}]\ \overline{T})$ (171). This
is trivially satisfied from (165). Explanation: Before the reduction step, by
definition of ROG, locations leading to channels are not considered part of a
ROG. Thus, $\iota^{\prime}$ was unreachable by any thread. By initial
assumption of well-formedness $\Gamma\vdash H$ and
${\Gamma(\iota^{\prime})\neq\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{local}}}}}}{}$.
Thus, $\iota^{\prime}$ is in a single thread, and we can conclude that it
satisfies $\textsf{Local}(H^{\prime},E[\iota^{\prime}]\ \overline{T})$.

     * •:

Show $\textsf{Isolated}(H^{\prime},E[\iota^{\prime}]\ \overline{T})$, (172).
This is satisfied from initial assumption (166). Explanation: From initial
assumption and the helper function Isolated, if $\iota^{\prime}$ is an
isolate, then it can only be in a channel. By taking a step and removing
$\iota^{\prime}$ from the channel, we place it in the stack and the incoming
number of references is 1, so it vacuously satisfies
$\textsf{Isolated}(H^{\prime},E[\iota^{\prime}]\ \overline{T})$.

By WF-Configuration, we conclude that $\Gamma\vdash H;E[\iota^{\prime}]\
\overline{T}$ is well-formed.

  11. (11)

$t=E[\iota\leftarrow v]$. By the induction hypothesis,

$\displaystyle H;E[\iota\leftarrow v]\ \overline{T}\rightsquigarrow
H;\overline{T^{\prime}}\ \overline{T}$
$\displaystyle\qquad\Rightarrow\exists\Gamma^{\prime}.\Gamma^{\prime}\supseteq\Gamma\land\Gamma^{\prime}\vdash
H^{\prime};\overline{T^{\prime}}\ \overline{T}$

There are multiple rules, depending on whether the element to send contains
local elements (E-SendingLocal), whether $\iota$ is a channel or not
(R-SendBlock and E-SendBadTargetOrArgument) and whether $v=\iota^{\prime}$ and
maps to a channel (E-SendBadTargetOrArgument)).

R-SendBlock:

, $H;E[\iota\leftarrow v]\rightsquigarrow H;E[\blacksquare_{i}\,\iota]$. From
initial assumption and WF-Configuration:

(173) $\displaystyle\Gamma\vdash H;E[\iota\leftarrow v]\overline{T}$ (174)
$\displaystyle\forall t^{\prime}\in E[\iota\leftarrow v]\ \overline{T}.\ \
\Gamma\vdash H;t^{\prime}$ (175)
$\displaystyle\textsf{Local}(H,E[\iota\leftarrow v]\ \overline{T})$ (176)
$\displaystyle\textsf{Isolated}(H,E[\iota\leftarrow v]\ \overline{T})$

Need to show:

$\exists\Gamma^{\prime}.\Gamma^{\prime}\supseteq\Gamma\land\Gamma^{\prime}\vdash
H^{\prime};\overline{T^{\prime}}\ \overline{T}$

The strategy of the proof is to show that all components are well-formed. By
rule WF-Configuration and IH, we need to show:

(177) $\displaystyle\Gamma^{\prime}\supseteq\Gamma$ (178)
$\displaystyle\Gamma^{\prime}\vdash H^{\prime}$ (179)
$\displaystyle\Gamma^{\prime}\vdash H^{\prime};E[\iota]$ (180)
$\displaystyle\forall t^{\prime\prime}\in E[\iota]\
\overline{T}.\Gamma^{\prime}\vdash H;t^{\prime\prime}$ (181)
$\displaystyle\textsf{Local}(H^{\prime},E[\iota]\ \overline{T})$ (182)
$\displaystyle\textsf{Isolated}(H^{\prime},E[\iota]\ \overline{T})$

We pick $\Gamma^{\prime}=\Gamma$, and
${H^{\prime}=H[\iota\mapsto\,\\!\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor{\@listingGroup{ltx_lst_identifier}{chan}}}}}}\,\\{i,v\\}]$
and $\overline{T^{\prime}}=E[\iota]$ by R-SendBlock. We now proof each of the
components of the configuration:

     * •:

We picked $\Gamma^{\prime}=\Gamma$, this trivially satisfies (177).

     * •:

Show $\Gamma^{\prime}\vdash H^{\prime}$ (178). From (173), all the locations
and variables match the expected capability and are defined in $\Gamma$ and
$H$. By WF-H-Chan with the initial assumptions, we conclude
$\Gamma^{\prime}\vdash H^{\prime}$ is well-formed.

     * •:

Show that $\Gamma^{\prime}\vdash H^{\prime};E[\iota]$ (179). By WF-Term-Let
with (173) and (178) where $\iota\in\textit{dom}(H)$, we conclude
$\Gamma^{\prime}\vdash H^{\prime};E[\iota]$.

     * •:

Show $\forall t^{\prime\prime}\in E[\iota]\ \overline{T}.\Gamma^{\prime}\vdash
H;t^{\prime\prime}$. The case for $\overline{T}$ is trivially satisfied from
(174). The case for $E[\iota]$ was shown above (179).

     * •:

Show $\textsf{Local}(H^{\prime},E[\iota]\ \overline{T})$ (181). This is
trivially satisfied from (175).

     * •:

Show $\textsf{Isolated}(H^{\prime},E[\iota]\ \overline{T})$, (182). This is
satisfied from initial assumption (176). Explanation: From initial assumption
and the helper function Isolated, if $v$ is an isolate, then it can only be in
the stack and is unique. By taking a step and removing $v$ from the stack, we
place it in channel. The number of stack incoming references for $v$ is 0, and
the number of heap incoming references is 1. Thus, the configuration vacuously
satisfies $\textsf{Isolated}(H^{\prime},E[\iota]\ \overline{T})$, as the
antecedent of the implication is false.

By WF-Configuration, we conclude that $\Gamma\vdash H;E[\iota]\ \overline{T}$
is well-formed.

E-SendBadTargetOrArgument:

, $H;E[\iota\leftarrow\iota^{\prime}]\rightsquigarrow H;\textmd{Err}_{N}$.