\newblock \showarticletitle{Order types: static reasoning about message races in asynchronous message passing concurrency}. In \bibinfo{booktitle}{\emph{AGERE!@SPLASH}}. \bibinfo{publisher}{{ACM}}, \bibinfo{pages}{21--30}.
\newblock

\bibitem[Bollig et~al\mbox{.}(2013)]%
\bibfield{author}{\bibinfo{person}{Benedikt Bollig}, \bibinfo{person}{Peter Habermehl}, \bibinfo{person}{Martin Leucker}, {and} \bibinfo{person}{Benjamin Monmege}.} \bibinfo{year}{2013}\natexlab{}.
\newblock \showarticletitle{{A} {F}resh {A}pproach to {L}earning {R}egister {A}utomata}. In \bibinfo{booktitle}{\emph{Developments in Language Theory}} \emph{(\bibinfo{series}{{LNCS}}, Vol.~\bibinfo{volume}{7907})}. \bibinfo{publisher}{Springer}, \bibinfo{pages}{118--130}.
\newblock

\bibitem[Brzozowski(1964)]%
\bibfield{author}{\bibinfo{person}{Janusz~A Brzozowski}.} \bibinfo{year}{1964}\natexlab{}.
\newblock \showarticletitle{Derivatives of regular expressions}.
\newblock \bibinfo{journal}{\emph{Journal of the ACM (JACM)}} \bibinfo{volume}{11}, \bibinfo{number}{4} (\bibinfo{year}{1964}), \bibinfo{pages}{481--494}.
\newblock

\bibitem[Chaudhuri(2009)]%
\bibfield{author}{\bibinfo{person}{Avik Chaudhuri}.} \bibinfo{year}{2009}\natexlab{}.
\newblock \showarticletitle{A {C}oncurrent {ML} library in {C}oncurrent {H}askell}. In \bibinfo{booktitle}{\emph{{ICFP}}}. \bibinfo{publisher}{{ACM}}, \bibinfo{pages}{269--280}.
\newblock

\bibitem[Christakis and Sagonas(2011)]%
\bibfield{author}{\bibinfo{person}{Maria Christakis} {and} \bibinfo{person}{Konstantinos Sagonas}.} \bibinfo{year}{2011}\natexlab{}.
\newblock \showarticletitle{Detection of Asynchronous Message Passing Errors Using Static Analysis}. In \bibinfo{booktitle}{\emph{{PADL}}} \emph{(\bibinfo{series}{Lecture Notes in Computer Science}, Vol.~\bibinfo{volume}{6539})}. \bibinfo{publisher}{Springer}, \bibinfo{pages}{5--18}.
\newblock

\bibitem[Ciccone and Padovani(2022)]%
\bibfield{author}{\bibinfo{person}{Luca Ciccone} {and} \bibinfo{person}{Luca Padovani}.} \bibinfo{year}{2022}\natexlab{}.
\newblock \showarticletitle{Fair termination of binary sessions}.
\newblock \bibinfo{journal}{\emph{Proc. {ACM} Program. Lang.}} \bibinfo{volume}{6}, \bibinfo{number}{{POPL}} (\bibinfo{year}{2022}), \bibinfo{pages}{1--30}.
\newblock

\bibitem[Crafa and Padovani(2017)]%
\bibfield{author}{\bibinfo{person}{Silvia Crafa} {and} \bibinfo{person}{Luca Padovani}.} \bibinfo{year}{2017}\natexlab{}.
\newblock \showarticletitle{The Chemical Approach to Typestate-Oriented Programming}.
\newblock \bibinfo{journal}{\emph{{ACM} Trans. Program. Lang. Syst.}} \bibinfo{volume}{39}, \bibinfo{number}{3} (\bibinfo{year}{2017}), \bibinfo{pages}{13:1--13:45}.
\newblock

\bibitem[de~Boer et~al\mbox{.}(2007)]%
\bibfield{author}{\bibinfo{person}{Frank~S. de Boer}, \bibinfo{person}{Dave Clarke}, {and} \bibinfo{person}{Einar~Broch Johnsen}.} \bibinfo{year}{2007}\natexlab{}.
\newblock \showarticletitle{A Complete Guide to the Future}. In \bibinfo{booktitle}{\emph{{ESOP}}} \emph{(\bibinfo{series}{Lecture Notes in Computer Science}, Vol.~\bibinfo{volume}{4421})}. \bibinfo{publisher}{Springer}, \bibinfo{pages}{316--330}.
\newblock

\bibitem[de~Moura and Bj{\o}rner(2008)]%
\bibfield{author}{\bibinfo{person}{Leonardo~Mendon{\c{c}}a de Moura} {and} \bibinfo{person}{Nikolaj~S. Bj{\o}rner}.} \bibinfo{year}{2008}\natexlab{}.
\newblock \showarticletitle{{Z3:} An Efficient {SMT} Solver}. In \bibinfo{booktitle}{\emph{{TACAS}}} \emph{(\bibinfo{series}{Lecture Notes in Computer Science}, Vol.~\bibinfo{volume}{4963})}. \bibinfo{publisher}{Springer}, \bibinfo{pages}{337--340}.
\newblock

\bibitem[de'Liguoro and Padovani(2018)]%
\bibfield{author}{\bibinfo{person}{Ugo de'Liguoro} {and} \bibinfo{person}{Luca Padovani}.} \bibinfo{year}{2018}\natexlab{}.
\newblock \showarticletitle{Mailbox Types for Unordered Interactions}. In \bibinfo{booktitle}{\emph{{ECOOP}}} \emph{(\bibinfo{series}{LIPIcs}, Vol.~\bibinfo{volume}{109})}. \bibinfo{publisher}{Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik}, \bibinfo{pages}{15:1--15:28}.
\newblock

\bibitem[Devore and Berk(2012)]%
\bibfield{author}{\bibinfo{person}{Jay~L. Devore} {and} \bibinfo{person}{Kenneth~N. Berk}.} \bibinfo{year}{2012}\natexlab{}.
\newblock \bibinfo{booktitle}{\emph{Modern Mathematical Statistics with Applications}}.
\newblock \bibinfo{publisher}{Springer}.
\newblock

\bibitem[Dunfield and Krishnaswami(2022)]%
\bibfield{author}{\bibinfo{person}{Jana Dunfield} {and} \bibinfo{person}{Neel Krishnaswami}.} \bibinfo{year}{2022}\natexlab{}.
\newblock \showarticletitle{Bidirectional Typing}.
\newblock \bibinfo{journal}{\emph{{ACM} Comput. Surv.}} \bibinfo{volume}{54}, \bibinfo{number}{5} (\bibinfo{year}{2022}), \bibinfo{pages}{98:1--98:38}.
\newblock

\bibitem[Ennals et~al\mbox{.}(2004)]%
\bibfield{author}{\bibinfo{person}{Robert Ennals}, \bibinfo{person}{Richard Sharp}, {and} \bibinfo{person}{Alan Mycroft}.} \bibinfo{year}{2004}\natexlab{}.
\newblock \showarticletitle{Linear Types for Packet Processing}. In \bibinfo{booktitle}{\emph{Programming Languages and Systems, 13th European Symposium on Programming, {ESOP} 2004, Held as Part of the Joint European Conferences on Theory and Practice of Software, {ETAPS} 2004, Barcelona, Spain, March 29 - April 2, 2004, Proceedings}} \emph{(\bibinfo{series}{Lecture Notes in Computer Science}, Vol.~\bibinfo{volume}{2986})}, \bibfield{editor}{\bibinfo{person}{David~A. Schmidt}} (Ed.). \bibinfo{publisher}{Springer}, \bibinfo{pages}{204--218}.
\newblock
\urldef\tempurl%
\url{https://doi.org/10.1007/978-3-540-24725-8\_15}
\showDOI{\tempurl}

\bibitem[Erdweg et~al\mbox{.}(2015)]%
\bibfield{author}{\bibinfo{person}{Sebastian Erdweg}, \bibinfo{person}{Oliver Bracevac}, \bibinfo{person}{Edlira Kuci}, \bibinfo{person}{Matthias Krebs}, {and} \bibinfo{person}{Mira Mezini}.} \bibinfo{year}{2015}\natexlab{}.
\newblock \showarticletitle{A co-contextual formulation of type rules and its application to incremental type checking}. In \bibinfo{booktitle}{\emph{{OOPSLA}}}. \bibinfo{publisher}{{ACM}}, \bibinfo{pages}{880--897}.
\newblock

\bibitem[Fournet and Gonthier(1996)]%
\bibfield{author}{\bibinfo{person}{C{\'{e}}dric Fournet} {and} \bibinfo{person}{Georges Gonthier}.} \bibinfo{year}{1996}\natexlab{}.
\newblock \showarticletitle{The Reflexive {CHAM} and the Join-Calculus}. In \bibinfo{booktitle}{\emph{{POPL}}}. \bibinfo{publisher}{{ACM} Press}, \bibinfo{pages}{372--385}.
\newblock

\bibitem[Fowler(2016)]%
\bibfield{author}{\bibinfo{person}{Simon Fowler}.} \bibinfo{year}{2016}\natexlab{}.
\newblock \showarticletitle{An {E}rlang Implementation of Multiparty Session Actors}. In \bibinfo{booktitle}{\emph{{ICE}}} \emph{(\bibinfo{series}{{EPTCS}}, Vol.~\bibinfo{volume}{223})}. \bibinfo{pages}{36--50}.
\newblock

\bibitem[Fowler et~al\mbox{.}(2021)]%
\bibfield{author}{\bibinfo{person}{Simon Fowler}, \bibinfo{person}{Wen Kokke}, \bibinfo{person}{Ornela Dardha}, \bibinfo{person}{Sam Lindley}, {and} \bibinfo{person}{J.~Garrett Morris}.} \bibinfo{year}{2021}\natexlab{}.
\newblock \showarticletitle{Separating Sessions Smoothly}. In \bibinfo{booktitle}{\emph{{CONCUR}}} \emph{(\bibinfo{series}{LIPIcs}, Vol.~\bibinfo{volume}{203})}. \bibinfo{publisher}{Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik}, \bibinfo{pages}{36:1--36:18}.
\newblock

\bibitem[Fowler et~al\mbox{.}(2017)]%
\bibfield{author}{\bibinfo{person}{Simon Fowler}, \bibinfo{person}{Sam Lindley}, {and} \bibinfo{person}{Philip Wadler}.} \bibinfo{year}{2017}\natexlab{}.
\newblock \showarticletitle{Mixing Metaphors: Actors as Channels and Channels as Actors}. In \bibinfo{booktitle}{\emph{{ECOOP}}} \emph{(\bibinfo{series}{LIPIcs}, Vol.~\bibinfo{volume}{74})}. \bibinfo{publisher}{Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik}, \bibinfo{pages}{11:1--11:28}.
\newblock

\bibitem[Gay and Vasconcelos(2010)]%
\bibfield{author}{\bibinfo{person}{Simon~J. Gay} {and} \bibinfo{person}{Vasco~Thudichum Vasconcelos}.} \bibinfo{year}{2010}\natexlab{}.
\newblock \showarticletitle{Linear type theory for asynchronous session types}.
\newblock \bibinfo{journal}{\emph{J. Funct. Program.}} \bibinfo{volume}{20}, \bibinfo{number}{1} (\bibinfo{year}{2010}), \bibinfo{pages}{19--50}.
\newblock

\bibitem[Gerbo and Padovani(2019)]%
\bibfield{author}{\bibinfo{person}{Rosita Gerbo} {and} \bibinfo{person}{Luca Padovani}.} \bibinfo{year}{2019}\natexlab{}.
\newblock \showarticletitle{Concurrent Typestate-Oriented Programming in Java}. In \bibinfo{booktitle}{\emph{PLACES@ETAPS}} \emph{(\bibinfo{series}{{EPTCS}}, Vol.~\bibinfo{volume}{291})}. \bibinfo{pages}{24--34}.
\newblock

\bibitem[Ginsburg and Spanier(1966)]%
\bibfield{author}{\bibinfo{person}{Seymour Ginsburg} {and} \bibinfo{person}{Edwin Spanier}.} \bibinfo{year}{1966}\natexlab{}.
\newblock \showarticletitle{Semigroups, Presburger formulas, and languages}.
\newblock \bibinfo{journal}{\emph{Pacific journal of Mathematics}} \bibinfo{volume}{16}, \bibinfo{number}{2} (\bibinfo{year}{1966}), \bibinfo{pages}{285--296}.
\newblock

\bibitem[Harrison(2018)]%
\bibfield{author}{\bibinfo{person}{Joseph~R. Harrison}.} \bibinfo{year}{2018}\natexlab{}.
\newblock \showarticletitle{Automatic detection of core Erlang message passing errors}. In \bibinfo{booktitle}{\emph{Erlang Workshop}}. \bibinfo{publisher}{{ACM}}, \bibinfo{pages}{37--48}.
\newblock

\bibitem[Harvey et~al\mbox{.}(2021)]%
\bibfield{author}{\bibinfo{person}{Paul Harvey}, \bibinfo{person}{Simon Fowler}, \bibinfo{person}{Ornela Dardha}, {and} \bibinfo{person}{Simon~J. Gay}.} \bibinfo{year}{2021}\natexlab{}.
\newblock \showarticletitle{Multiparty Session Types for Safe Runtime Adaptation in an Actor Language}. In \bibinfo{booktitle}{\emph{{ECOOP}}} \emph{(\bibinfo{series}{LIPIcs}, Vol.~\bibinfo{volume}{194})}. \bibinfo{publisher}{Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik}, \bibinfo{pages}{10:1--10:30}.
\newblock

\bibitem[He et~al\mbox{.}(2014)]%
\bibfield{author}{\bibinfo{person}{Jiansen He}, \bibinfo{person}{Philip Wadler}, {and} \bibinfo{person}{Philip~W. Trinder}.} \bibinfo{year}{2014}\natexlab{}.
\newblock \showarticletitle{Typecasting actors: from Akka to TAkka}. In \bibinfo{booktitle}{\emph{SCALA@ECOOP}}. \bibinfo{publisher}{{ACM}}, \bibinfo{pages}{23--33}.
\newblock

\bibitem[Honda(1993)]%
\bibfield{author}{\bibinfo{person}{Kohei Honda}.} \bibinfo{year}{1993}\natexlab{}.
\newblock \showarticletitle{Types for Dyadic Interaction}. In \bibinfo{booktitle}{\emph{{CONCUR} '93, 4th International Conference on Concurrency Theory, Hildesheim, Germany, August 23-26, 1993, Proceedings}} \emph{(\bibinfo{series}{Lecture Notes in Computer Science}, Vol.~\bibinfo{volume}{715})}, \bibfield{editor}{\bibinfo{person}{Eike Best}} (Ed.). \bibinfo{publisher}{Springer}, \bibinfo{pages}{509--523}.
\newblock
\urldef\tempurl%
\url{https://doi.org/10.1007/3-540-57208-2\_35}
\showDOI{\tempurl}

\bibitem[Honda et~al\mbox{.}(1998)]%
\bibfield{author}{\bibinfo{person}{Kohei Honda}, \bibinfo{person}{Vasco~Thudichum Vasconcelos}, {and} \bibinfo{person}{Makoto Kubo}.} \bibinfo{year}{1998}\natexlab{}.
\newblock \showarticletitle{Language Primitives and Type Discipline for Structured Communication-Based Programming}. In \bibinfo{booktitle}{\emph{{ESOP}}} \emph{(\bibinfo{series}{Lecture Notes in Computer Science}, Vol.~\bibinfo{volume}{1381})}. \bibinfo{publisher}{Springer}, \bibinfo{pages}{122--138}.
\newblock

\bibitem[Honda et~al\mbox{.}(2016)]%
\bibfield{author}{\bibinfo{person}{Kohei Honda}, \bibinfo{person}{Nobuko Yoshida}, {and} \bibinfo{person}{Marco Carbone}.} \bibinfo{year}{2016}\natexlab{}.
\newblock \showarticletitle{Multiparty Asynchronous Session Types}.
\newblock \bibinfo{journal}{\emph{J. {ACM}}} \bibinfo{volume}{63}, \bibinfo{number}{1} (\bibinfo{year}{2016}), \bibinfo{pages}{9:1--9:67}.
\newblock

\bibitem[Hopkins and Kozen(1999)]%
\bibfield{author}{\bibinfo{person}{Mark~W. Hopkins} {and} \bibinfo{person}{Dexter Kozen}.} \bibinfo{year}{1999}\natexlab{}.
\newblock \showarticletitle{Parikh's Theorem in Commutative Kleene Algebra}. In \bibinfo{booktitle}{\emph{{LICS}}}. \bibinfo{publisher}{{IEEE} Computer Society}, \bibinfo{pages}{394--401}.
\newblock

\bibitem[Hu and Yoshida(2017)]%
\bibfield{author}{\bibinfo{person}{Raymond Hu} {and} \bibinfo{person}{Nobuko Yoshida}.} \bibinfo{year}{2017}\natexlab{}.
\newblock \showarticletitle{Explicit Connection Actions in Multiparty Session Types}. In \bibinfo{booktitle}{\emph{{FASE}}} \emph{(\bibinfo{series}{Lecture Notes in Computer Science}, Vol.~\bibinfo{volume}{10202})}. \bibinfo{publisher}{Springer}, \bibinfo{pages}{116--133}.
\newblock

\bibitem[Hu et~al\mbox{.}(2008)]%
\bibfield{author}{\bibinfo{person}{Raymond Hu}, \bibinfo{person}{Nobuko Yoshida}, {and} \bibinfo{person}{Kohei Honda}.} \bibinfo{year}{2008}\natexlab{}.
\newblock \showarticletitle{Session-Based Distributed Programming in Java}. In \bibinfo{booktitle}{\emph{{ECOOP}}} \emph{(\bibinfo{series}{Lecture Notes in Computer Science}, Vol.~\bibinfo{volume}{5142})}. \bibinfo{publisher}{Springer}, \bibinfo{pages}{516--541}.
\newblock

\bibitem[H{\"{u}}ttel et~al\mbox{.}(2016)]%
\bibfield{author}{\bibinfo{person}{Hans H{\"{u}}ttel}, \bibinfo{person}{Ivan Lanese}, \bibinfo{person}{Vasco~T. Vasconcelos}, \bibinfo{person}{Lu{\'{\i}}s Caires}, \bibinfo{person}{Marco Carbone}, \bibinfo{person}{Pierre{-}Malo Deni{\'{e}}lou}, \bibinfo{person}{Dimitris Mostrous}, \bibinfo{person}{Luca Padovani}, \bibinfo{person}{Ant{\'{o}}nio Ravara}, \bibinfo{person}{Emilio Tuosto}, \bibinfo{person}{Hugo~Torres Vieira}, {and} \bibinfo{person}{Gianluigi Zavattaro}.} \bibinfo{year}{2016}\natexlab{}.
\newblock \showarticletitle{Foundations of Session Types and Behavioural Contracts}.
\newblock \bibinfo{journal}{\emph{{ACM} Comput. Surv.}} \bibinfo{volume}{49}, \bibinfo{number}{1} (\bibinfo{year}{2016}), \bibinfo{pages}{3:1--3:36}.
\newblock
\urldef\tempurl%
\url{https://doi.org/10.1145/2873052}
\showDOI{\tempurl}

\bibitem[Imam and Sarkar(2014)]%
\bibfield{author}{\bibinfo{person}{Shams~Mahmood Imam} {and} \bibinfo{person}{Vivek Sarkar}.} \bibinfo{year}{2014}\natexlab{}.
\newblock \showarticletitle{Savina - An Actor Benchmark Suite: Enabling Empirical Evaluation of Actor Libraries}. In \bibinfo{booktitle}{\emph{AGERE!@SPLASH}}. \bibinfo{publisher}{{ACM}}, \bibinfo{pages}{67--80}.
\newblock

\bibitem[Juri\'{c}(2019)]%
\bibfield{author}{\bibinfo{person}{Sa\v{s}a Juri\'{c}}.} \bibinfo{year}{2019}\natexlab{}.
\newblock \bibinfo{booktitle}{\emph{Elixir in Action}}.
\newblock \bibinfo{publisher}{Manning}.
\newblock

\bibitem[Kamburjan et~al\mbox{.}(2016)]%
\bibfield{author}{\bibinfo{person}{Eduard Kamburjan}, \bibinfo{person}{Crystal~Chang Din}, {and} \bibinfo{person}{Tzu{-}Chun Chen}.} \bibinfo{year}{2016}\natexlab{}.
\newblock \showarticletitle{Session-Based Compositional Analysis for Actor-Based Languages Using Futures}. In \bibinfo{booktitle}{\emph{{ICFEM}}} \emph{(\bibinfo{series}{Lecture Notes in Computer Science}, Vol.~\bibinfo{volume}{10009})}. \bibinfo{pages}{296--312}.
\newblock

\bibitem[Kobayashi(1999)]%
\bibfield{author}{\bibinfo{person}{Naoki Kobayashi}.} \bibinfo{year}{1999}\natexlab{}.
\newblock \showarticletitle{Quasi-Linear Types}. In \bibinfo{booktitle}{\emph{{POPL}}}. \bibinfo{publisher}{{ACM}}, \bibinfo{pages}{29--42}.
\newblock

\bibitem[Kuci et~al\mbox{.}(2017)]%
\bibfield{author}{\bibinfo{person}{Edlira Kuci}, \bibinfo{person}{Sebastian Erdweg}, \bibinfo{person}{Oliver Bracevac}, \bibinfo{person}{Andi Bejleri}, {and} \bibinfo{person}{Mira Mezini}.} \bibinfo{year}{2017}\natexlab{}.
\newblock \showarticletitle{A Co-contextual Type Checker for Featherweight Java}. In \bibinfo{booktitle}{\emph{{ECOOP}}} \emph{(\bibinfo{series}{LIPIcs}, Vol.~\bibinfo{volume}{74})}. \bibinfo{publisher}{Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik}, \bibinfo{pages}{18:1--18:26}.
\newblock

\bibitem[Levy et~al\mbox{.}(2003)]%
\bibfield{author}{\bibinfo{person}{Paul~Blain Levy}, \bibinfo{person}{John Power}, {and} \bibinfo{person}{Hayo Thielecke}.} \bibinfo{year}{2003}\natexlab{}.
\newblock \showarticletitle{Modelling environments in call-by-value programming languages}.
\newblock \bibinfo{journal}{\emph{Information and Computation}} \bibinfo{volume}{185}, \bibinfo{number}{2} (\bibinfo{year}{2003}), \bibinfo{pages}{182--210}.
\newblock

\bibitem[Lindley and Morris(2015)]%
\bibfield{author}{\bibinfo{person}{Sam Lindley} {and} \bibinfo{person}{J.~Garrett Morris}.} \bibinfo{year}{2015}\natexlab{}.
\newblock \showarticletitle{A Semantics for Propositions as Sessions}. In \bibinfo{booktitle}{\emph{{ESOP}}} \emph{(\bibinfo{series}{Lecture Notes in Computer Science}, Vol.~\bibinfo{volume}{9032})}. \bibinfo{publisher}{Springer}, \bibinfo{pages}{560--584}.
\newblock

\bibitem[McBride(2018)]%
\bibfield{author}{\bibinfo{person}{Conor McBride}.} \bibinfo{year}{2018}\natexlab{}.
\newblock \showarticletitle{Everybody's Got To Be Somewhere}. In \bibinfo{booktitle}{\emph{MSFP@FSCD}} \emph{(\bibinfo{series}{{EPTCS}}, Vol.~\bibinfo{volume}{275})}. \bibinfo{pages}{53--69}.
\newblock

\bibitem[Mostrous and Vasconcelos(2011)]%
\bibfield{author}{\bibinfo{person}{Dimitris Mostrous} {and} \bibinfo{person}{Vasco~Thudichum Vasconcelos}.} \bibinfo{year}{2011}\natexlab{}.
\newblock \showarticletitle{Session Typing for a Featherweight Erlang}. In \bibinfo{booktitle}{\emph{{COORDINATION}}} \emph{(\bibinfo{series}{Lecture Notes in Computer Science}, Vol.~\bibinfo{volume}{6721})}. \bibinfo{publisher}{Springer}, \bibinfo{pages}{95--109}.
\newblock

\bibitem[Neykova and Yoshida(2017a)]%
\bibfield{author}{\bibinfo{person}{Rumyana Neykova} {and} \bibinfo{person}{Nobuko Yoshida}.} \bibinfo{year}{2017}\natexlab{a}.
\newblock \showarticletitle{Let it recover: multiparty protocol-induced recovery}. In \bibinfo{booktitle}{\emph{{CC}}}. \bibinfo{publisher}{{ACM}}, \bibinfo{pages}{98--108}.
\newblock

\bibitem[Neykova and Yoshida(2017b)]%
\bibfield{author}{\bibinfo{person}{Rumyana Neykova} {and} \bibinfo{person}{Nobuko Yoshida}.} \bibinfo{year}{2017}\natexlab{b}.
\newblock \showarticletitle{Multiparty Session Actors}.
\newblock \bibinfo{journal}{\emph{Log. Methods Comput. Sci.}} \bibinfo{volume}{13}, \bibinfo{number}{1} (\bibinfo{year}{2017}).
\newblock

\bibitem[Osvald et~al\mbox{.}(2016)]%
\bibfield{author}{\bibinfo{person}{Leo Osvald}, \bibinfo{person}{Gr{\'{e}}gory~M. Essertel}, \bibinfo{person}{Xilun Wu}, \bibinfo{person}{Lilliam I.~Gonz{\'{a}}lez Alay{\'{o}}n}, {and} \bibinfo{person}{Tiark Rompf}.} \bibinfo{year}{2016}\natexlab{}.
\newblock \showarticletitle{Gentrification gone too far? affordable 2nd-class values for fun and (co-)effect}. In \bibinfo{booktitle}{\emph{{OOPSLA}}}. \bibinfo{publisher}{{ACM}}, \bibinfo{pages}{234--251}.
\newblock

\bibitem[Padovani(2014)]%
\bibfield{author}{\bibinfo{person}{Luca Padovani}.} \bibinfo{year}{2014}\natexlab{}.
\newblock \showarticletitle{Type Reconstruction for the Linear {\(\pi\)}-Calculus with Composite and Equi-Recursive Types}. In \bibinfo{booktitle}{\emph{FoSSaCS}} \emph{(\bibinfo{series}{Lecture Notes in Computer Science}, Vol.~\bibinfo{volume}{8412})}. \bibinfo{publisher}{Springer}, \bibinfo{pages}{88--102}.
\newblock

\bibitem[Padovani(2018a)]%
\bibfield{author}{\bibinfo{person}{Luca Padovani}.} \bibinfo{year}{2018}\natexlab{a}.
\newblock \showarticletitle{Deadlock-Free Typestate-Oriented Programming}.
\newblock \bibinfo{journal}{\emph{Art Sci. Eng. Program.}} \bibinfo{volume}{2}, \bibinfo{number}{3} (\bibinfo{year}{2018}), \bibinfo{pages}{15}.
\newblock

\bibitem[Padovani(2018b)]%
\bibfield{author}{\bibinfo{person}{Luca Padovani}.} \bibinfo{year}{2018}\natexlab{b}.
\newblock \bibinfo{booktitle}{\emph{Mailbox Calculus Checker}}.
\newblock
\urldef\tempurl%
\url{https://boystrange.github.io/mcc/}
\showURL{%
\tempurl}

\bibitem[Padovani(2018c)]%
\bibfield{author}{\bibinfo{person}{Luca Padovani}.} \bibinfo{year}{2018}\natexlab{c}.
\newblock \showarticletitle{A type checking algorithm for concurrent object protocols}.
\newblock \bibinfo{journal}{\emph{Journal of Logical and Algebraic Methods in Programming}}  \bibinfo{volume}{100} (\bibinfo{year}{2018}), \bibinfo{pages}{16--35}.
\newblock
\showISSN{2352-2208}
\urldef\tempurl%
\url{https://doi.org/10.1016/j.jlamp.2018.06.001}
\showDOI{\tempurl}

\bibitem[Padovani(2019)]%
\bibfield{author}{\bibinfo{person}{Luca Padovani}.} \bibinfo{year}{2019}\natexlab{}.
\newblock \showarticletitle{Context-Free Session Type Inference}.
\newblock \bibinfo{journal}{\emph{{ACM} Trans. Program. Lang. Syst.}} \bibinfo{volume}{41}, \bibinfo{number}{2} (\bibinfo{year}{2019}), \bibinfo{pages}{9:1--9:37}.
\newblock

\bibitem[Parikh(1966)]%
\bibfield{author}{\bibinfo{person}{Rohit Parikh}.} \bibinfo{year}{1966}\natexlab{}.
\newblock \showarticletitle{On Context-Free Languages}.
\newblock \bibinfo{journal}{\emph{J. {ACM}}} \bibinfo{volume}{13}, \bibinfo{number}{4} (\bibinfo{year}{1966}), \bibinfo{pages}{570--581}.
\newblock

\bibitem[Pierce and Turner(2000)]%
\bibfield{author}{\bibinfo{person}{Benjamin~C. Pierce} {and} \bibinfo{person}{David~N. Turner}.} \bibinfo{year}{2000}\natexlab{}.
\newblock \showarticletitle{Local type inference}.
\newblock \bibinfo{journal}{\emph{{ACM} Trans. Program. Lang. Syst.}} \bibinfo{volume}{22}, \bibinfo{number}{1} (\bibinfo{year}{2000}), \bibinfo{pages}{1--44}.
\newblock

\bibitem[Pitts(1998)]%
\bibfield{author}{\bibinfo{person}{Andrew~M. Pitts}.} \bibinfo{year}{1998}\natexlab{}.
\newblock \showarticletitle{Existential Types: Logical Relations and Operational Equivalence}. In \bibinfo{booktitle}{\emph{{ICALP}}} \emph{(\bibinfo{series}{Lecture Notes in Computer Science}, Vol.~\bibinfo{volume}{1443})}. \bibinfo{publisher}{Springer}, \bibinfo{pages}{309--326}.
\newblock

\bibitem[Rouvoet et~al\mbox{.}(2021)]%
\bibfield{author}{\bibinfo{person}{Arjen Rouvoet}, \bibinfo{person}{Robbert Krebbers}, {and} \bibinfo{person}{Eelco Visser}.} \bibinfo{year}{2021}\natexlab{}.
\newblock \showarticletitle{Intrinsically typed compilation with nameless labels}.
\newblock \bibinfo{journal}{\emph{Proc. {ACM} Program. Lang.}} \bibinfo{volume}{5}, \bibinfo{number}{{POPL}} (\bibinfo{year}{2021}), \bibinfo{pages}{1--28}.
\newblock

\bibitem[Scalas et~al\mbox{.}(2019)]%
\bibfield{author}{\bibinfo{person}{Alceste Scalas}, \bibinfo{person}{Nobuko Yoshida}, {and} \bibinfo{person}{Elias Benussi}.} \bibinfo{year}{2019}\natexlab{}.
\newblock \showarticletitle{Verifying message-passing programs with dependent behavioural types}. In \bibinfo{booktitle}{\emph{{PLDI}}}. \bibinfo{publisher}{{ACM}}, \bibinfo{pages}{502--516}.
\newblock

\bibitem[Tabone and Francalanza(2021)]%
\bibfield{author}{\bibinfo{person}{Gerard Tabone} {and} \bibinfo{person}{Adrian Francalanza}.} \bibinfo{year}{2021}\natexlab{}.
\newblock \showarticletitle{Session types in Elixir}. In \bibinfo{booktitle}{\emph{AGERE!@SPLASH}}. \bibinfo{publisher}{{ACM}}, \bibinfo{pages}{12--23}.
\newblock

\bibitem[Tabone and Francalanza(2022)]%
\bibfield{author}{\bibinfo{person}{Gerard Tabone} {and} \bibinfo{person}{Adrian Francalanza}.} \bibinfo{year}{2022}\natexlab{}.
\newblock \showarticletitle{Session Fidelity for ElixirST: {A} Session-Based Type System for Elixir Modules}. In \bibinfo{booktitle}{\emph{{ICE}}} \emph{(\bibinfo{series}{{EPTCS}}, Vol.~\bibinfo{volume}{365})}. \bibinfo{pages}{17--36}.
\newblock

\bibitem[Takeuchi et~al\mbox{.}(1994)]%
\bibfield{author}{\bibinfo{person}{Kaku Takeuchi}, \bibinfo{person}{Kohei Honda}, {and} \bibinfo{person}{Makoto Kubo}.} \bibinfo{year}{1994}\natexlab{}.
\newblock \showarticletitle{An Interaction-based Language and its Typing System}. In \bibinfo{booktitle}{\emph{{PARLE} '94: Parallel Architectures and Languages Europe, 6th International {PARLE} Conference, Athens, Greece, July 4-8, 1994, Proceedings}} \emph{(\bibinfo{series}{Lecture Notes in Computer Science}, Vol.~\bibinfo{volume}{817})}, \bibfield{editor}{\bibinfo{person}{Constantine Halatsis}, \bibinfo{person}{Dimitris~G. Maritsas}, \bibinfo{person}{George Philokyprou}, {and} \bibinfo{person}{Sergios Theodoridis}} (Eds.). \bibinfo{publisher}{Springer}, \bibinfo{pages}{398--413}.
\newblock
\urldef\tempurl%
\url{https://doi.org/10.1007/3-540-58184-7\_118}
\showDOI{\tempurl}

\bibitem[Tasharofi et~al\mbox{.}(2013)]%
\bibfield{author}{\bibinfo{person}{Samira Tasharofi}, \bibinfo{person}{Peter Dinges}, {and} \bibinfo{person}{Ralph~E. Johnson}.} \bibinfo{year}{2013}\natexlab{}.
\newblock \showarticletitle{Why Do Scala Developers Mix the Actor Model with other Concurrency Models?}. In \bibinfo{booktitle}{\emph{{ECOOP}}} \emph{(\bibinfo{series}{Lecture Notes in Computer Science}, Vol.~\bibinfo{volume}{7920})}. \bibinfo{publisher}{Springer}, \bibinfo{pages}{302--326}.
\newblock

\bibitem[Trinder et~al\mbox{.}(2017)]%
\bibfield{author}{\bibinfo{person}{Phil Trinder}, \bibinfo{person}{Natalia Chechina}, \bibinfo{person}{Nikolaos Papaspyrou}, \bibinfo{person}{Konstantinos Sagonas}, \bibinfo{person}{Simon Thompson}, \bibinfo{person}{Stephen Adams}, \bibinfo{person}{Stavros Aronis}, \bibinfo{person}{Robert Baker}, \bibinfo{person}{Eva Bihari}, \bibinfo{person}{Olivier Boudeville}, {et~al\mbox{.}}} \bibinfo{year}{2017}\natexlab{}.
\newblock \showarticletitle{Scaling reliably: Improving the scalability of the Erlang distributed actor platform}.
\newblock \bibinfo{journal}{\emph{ACM Transactions on Programming Languages and Systems (TOPLAS)}} \bibinfo{volume}{39}, \bibinfo{number}{4} (\bibinfo{year}{2017}), \bibinfo{pages}{1--46}.
\newblock

\bibitem[Vasconcelos(2012)]%
\bibfield{author}{\bibinfo{person}{Vasco~T. Vasconcelos}.} \bibinfo{year}{2012}\natexlab{}.
\newblock \showarticletitle{Fundamentals of session types}.
\newblock \bibinfo{journal}{\emph{Inf. Comput.}}  \bibinfo{volume}{217} (\bibinfo{year}{2012}), \bibinfo{pages}{52--70}.
\newblock

\bibitem[Wadler(2014)]%
\bibfield{author}{\bibinfo{person}{Philip Wadler}.} \bibinfo{year}{2014}\natexlab{}.
\newblock \showarticletitle{Propositions as sessions}.
\newblock \bibinfo{journal}{\emph{J. Funct. Program.}} \bibinfo{volume}{24}, \bibinfo{number}{2-3} (\bibinfo{year}{2014}), \bibinfo{pages}{384--418}.
\newblock

\bibitem[Zeilberger(2015)]%
\bibfield{author}{\bibinfo{person}{Noam Zeilberger}.} \bibinfo{year}{2015}\natexlab{}.
\newblock \bibinfo{title}{Balanced polymorphism and linear lambda calculus}.
\newblock \bibinfo{howpublished}{{Talk at TYPES}}.
\newblock
\urldef\tempurl%
\url{http://noamz.org/papers/linprin.pdf}
\showURL{%
\tempurl}

\end{thebibliography}

\clearpage
\appendix

\begin{center}
{\Huge Appendices}
\end{center}

\etoctocstyle{1}{Appendix Contents}
\etocdepthtag.toc{mtappendix}
\etocsettagdepth{mtchapter}{none}
\etocsettagdepth{mtappendix}{subsection}
\tableofcontents

\newpage

\section{Omitted Definitions}\label{ap:defs}

Here we add in the omitted definitions from the main body of the paper.

\subsection{Algorithmic environment combination operators}

\headersig{Environment join}{$\joinseq{\penv_1}{\penv_2}{\penv}{\constrs}$}
\begin{mathpar}
\inferrule
{ }
{ \joinseq{\cdot}{\cdot}{\cdot}{\emptyset} }

\inferrule
x \not\in \dom{\penv_2} \\\\
\joinseq{\penv_1}{\penv_2}{\penv}{\constrs}
{ \joinseq{\penv_1, x {:} \ptya}{\penv_2}{\penv, x {:} \ptya}{\constrs}  }

\inferrule
x \not\in \dom{\penv_1} \\\\
\joinseq{\penv_1}{\penv_2}{\penv}{\constrs}
{ \joinseq{\penv_1}{\penv_2, x {:} \ptya}{\penv, x {:} \ptya}{\constrs}  }

\inferrule
\joinseq{\ptya_1}{\ptya_2}{\ptyb}{\constrs_1} \\
\joinseq{\penv_1}{\penv_2}{\penv}{\constrs_2}
{ \joinseq
{\penv_1, x {:} \ptya_1}
{\penv_2, x {:} \ptya_2}
{\penv, x {:} \ptyb}{\constrs_1 \cup \constrs_2}
\end{mathpar}

\headersig{Environment merge}{$\mergeseq{\penv_1}{\penv_2}{\penv}{\constrs}$}
\begin{mathpar}
\inferrule
{ }
{ \mergeseq{\cdot}{\cdot}{\cdot}{\emptyset} }

\inferrule
x \not\in \dom{\penv_2} \\
\mergeseq{\penv_1}{\penv_2}{\penv}{\constrs}
\mergeseq
{ \penv_1, x {:} \basety }
{ \penv_2 }
{ \penv, x {:} \basety }
{ \constrs }

\inferrule
x \not\in \dom{\penv_2} \\
\mergeseq{\penv_1}{\penv_2}{\penv}{\constrs}
\mergeseq
{ \penv_1, x {:} \usagety{\tysend{\ppata}} }
{ \penv_2 }
{ \penv, x {:} \usagety{\tysendp{\ppata \patplus \mbone}} }
{ \constrs }

\inferrule
x \not\in \dom{\penv_1} \\
\mergeseq{\penv_1}{\penv_2}{\penv}{\constrs_2}
\mergeseq
{ \penv_1 }
{ \penv_2, x {:} \basety }
{ \penv, x {:} \ptya }
{ \constrs  }

\inferrule
x \not\in \dom{\penv_1} \\
\mergeseq{\penv_1}{\penv_2}{\penv}{\constrs_2}
\mergeseq
{ \penv_1 }
{ \penv_2, x {:} \usagety{\tysend{\ppata}} }
{ \penv, x {:} \usagety{\tysendp{\ppata \patplus \mbone}} }
{ \constrs }

\inferrule
\mergeseq{\ptya_1}{\ptya_2}{\ptyb}{\constrs_1} \\
\mergeseq{\penv_1}{\penv_2}{\penv}{\constrs_2}
\mergeseq
{ \penv_1, x {:} \ptya_1 }
{ \penv_2, x {:} \ptya_2 }
{ \penv, x {:} \ptyb }
{ \constrs_1 \cup \constrs_2 }
\end{mathpar}

\headersig{Disjoint combination}{$\combineseq{\penv_1}{\penv_2}{\penv}{\constrs}$}
\begin{mathpar}
\inferrule
{ }
{ \combineseq{\cdot}{\cdot}{\cdot}{\emptyset} }

\inferrule
x \not\in \dom{\penv_2} \\\\
\combineseq{\penv_1}{\penv_2}{\penv}{\constrs}
{ \combineseq{\penv_1, x {:} \ptya}{\penv_2}{\penv, x {:} \ptya}{\constrs}}

\inferrule
x \not\in \dom{\penv_1} \\\\
\combineseq{\penv_1}{\penv_2}{\penv}{\constrs}
{ \combineseq{\penv_1}{\penv_2, x {:} \ptya}{\penv, x {:} \ptya}{\constrs}}

\inferrule
\combineseq{\penv_1}{\penv_2}{\penv}{\constrs} \\
{ \combineseq
{\penv_1, x {:} \basety}
{\penv_2, x {:} \basety}
{\penv, x {:} \basety}
\end{mathpar}

The environment join operator $\joinseq{\penv_1}{\penv_2}{\penv}{\constrs}$
concatenates $\penv_1$ and $\penv_2$, computing the algorithmic type join of any
types for overlapping variables, and produces constraints $\constrs$.

The environment merge computes the algorithmic type merge of any overlapping
types. If a variable is in one environment but not another, then if it is a base
type, it is simply added to the output environment. If it is a send mailbox
type $\usagety{\tysend{\ppata}}$, then its type is changed to
$\usagety{\tysendp{\ppata \patplus \mbone}}$ to denote the fact that it may not
be used.

Disjoint environment combination combines two environments; if there are two
overlapping types then they must be identical base types.
\newpage
\section{Details of Extensions}\label{ap:extensions}
Here we discuss the details of the extensions overviewed

\subsection{Product and sum types}

Product and sum types can be added relatively straightforwardly. In both cases,
their components must be returnable as otherwise it would not be possible to
substitute their contents upon deconstruction.

\paragraph*{Product types.}

We can write the declarative typing rules for products as follows; the rules are
unremarkable apart from the requirement that each component of the pair must be
returnable in the elimination form.

\begin{mathpar}
\inferrule
\vseq{\tyenv_1}{\vala}{\tya} \\
\vseq{\tyenv_2}{\valb}{\tyb}
{ \tseq{\tyenv_1 + \tyenv_2}{(\vala, \valb)}{\typair{\tya}{\tyb}} }

\inferrule
\vseq{\tyenv_1}{\vala}{\typair{\tya_1}{\tya_2}} \\
\returnablepred{\tya} \\
\returnablepred{\tyb} \\
\tseq{\tyenv_2, x : \tya_1, y : \tya_2}{\vala}{\tyb}
{ \tseq{\tyenv_1 + \tyenv_2}{\letin{(x, y)}{\vala}{\tma}}{\tyb} }
\end{mathpar}

We can write the corresponding algorithmic rules as follows:

\begin{mathpar}
\inferrule
\chkseq{\vala}{\ptya}{\penv_1}{\constrs_1} \\
\chkseq{\valb}{\ptyb}{\penv_2}{\constrs_2} \\
\combineseq{\penv_1}{\penv_2}{\penv}{\constrs_3}
{ \chkseq
{(\vala, \valb)}
{\constrs_1 \cup \constrs_2 \cup \constrs_3}

\inferrule
\chkseq{\vala}{\typair{\ptya_1}{\ptya_2}}{\penv_1}{\constrs_1} \\
\returnablepred{\ptya_1} \\
\returnablepred{\ptya_2} \\
\chkseq
{\constrs_2} \\\\
\checkenvseq{\penv_2}{x}{\tya_1}{\constrs_3} \\
\checkenvseq{\penv_2}{y}{\tya_2}{\constrs_4} \\\\
\combineseq{\penv_1}{\penv_2}{\penv}{\constrs_5}
{ \chkseq
{\letin[(\typair{\ptya_1}{\ptya_2})]{(x, y)}{\vala}{\tma}}
{\constrs_1 \cup \cdots \cup \constrs_5}

\inferrule
\chkseq{\tma}{\tyb}{\penv, x : \ptya_1, y : \ptya_2}{\penv_1}{\constrs_1} \\\\
\returnablepred{\ptya_1} \\
\returnablepred{\ptya_2} \\
\chkseq{\vala}{\typair{\ptya_1}{\ptya_2}}{\penv_2}{\constrs_2} \\
\combineseq{\penv_1}{\penv_2}{\penv}{\constrs_3}
{ \chkseq
{\letin{(x, y)}{\vala}{\tma}}
{\constrs_1 \cup \constrs_2 \cup \constrs_3}
\end{mathpar}

Pair construction (\textsc{TC-Pair}) checks that both components have the given
types. Environment combination and constraints are handled as usual.
Deconstructing the pair in general requires an annotation (\textsc{TC-LetPair}); as with the let
rule, we check that the pair has the given annotation and that the types
inferred in the environment of the continuation are consistent with the
If both components of the pair are used within the continuation then we can omit
the annotation (\textsc{TC-LetPairNoAnn}): the rule first checks that the continuation
has the given type, and inspects the resulting environment to construct the
product type used for checking $\vala$.

\paragraph*{Sum types.}

Sum types are similar to product types; again, the declarative rules are
unremarkable except for the requirement that sum components must be returnable
in the elimination rule.

\begin{mathpar}
\inferrule
{ \vseq{\tyenv}{\vala}{\tya} }
{ \vseq{\tyenv}{\inl{\vala}}{\tysum{\tya}{\tyb}} }

\inferrule
{ \vseq{\tyenv}{\vala}{\tyb} }
{ \vseq{\tyenv}{\inr{\vala}}{\tysum{\tya}{\tyb}} }

\inferrule
\tseq{\tyenv_1 }{\vala}{\tysum{\tya_1}{\tya_2}} \\\\
\returnablepred{\tya} \\
\returnablepred{\tyb} \\
\tseq{\tyenv_2, x : \tya_1}{\tma}{\tyb} \\
\tseq{\tyenv_2, y : \tya_2}{\tmb}{\tyb}
{ \tseq{\tyenv}{\caseofcore{\vala}{x : \tya_1}{\tma}{y : \tya_2}{\tmb}}{\tyb} }

\inferrule
\tseq{\tyenv_1 }{\vala}{\tysum{\tya_1}{\tya_2}} \\\\
\tseq{\tyenv_2, x : \tya_1}{\tma}{\tyb} \\
\tseq{\tyenv_2, y : \tya_2}{\tmb}{\tyb}
{ \tseq{\tyenv}{\caseofcore{\vala}{x}{\tma}{y}{\tmb}}{\tyb} }
\end{mathpar}

We can also write the corresponding algorithmic rules:

\begin{mathpar}
\inferrule
{ \chkseq{\vala}{\ptya}{\penv}{\constrs} }
{ \chkseq{\inl{\vala}}{\tysum{\ptya}{\ptyb}}{\penv}{\constrs} }

\inferrule
{ \chkseq{\vala}{\ptyb}{\penv}{\constrs} }
{ \chkseq{\inr{\vala}}{\tysum{\ptya}{\ptyb}}{\penv}{\constrs} }

\inferrule
\chkseq{\vala}{\tysum{\tya}{\tyb}}{\penv_1}{\constrs_1} \\
\chkseq{\tma}{\ptya}{\penv_2}{\constrs_2} \\\\
\chkseq{\tmb}{\ptya}{\penv_3}{\constrs_3} \\
\checkenvseq{\penv_2}{x}{\tya}{\constrs_4} \\\\
\checkenvseq{\penv_3}{y}{\tyb}{\constrs_5} \\
\mergeseq{\envwithouttwo{\penv_2}{x}}{\envwithouttwo{\penv_3}{y}}{\penv_4}{\constrs_6} \\
\combineseq{\penv_1}{\penv_4}{\penv}{\constrs_7}
{ \chkseq
{\inl{x}: \tya \mapsto \tma; \inr{y}: \tyb \mapsto \tmb}
{ \penv }
{ \constrs_1 \cup \cdots \cup \constrs_7 }

\inferrule
\chkseq{\tma}{\ptya}{\penv_1, x : \ptya_1}{\constrs_1} \\
\chkseq{\tmb}{\ptya}{\penv_2, y : \ptya_2}{\constrs_2} \\\\
\chkseq{\vala}{\ptya_1 + \ptya_2}{\penv_3}{\constrs_3} \\
\mergeseq{\penv_1}{\penv_2}{\penv_4}{\constrs_4} \\
\combineseq{\penv_3}{\penv_4}{\penv}{\constrs_5}
{ \chkseq
{\caseof{\vala}{\inl{x} \mapsto \tma; \inr{y} \mapsto \tmb}}
{\constrs_1 \cup \cdots \cup \constrs_5}
\end{mathpar}

As expected, sum injections are checking cases; similar to the product rules, we
also have two separate rules for case expressions which allow annotations to be
elided if both $x$ and $y$ are used within continuations $\tma$ and $\tmb$.

\subsection{Contextual Type Information}

The other main extension supplements co-contextual type checking with contextual
type information in order to enable extensions such as higher-order functions
and interfaces.

\subsubsection{Extended syntax}

We begin by showing the modified syntax.

\header{Syntax}
\[
\begin{array}{lrcl}
\text{Modified types} & \ppretya, \ppretyb & ::= &
\basety \midspace \tysendiface{\ppata} \midspace
\tyrecviface{\ppatb} \midspace \tyannfun{\seq{\ptya}}{\ptyb}
\\
\text{Interfaces} & \iface & ::= & \cdot \midspace I, \msgtag{m}
\mapsto \ppretya \\
\text{Linearity annotations} & \linann & ::= & \linear \midspace
\unrestricted \\
\text{Additional values} & \vala, \valb & ::= & \cdots \midspace
\flaglambda{\seq{x : \ptya}}{\ptyb}{\tma}
\\
\text{Modified computations} & \tma, \tmb & ::= & \cdots \midspace
\appann{\vala}{\tyfun{\seq{\ptya}}{\ptyb}}{\valb} \midspace
\mbnewiface
\midspace
\guardifaceann{\vala}{\pata}{\seq{\gd}} \\
& &  \midspace & \sendann{\vala}{\iface}{m}{\seq{\valb}}
\end{array}
\]

Like signatures in the core calculus, interfaces $\iface$ map message names to
lists of types.
We modify types $\ppretya, \ppretyb$ to include \emph{interface-annotated}
mailbox types, as well as $n$-ary function types $\tyannfun{\seq{\ptya}}{\ptyb}$
that are annotated as either \emph{linear} ($\linear$, meaning that the function
closes over linear variables and therefore must be used precisely once) or
\emph{unrestricted} ($\unrestricted$, meaning that the function only closes over
unrestricted variables and therefore can be used an unlimited number of times).

\paragraph*{First-class functions.}
We extend values with fully-annotated, $n$-ary anonymous functions. We require a
return annotation since we wish to check the body type, while also synthesising
a return type. We opt for an $n$-ary function rather than a curried
representation because anonymous functions may only close over returnable
values, to ensure they do not violate the conditions on lexical scoping
once applied.

\begin{example}
Consider the following expression:

\[
\bl
\letintwo{\var{mb}}{\mbnew} \\
\letintwo{f}{(\linlambda{}{\one}{\send{\var{mb}}{m}{}})} \\
\guardanntwo{\var{mb}}{\msgtag{m}} \\
\quad \receive{m}{}{\var{mb}}{\sugarfree{\var{mb}}} \\
\} \\
\fnapp{f}{}
\el
\]

Here we bind $f$ to a function which sends message $\msgtag{m}$ to mailbox
$\var{mb}$; note that it is used lexically before the $\calcwd{guard}$, which
aligns with type combination. However, after reducing the expression (assuming
that $a$ is chosen as a runtime name), we obtain the following term:

\[
\bl
\guardanntwo{\var{a}}{\msgtag{m}} \\
\quad \receive{m}{}{\var{mb}}{\sugarfree{\var{mb}}} \\
\} \\
\fnapp{(\linlambda{}{\one}{\send{\var{mb}}{m}{}})}{}
\el
\]

After substituting the function body for $f$ we now have a second-class use
\emph{after} the first-class use, violating the ordering of returnable and
second-class usages.
\end{example}

\paragraph*{Mailbox terms.}
We extend computations so that a user specifies an interface $\iface$ when creating a
mailbox ($\mbnewiface$). Furthermore, we also augment send and guard expressions
with the interface of the mailbox they operate on. Unlike the annotation on
$\mbnew$, this does not need to be specified by the user, but instead is added
by a straightforward type-directed translation.

\subsubsection{Type-directed translation}
We propagate annotations to function application and mailbox terms via a
contextual type-directed translation.

To do so, we introduce \emph{pre-types} $\contya, \contyb$: the main difference
is that mailbox types \emph{do not} carry a pattern, but only an interface.

\[
\begin{array}{lrcl}
\text{Pre-types} & \contya, \contyb & ::= & \basety \midspace \conmb
\midspace \tyannfun{\seq{\contya}}{\contyb} \\
\text{Pre-type environments} & \contyenv & ::= & \cdot \midspace
\contyenv, x : \contya
\end{array}
\]

The type-directed translation pass follows the form of a standard type system
for the simply-typed $\lambda$ calculus so we omit the rules here. However the
judgement has the form $\anntmseq{\contyenv}{\tma}{\contya}{\tmb}$ which can be
read ``under pre-type environment $\contyenv$, term $\tma$ has pre-type
$\contya$ and produces annotated term $\tmb$''.

\subsubsection{Constraint generation rules}

Finally, we can see how to write constraint generation rules for the extended
calculus. The rules in the declarative setting are similar.

\begin{minipage}{\textwidth}
\headertwo
{Modified constraint generation rules}
\framebox{$\chkseq{\tma}{\ptya}{\penv}{\constrs}$}~
\framebox{$\chkgseqcon{\pata}{\iface}{\gd}{\ptya}{\nullableenv}{\constrs}{\patb}$}}

\begin{mathpar}
\inferrule
\chkseq{\tma}{\ptyb}{\penv'}{\constrs_1} \\
\penv = \penv' \envwithout \seq{x} \\\\
\checkenvseq{\seq{x}}{\seq{\ptya}}{\penv'}{\constrs_2} \\
\returnablepred{\penv}
\synthseq
{\linlambda{\seq{x : \ptya}}{\ptyb}{\tma}}
{\constrs_1 \cup \constrs_2}

\inferrule
\chkseq{\tma}{\ptyb}{\penv'}{\constrs_1} \\
\penv = \penv' \envwithout \seq{x} \\\\
\checkenvseq{\seq{x}}{\seq{\ptya}}{\penv'}{\constrs_2} \\
\unrseq{\penv}{\constrs_3} \\
\returnablepred{\penv}
\synthseq
{\unlambda{\seq{x : \ptya}}{\ptyb}{\tma}}
{\constrs_1 \cup \constrs_2 \cup \constrs_3}

\inferrule
\chkseq
\\\\
(\chkseq{\valb_i}{\ptya_i}{\penv_i}{\constrs_i})_{i \in 1..n} \\
\combineseqmany{\penv' + \penv_1 + \ldots + \penv_n}{\penv}{\constrs}
{ \synthseq
{ \appann{\vala}{\tyannfun{\seq{\ptya}}{\ptyb}}{\seq{\valb}} }
{\constrs \cup \constrs_1 \cup \ldots \cup \constrs_n}

\inferrule
\iface(\msgtag{m}) = \seq{\ppretya} \\
\chkseq{\vala}{\usablety{\tysendiface{\msgtag{m}}}}{\penv'}{\constrs}
\\\\
(\chkseq{\valb_i}{\makeusable{\ppretya_i}}{\penv_i}{\constrs'_i})_i \\
\combineseqmany{\penv' + \penv_1 + \cdots + \penv_n}{\penv}{\constrs''}
{ \synthseq
{ \constrs \cup \constrs'_1 \cup \cdots \cup \constrs'_n \cup \constrs''}

\inferrule
{ }
{ \synthseq{\mbnewiface}{\retty{\tyrecviface{\mbone}}}{\cdot}{\emptyset} }

\inferrule
\chkgseqcon
{\patb} \\\\
\chkseq{\vala}{\retty{\tyrecviface{\patb}}}{\penv'}{\constrs_2} \\
\combineseq{\nullableenv}{\penv'}{\penv}{\constrs_3}
{ \chkseq
{\constrs_1 \cup \constrs_2 \cup \constrs_3 \cup
\set{\subpatconstr{\pata}{\patb} }}

\inferrule
\chkseq{\tma}{\ptya}{\penv', y : \retty{\tyrecviface{\ppata}}}{\constrs_1} \\
I(\msgtag{m}) = {\seq{\ppretya}} \\
\penv = \penv' \envwithout \seq{x} \\
\interfaces{\seq{\ppretya}} \cap \interfaces{\penv} = \emptyset \\
\checkenvseq{\penv'}{\seq{x}}{\seq{\makeusable{\ppretya}}}{\constrs_2}
{ \chkgseqcon
{\constrs_1 \cup \constrs_2 \cup
\set{\subpatconstr{\pata \without \msgtag{m}}{\ppata}}
{\algomsg{m} \patconcat (\pata \without \msgtag{m})}
\end{mathpar}
\end{minipage}

We require three new rules for first-class functions: \textsc{TS-LinLam} types a
linear anonymous function by checking that the body has the given result type,
and the inferred environment uses variables consistently with the parameter
annotations; the rule synthesises a type consistent with the annotation.
Further, we require that the inferred environment only closes over
variables with returnable types. Rule \textsc{TS-UnLam} is similar, but
additionally requires that the inferred environment is unrestricted. Rule
\textsc{TS-FnApp} types an annotated function application, checking that the
function has the given annotation and that the arguments have the correct types.

As for the rules that support interfaces, rule \textsc{TS-Send} is similar but
looks up the types according to the interface rather than the global signature,
and checks that the target mailbox has the given interface. Rule \textsc{TS-New}
synthesises a mailbox type with the user-supplied interface. Finally, we modify
the shape of the guard typing judgement to record the interface of the mailbox
being guarded upon, and use this to look up the desired payload types in
\textsc{TCG-Recv}.

\newpage
\section{Supplementary Implementation and Evaluation Material}\label{ap:evaluation}

Our typechecking tool processes \langname\ programs specified in plain text files that are structured in three segments:

\begin{enumerate}
\item \textbf{Interface definitions} that establish the set of messages that a mailbox can receive;

\item\label{itm:function_definitions} \textbf{Function definitions} that specify processes that are instantiable using \lstinline+spawn+;

\item \textbf{Body} an invocation of a function defined in (\ref{itm:function_definitions}) that acts as the program entry point.
\end{enumerate}

\langname\ programs are type checked following the six-stage pipeline of \Cref{fig:implementation-pipeline}; see \secref{sec:implementation_overview} for an overview.

\begin{figure}[t]
\centering
\includegraphics[width=\textwidth]{figs/flowchart.pdf}
\caption{\langname\ type checking pipeline}
\label{fig:implementation-pipeline}
\end{figure}

\subsection{Experimental Conditions}
We report the mean typechecking time, excluding phases 1--3 of the pipeline.
Measurements are made on a MacBook M1 Pro with 16GB of memory, running macOS
13.2 and OCaml 5.0.  To ensure minimal variability in our measurements show in
\Cref{tbl:examples-table}, we preformed 1000 repetition of each experiment.
The number of repetitions  was determined empirically by calculating the
coefficient of variation (CV)~\cite{Devore12}, \ie\ the ratio of the standard
deviation to the mean, $\textrm{CV}=\sigma/\bar{x}$, for different repetitions
until an adequately-low value ($<\!10\%$) was obtained.

\subsection{Case Study}\label{ap:case_study}

We give the full \langname\ program for our factory case study described in \secref{sec:case_study_robots}.
The interaction sequence between our different entities, Robots, Door, and Warehouse, is captured in \Cref{fig:factory-seqdiag} and naturally translates to the code that follows.

\paragraph{Interfaces}
The messages that Robot, Door, and Warehouse accept are defined by the interfaces:

\noindent
\begin{lstlisting}[language=Pat, emph={self}, firstnumber=1]
interface Robot { (*\label[ln]{ln:begin_interfaces}*)
GoIn(Door!), GoOut(Door!), Busy(), Delivered(Warehouse!, Door!)

interface Door {
Want(Int, Robot!), Inside(Robot!), Outside(), WantLeave(Robot!), Prepared(Warehouse!), TableIdle()

interface Warehouse {
Prepare(Int, Door!), Deliver(Robot!, Door!), PartTaken()
} (*\label[ln]{ln:end_interfaces}*)
\end{lstlisting}

\paragraph{Robot}
Robots are initially \lstinline+idle+ and issue a \lstinline+Want+ message to the Door to obtain Warehouse access (\cref{ln:door_want}).
The Door replies either with the message \lstinline+Busy+, in which case the Robot terminates (lines \ref{ln:robot_terminate_start}\crefrangeconjunction\ref{ln:robot_terminate_end}), or \lstinline+GoIn+, to which the Robot replies by an \lstinline+Inside+ message
before transitioning to the \lstinline+working+ state (lines \ref{ln:robot_working_start}\crefrangeconjunction\ref{ln:robot_working_end}).
When in \lstinline+working+ state, the Robot expects one \lstinline+Delivered+ message, as the guard on \cref{ln:robot_guard_delivered} asserts.
This informs the Robot that the part is delivered by the Warehouse.
The recipient Robot replies by sending \lstinline+PartTaken+, and notifies the Door that it wants to exit via \lstinline+WantLeave+ on lines \ref{ln:robot_delivered_start}\crefrangeconjunction\ref{ln:robot_delivered_end}.
It then awaits \lstinline+GoOut+ and finalises its negotiation with the Door through an \lstinline+Outside+ message.

\begin{lrbox}{\listingbox}
\begin{minipage}[b]{.47\textwidth}
\begin{lstlisting}[language=Pat, emph={self}, firstnumber=12]
def idle(self: Robot?, door: Door!): Unit {
door ! Want(0, self); (*\label[ln]{ln:door_want}*)
guard self: (Busy + GoIn) {
receive Busy() from self (*$\shortrightarrow$*) (*\label[ln]{ln:robot_terminate_start}*)
free(self) (*\label[ln]{ln:robot_terminate_end}*)
receive GoIn(door) from self (*$\shortrightarrow$*)  (*\label[ln]{ln:robot_working_start}*)
door ! Inside(self);
working(self) (*\label[ln]{ln:robot_working_end}*)
\end{lstlisting}
\end{minipage}
\end{lrbox}
\noindent
\raisebox{0.5em}{\usebox{\listingbox}}
\hfill
\begin{minipage}[b]{.47\textwidth}
\begin{lstlisting}[language=Pat, emph={self}, firstnumber=last]
def working(self: Robot?): Unit {
let self = guard self: Delivered { (*\label[ln]{ln:robot_guard_delivered}*)
receive Delivered(wh, door) from self (*$\shortrightarrow$*)
wh ! PartTaken(); (*\label[ln]{ln:robot_delivered_start}*)
door ! WantLeave(self); self (*\label[ln]{ln:robot_delivered_end}*)
} in guard self: GoOut {
receive GoOut(door) from self (*$\shortrightarrow$*)
door ! Outside();
\end{lstlisting}
\end{minipage}

\paragraph{Door}
The Door
accepts zero or more \lstinline+Want+
messages, replying to each with \lstinline+Busy+ or \lstinline+GoIn+.
In the latter case, the Door informs the Warehouse of an inbound Robot by sending it a \lstinline+Prepare+ message, and transitioning to the \lstinline+busy+ state (lines \ref{ln:door_go_in_start}\crefrangeconjunction\ref{ln:door_go_in_end}).
Both \lstinline+GoIn+ and \lstinline+Prepare+ include an updated self-reference to ensure precise types.
clause \lstinline+free+ on \cref{ln:door_guard_free} handles the case where no Robots are present.
When \lstinline+busy+, the Door mailbox potentially contains an \lstinline+Inside+ message from the admitted Robot, a \lstinline+Prepared+ message from the Warehouse,
and \lstinline+Want+ messages sent by other Robots requesting access (\cref{ln:door_busy_guard}).
These \lstinline+Want+ messages are answered with \lstinline+Busy+, as lines \ref{ln:door_answer_busy_start}\crefrangeconjunction\ref{ln:door_answer_busy_end} show.
Once the Door receives the \lstinline+Inside+ message, it awaits a \lstinline+Prepared+ message issued by the Warehouse, before notifying the latter that the Robot is collecting its part via \lstinline+Deliver+ (lines \cref{ln:door_inside_deliver_start}\crefrangeconjunction\ref{ln:door_inside_deliver_end}).
Eventually, the Robot demands exit
by sending \lstinline+WantLeave+ to the Door, which handles it on lines \cref{ln:door_handle_want_leave_start}\crefrangeconjunction\ref{ln:door_handle_want_leave_end}.
The Door transitions to the \lstinline+ready+ state, whereupon it confirms that the Robot has exited and that the Warehouse is available; these interactions are captured by the \lstinline+Outside+ and \lstinline+TableIdle+ messages respectively (lines \ref{ln:door_outside_tableidle_start}\crefrangeconjunction\ref{ln:door_outside_tableidle_end}).
Finally, the Door transitions back to \lstinline+clear+ on \cref{ln:door_transition_clear}, ready to service other Robots.

\noindent
\begin{minipage}[b]{.47\textwidth}
\begin{lstlisting}[language=Pat, emph={self}, firstnumber=33]
def clear(self: Door?, wh: Warehouse!): Unit {
guard self: *Want {
free (*$\shortrightarrow$*) () (*\label[ln]{ln:door_guard_free}*)
receive Want(part, robot) from self (*$\shortrightarrow$*) (*\label[ln]{ln:door_go_in_start}*)
robot ! GoIn(self);
wh ! Prepare(part, self);
busy(self) (*\label[ln]{ln:door_go_in_end}*)

def busy(self: Door?): Unit {
guard self: Inside.Prepared.*Want { (*\label[ln]{ln:door_busy_guard}*)
receive Want(partNum, robot) from self (*$\shortrightarrow$*) (*\label[ln]{ln:door_answer_busy_start}*)
robot ! Busy();
busy(self) (*\label[ln]{ln:door_answer_busy_end}*)
receive Inside(robot) from self (*$\shortrightarrow$*) (*\label[ln]{ln:door_inside_deliver_start}*)
guard self: Prepared.*Want {
receive Prepared(wh) from self (*$\shortrightarrow$*)
wh ! Deliver(robot, self); (*\label[ln]{ln:door_inside_deliver_end}*)
guard self: WantLeave.TableIdle.*Want {
receive WantLeave(robot) from self (*$\shortrightarrow$*) (*\label[ln]{ln:door_handle_want_leave_start}*)
robot ! GoOut(self); (*\label[ln]{ln:door_handle_want_leave_end}*)
ready(self, wh)
\end{lstlisting}
\end{minipage}
\hfill
\begin{lrbox}{\listingbox}
\begin{minipage}[b]{.47\textwidth}
\begin{lstlisting}[language=Pat, emph={self}, firstnumber=last]
def ready(self: Door?, wh: Warehouse!): Unit {
guard self: Outside.TableIdle.*Want {
# Handle messages Outside and TableIdle in
# any order (code omitted) and clear door.
receive Outside() from self (*$\shortrightarrow$*) (*\label[ln]{ln:door_outside_tableidle_start}*)
guard self: TableIdle.*Want {
receive TableIdle(wh) from self (*$\shortrightarrow$*)
clear(self, wh)
receive TableIdle(wh) from self (*$\shortrightarrow$*)
guard self: Outside.*Want {
receive Outside() from self (*$\shortrightarrow$*)
clear(self, wh)
} (*\label[ln]{ln:door_outside_tableidle_end}*)
clear(self, wh) (*\label{ln:door_transition_clear}*)
\end{lstlisting}
\end{minipage}
\end{lrbox}
\raisebox{4em}{\usebox{\listingbox}}

\paragraph{Warehouse}
The Warehouse in its \lstinline+empty+ state expects a \lstinline+Prepare+ message (if there are Robots in the system), or none (if no Robot requests access), \ie\ the guard \lstinline:Prepared + 1: on \cref{ln:warehouse_prepare_or_not}.
When a part is requested, the Warehouse transitions to the \lstinline+engaged+ state and awaits a \lstinline+Deliver+ message from the Door, notifying the Robot collecting the part via a \lstinline+Delivered+ message (lines \ref{ln:warehouse_collect_part_start}\crefrangeconjunction\ref{ln:warehouse_collect_part_end}).
The Robot acknowledges the delivery by sending \lstinline+PartTaken+, as the guard on \cref{ln:warehouse_part_taken} stipulates.
To conclude its interaction with the Door, the Warehouse sends \lstinline+TableIdle+ before transitioning back to \lstinline+empty+.

\begin{lrbox}{\listingbox}
\begin{minipage}[b]{.47\textwidth}
\begin{lstlisting}[language=Pat, emph={self}, firstnumber=77]
def empty(self: wh?): Unit {
guard self: Prepare + 1 { (*\label[ln]{ln:warehouse_prepare_or_not}*)
free (*$\shortrightarrow$*) ()
receive Prepare(partNum, door) from self (*$\shortrightarrow$*)
door ! Prepared(self);

def engaged(self: wh?): Unit { (*\label[ln]{ln:warehouse_collect_part_start}*)
guard self: Deliver {
receive Deliver(robot, door) from self (*$\shortrightarrow$*)
robot ! Delivered(self, door);
given(self, door)
} (*\label[ln]{ln:warehouse_collect_part_end}*)
\end{lstlisting}
\end{minipage}
\end{lrbox}

\noindent
\raisebox{0em}{\usebox{\listingbox}}
\hfill
\begin{minipage}[b]{.47\textwidth}
\begin{lstlisting}[language=Pat, emph={self}, firstnumber=last]
def given(self: wh?, door: Door!): Unit {
guard self : PartTaken { (*\label[ln]{ln:warehouse_part_taken}*)
receive PartTaken() from self (*$\shortrightarrow$*)
door ! TableIdle(self);

def main(): Unit { # Launcher function.
let robot(*$_i$*) = new[Robot] in # (*\color{Gray}{$n$}*) Robot mailboxes.
let door = new[Door] in
let wh = new[Warehouse] in
spawn { clear(door, wh) }; # Door. (*\label[ln]{ln:main_spawn_start}*)
spawn { idle(robot(*$_i$*), door) }; # (*\color{Gray}{$n$}*) Robots.
spawn { empty(wh) } # Warehouse. (*\label[ln]{ln:main_spawn_end}*)
\end{lstlisting}
\end{minipage}

The function \lstinline+main()+ creates $n$ \lstinline+Robot+ mailboxes, together with a \lstinline+Door+ and \lstinline+Warehouse+ mailbox, spawning the respective processes on lines \ref{ln:main_spawn_start}\crefrangeconjunction\ref{ln:main_spawn_end}.

\newpage
\section{Proofs}\label{ap:proofs}
\subsection{Preservation}

\subsubsection{Auxiliary Definitions and Lemmas}

We extend $\returnablepred{-}$ to typing environments, writing
$\returnablepred{\tyenv}$ if $\returnablepred{\tya}$ for each $x : \tya \in
\tyenv$.
Similarly, we write $\irrelevantpred{\tya}$ if $\tya$ is irrelevant (i.e., it is
a mailbox type $\usagety{\tysend{\pata}} \subtype \usagety{\mbsendone}$), and
extend this to environments.

We write $\fv{\tma}$ to return the free variables of a term.

Environment subtyping includes a notion of weakening. Read top-down, environment
subtyping rules allow us to add a variable with mailbox type $\mbsendone$,
replace a type with its subtype, and add in base types.
It is therefore useful to introduce a definition referring to the class of types
which can be added in through \textsc{T-Sub} which may not be used by a term.
We call these types \emph{cruft}. Cruft is a refinement of $\un{-}$ since it
also encompasses types which are \emph{subtypes} of $\mbsendone$.

\begin{definition}[Cruft]
A type $\pretya$ is \emph{cruft}, written $\cruftpred{\pretya}$, if either
$\pretya$ is a base type, or $\irrelevantpred{\pretya}$.

A usage-aware type $\usagety{\pretya}$ is cruft if $\usage = \usable$ and $\pretya$ is cruft.
\end{definition}

It helps to define a stricter version of environment subtyping which does not
permit weakening:

\begin{definition}[Strict environment subtyping]
An environment $\tyenv$ is a \emph{strict subtype environment} of an environment
$\tyenv'$, written $\strictsubtytwo{\tyenv}{\tyenv'}$ if $\tyenv \subtype \tyenv'$ and $\dom{\tyenv} = \dom{\tyenv'}$.
\end{definition}

We extend $\cruftpred{-}$ to type environments and usage-aware type environments
in the usual way.

\begin{definition}[Cruftless]
We say that an environment is \emph{cruftless for a term} $\tma$ if
$\tseq{\tyenv}{\tma}{\tya}$ and $\dom{\tyenv} = \fv{\tma}$.
\end{definition}

Let us also use $\Pi$ to range over type environments.
A crucial lemma for taming the complexity of environment subtyping is the
following, which allows us to separate the type environment required for typing
the term from the cruft introduced by environment subtyping.

\begin{lemma}\label{lem:disjoint-from-cruft}
If $\tseq{\tyenv}{\tma}{\tya}$, then there exist $\tyenvb_1, \tyenvb_2,
\tyenvb_3$ such

\begin{itemize}
\item $\tyenv = \tyenvb_1, \tyenvb_2$
\item $\tseq{\tyenvb_3}{\tma}{\tya'}$
\item $\tyenvb_1$ is cruftless for $\tma$, and $\tyenvb_1 \strictsubty \tyenvb_3$
\item $\tya' \subtype \tya$
\item $\cruftpred{\tyenvb_2}$
\end{itemize}
\end{lemma}
\begin{proof}
Follows from the definition of environment subtyping: read top-down, each
application of environment subtyping will either add a variable with an
unrestricted type, or alter the type of an existing variable.
\end{proof}

The substitution lemma is only defined on disjoint environments: we should not
be substituting a name into a term where it is already free. This is ensured by
distinguishing between returnable and second-class usages of a variable: if a
variable is returnable, then we know it cannot be used within the term into
which it is being substituted. If a variable is second-class, then there will be
no applicable reduction rules which result in substitution.

\begin{lemma}[Substitution]\label{lem:substitution}
\begin{itemize}
\item $\tseq{\tyenv_1, x : \tya}{M}{\tyb}$
\item $\vseq{\tyenv_2}{V}{\tya'}$
\item $\subtypetwo{\tya'}{\tya}$
\item $\tyenv_1 + \tyenv_2$ is defined
\end{itemize}

then $\tseq{\tyenv_1 + \tyenv_2}{M \{ V / x \}}{\tyb}$.
\end{lemma}
\begin{proof}
By induction on the derivation of $\tseq{\tyenv_1, x : \tya}{M}{\tyb}$.
\end{proof}

\begin{lemma}[Subtyping preserves reliablility / usability~\cite{dP18:mbc}]
\label{lem:subtype-usability}
If $\subtypetwo{\tya}{\tyb}$, then:

\begin{enumerate}
\item $\tya$ reliable implies $\tyb$ reliable
\item $\tyb$ usable implies $\tya$ usable
\end{enumerate}
\end{lemma}

\begin{corollary}
\label{lem:subenv-env-usability}
If $\subtypetwo{\tyenv_1}{\tyenv_2}$ then:
\begin{enumerate}
\item $\tyenv_1$ reliable implies $\tyenv_2$ reliable
\item $\tyenv_2$ usable implies $\tyenv_2$ usable
\end{enumerate}
\end{corollary}

\begin{restatable}[Balancing~\cite{dP18:mbc}]{lemma}{balancing}
\label{lem:balancing}
If $\patconcattwo{\msgtag{m}}{\patb} \subpatone \pata$
where $\patb \not\subpatone \mbzero$ and
$E \without \msgtag{m}$ is defined, then
$\subpat{\patb}{\pata \without \msgtag{m}}$.
\end{restatable}

\begin{lemma}\label{lem:returnable-subtype}
If $\tya \subtype \tyb$ and $\returnablepred{\tyb}$, then $\returnablepred{\tya}$
\end{lemma}
\begin{proof}
Follows from the fact that $\returnable \subtype \usable$.
\end{proof}

\begin{corollary}\label{cor:returnable-subtype-env}
If $\tyenv_1 \strictsubty \tyenv_2$ and
$\returnablepred{\tyenv_2}$, then
\end{corollary}

\begin{lemma}\label{lem:returnable-val-env}
If $\vseq{\tyenv}{\vala}{\tya}$ where $\returnablepred{\tya}$ and $\tyenv$ is
cruftless for $\vala$, then $\returnablepred{\tyenv}$.
\end{lemma}
\begin{proof}
By case analysis on the derivation of $\vseq{\tyenv}{\vala}{\tya}$.
\end{proof}

\begin{restatable}{lemma}{returnablenonaliased}\label{lem:returnable-non-aliased}
If $\scombtwo{(\tyenvb_1, \tyenvb_2)}{\tyenv}$ is defined and
then $\scombtwo{\tyenvb_1, \tyenvb_2}{\tyenv} = \tyenvb_1 + (\scombtwo{\tyenvb_2}{\tyenv})$.
\end{restatable}
\begin{proof}\hfill
Follows from the definition of usage combination:
the operation is not symmetric for returnable mailbox types, so the returnable mailbox type must be the last occurrence of that name in the combination. For base types, the definitions of combination for $\scomb$ and $+$ coincide.
\end{proof}

\begin{lemma}\label{lem:scomb-plus-defined}
If $\scombtwo{\tyenv_1}{\tyenv_2}$ is defined, with $\tyenv_1$ and
$\tyenv_2$ sharing only variables of base type, then
$\pluscombtwo{\tyenv_1}{\tyenv_2}$ is defined.
\end{lemma}
\begin{proof}
Immediate from the definitions.
\end{proof}

\begin{lemma}[$\scomb$ is associative]\label{lem:scomb-assoc}\hfill
$\tya_1 \scomb (\tya_2 \scomb \tya_3) \iff (\tya_1 \scomb \tya_2) \scomb \tya_3$
\end{lemma}
\begin{proof}
Follows from the fact that usage combination is associative, and that we
identify patterns up to commutativity and associativity.
\end{proof}

Extending to usage-aware type environments, we get the following corollary:

\begin{corollary}\label{lem:scomb-env-assoc}\hfill
$\tyenv_1 \scomb (\tyenv_2 \scomb \tyenv_3) \iff (\tyenv_1 \scomb \tyenv_2) \scomb \tyenv_3$
\end{corollary}

The same result holds for runtime type environments and $\pcomb$:

\begin{lemma}[$\pcomb$ is associative]\label{lem:pcomb-env-assoc}\hfill
$\plainenv_1 \pcomb (\plainenv_2 \pcomb \plainenv_3) \iff (\plainenv_1 \pcomb \plainenv_2) \pcomb \plainenv_3$
\end{lemma}
\begin{proof}
Follows the same reasoning as for $\scomb$.
\end{proof}

\begin{lemma}\label{lem:pcomb-env-comm}
The $\pcomb$ operator is commutative:
$\plainenv_1 \pcomb \plainenv_2 = \plainenv_2 \pcomb \plainenv_1$.
\end{lemma}
\begin{proof}
Follows from the fact that $\mbcomb$ is commutative.
\end{proof}

\begin{lemma}\label{lem:plus-scomb-env}
$\tyenv_1 + (\tyenv_2 \scomb \tyenv_3) = (\tyenv_1 + \tyenv_2) \scomb \tyenv_3$.
\end{lemma}
\begin{proof}
Follows directly from the definitions.
\end{proof}

\begin{lemma}\label{lem:disjoint-scomb}
If $\tyenv_1, \tyenv_2 = \tyenv$, then $\tyenv_1 \scomb \tyenv_2 = \tyenv$
\end{lemma}
\begin{proof}
Follows from the definition of $\scomb$ given that $\tyenv_1$ and
$\tyenv_2$ are disjoint.
\end{proof}

\begin{lemma}\label{lem:scomb-to-pcomb}
If $\tyenv_1 \scomb \tyenv_2 = \tyenv$, then $\strip{\tyenv_1} \pcomb
\strip{\tyenv_2} = \strip{\tyenv}$.
\end{lemma}
\begin{proof}
Follows directly from the definitions, since $\pcomb$ is more liberal than $\scomb$.
\end{proof}

\begin{lemma}\label{lem:pcomb-to-scomb}
$\strip{\tyenv} \pcomb \plainenv = \strip{\makeusable{\plainenv} \scomb \tyenv}$.
\end{lemma}
\begin{proof}
For each $x$ such that $x : \pretya \in \strip{\tyenv}$ and $x : \pretyb \in
\plainenv$, since
$\strip{\tyenv} \pcomb \plainenv$ is defined, we have that $\pretya \mbcomb
\pretyb$ is defined. The result then follows from the definition of
$\scomb$, noting that all types in $\makeusable{\plainenv}$ are usable and
therefore combinable with any other usage.
\end{proof}

\begin{lemma}\label{lem:cruft-irrelevant}
If $\scombtwo{\tyenv_1}{\tyenv_2} = \tyenv$ and $\irrelevantpred{\tyenv_1}$,
then $\tyenv_2 \tyequiv \tyenv$.
\end{lemma}
\begin{proof}
Since $\irrelevantpred{\tyenv_1}$, we have that for each $x : \tya$, it is
the case that $\tya = \usablety{\tysend{\pata}}$ where $\pata \incll \mbone$.
\end{proof}

\subsubsection{Preservation proof}

\begin{lemma}[Preservation (Equivalence)]\label{lem:equiv-pres}
If $\cseq{\tyenv}{\config{C}}$ and $\config{C} \equiv \config{D}$, then
\end{lemma}
\begin{proof}
By induction on the derivation of $\config{C} \equiv \config{D}$, relying on
Lemmas~\ref{lem:pcomb-env-assoc} and~\ref{lem:pcomb-env-comm} and \textsc{TC-Subs}.
\end{proof}

\preservation*
\begin{proof}
By induction on the derivation of $\cseq{\tyenv}{\config{C}}$.

\begin{proofcase}{E-Let}

\begin{mathpar}
\inferrule
\inferrule
\scombtwo{\tyenv_1}{\tyenv_2} = \makereturnable{\plainenv'} \\
\inferrule
\scombtwo{\tyenv_3}{\tyenv_4} = \tyenv_1 \\
\tseq{\tyenv_3}{\tma}{\makereturnable{\pretya}} \\\\
\tseq{\tyenv_4, x : \makereturnable{\pretya}}{\tmb}{\tyb}
{ \tseq{\tyenv_1}{\letin[\pretya]{x}{\tma}{\tmb}}{\tyb} } \\
\inferrule
{ \stackseq{\tyenv_2}{\tyb}{\framestack}}
{ \cseq{\plainenv'}{\thread{\letin[\pretya]{x}{\tma}{\tmb}}{\framestack}} }
{ \cseq{\plainenv}{\thread{\letin[\pretya]{x}{\tma}{\tmb}}{\framestack}} }
\end{mathpar}

\begin{itemize}
\item $\plainenv \subtype \plainenv'$
\item $\makereturnable{\plainenv'} = \scombtwo{\tyenv_1}{\tyenv_2}$
\item $\tyenv_1 = \scombtwo{\tyenv_3}{\tyenv_4}$
\end{itemize}

so, $\makereturnable{\plainenv'} = (\scombtwo{\tyenv_3}{\tyenv_4}) \scomb \tyenv_2$.

By Lemma~\ref{lem:scomb-assoc},
$\makereturnable{\plainenv'} = {\tyenv_3} \scomb ({\tyenv_4} \scomb
\tyenv_2)$.

\begin{mathpar}
\inferrule
\inferrule
{\tyenv_3} \scomb ({\tyenv_4} \scomb \tyenv_2) =
\makereturnable{\plainenv'} \\
\tseq{\tyenv_3}{\tma}{\makereturnable{\pretya}}
\\
\inferrule
\tseq{\tyenv_4, x : \makereturnable{\pretya}}{\tmb}{\tyb} \\
\stackseq{\tyenv_2}{\tyb}{\framestack}
{ \stackseq
\cseq
\cseq
\end{mathpar}
\end{proofcase}

\begin{proofcase}{E-Return}

\begin{mathpar}
\inferrule
\scombtwo{\tyenv_1}{\tyenv_2} = \makereturnable{\plainenv}
\\
\tseq{\tyenv_1}{V}{\tya}
\\
\returnablepred{\tya}
\\
\inferrule
\tyenv_2 = \scombtwo{\tyenv_3}{\tyenv_4} \\\\
\tseq{\tyenv_3, x : \tya}{M}{\tyb} \\
\stackseq{\tyenv_4}{\tyb}{\framestack}
{ \stackseq{\tyenv_2}{\tya}{\frameconcat{\fframe{x}{M}}{\framestack} } }
\cseq
\thread
\end{mathpar}

\begin{itemize}
\item $\makereturnable{\plainenv} = \scombtwo{\tyenv_1}{\tyenv_2}$
\item $\tyenv_2 = \scombtwo{\tyenv_3}{\tyenv_4}$
\end{itemize}
so, $\makereturnable{\plainenv} = \tyenv_1 \scomb (\scombtwo{\tyenv_3}{\tyenv_4})$.

By Lemma~\ref{lem:disjoint-from-cruft}, we have that there exist
$\tyenvb_1, \tyenvb_2, \tyenvb_3$ such that:

\begin{itemize}
\item $\tyenv_1 = \tyenvb_1, \tyenvb_2$
\item $\tseq{\tyenvb_3}{\vala}{\tya'}$
\item $\tyenvb_1$ is cruftless for $\vala$, and $\tyenvb_1 \strictsubty \tyenvb_3$
\item $\tya' \subtype \tya$
\item $\cruftpred{\tyenvb_2}$
\end{itemize}

By Lemma~\ref{lem:returnable-subtype}, $\returnablepred{\tya'}$, and
by Lemma~\ref{lem:returnable-val-env}, $\returnablepred{\tyenvb_3}$.

By Corollary~\ref{cor:returnable-subtype-env},

By Lemma~\ref{lem:substitution},
{\tyenvb_1 + \tyenv_3}
{\tma \{ \vala / x \}}

Equational reasoning on environments:
\[
\bl
\makereturnable{\plainenv} \\
\quad = (\text{expanding}) \\
\scombtwo{\tyenv_1}{\tyenv_2} \\
\quad = (\text{expanding}) \\
\scombtwo{\tyenv_1}{(\scombtwo{\tyenv_3}{\tyenv_4})} \\
\quad = (\text{expanding}) \\
\tyenvb_1, \tyenvb_2 \scomb (\scombtwo{\tyenv_3}{\tyenv_4}) \\
\quad = (\text{Lemma~\ref{lem:scomb-assoc}}) \\
(\tyenvb_1, \tyenvb_2 \scomb \tyenv_3) \scomb \tyenv_4 \\
\quad = (\text{Lemma~\ref{lem:returnable-non-aliased}}) \\
(\tyenvb_1 + (\tyenvb_2 \scomb \tyenv_3)) \scomb \tyenv_4
\el
\]

Let $\plainenv' =
\strip{(\tyenvb_1 + (\tyenvb_2 \scomb \tyenv_3)) \scomb \tyenv_4}$.

By the definitions of environment subtyping,
follows that
$\tyenvb_1 + (\tyenvb_2 \scomb \tyenv_3) \subtype \tyenvb_1 + \tyenv_3$.

\begin{mathpar}
\inferrule*
\inferrule*
(\tyenvb_1 + (\tyenvb_2 \scomb \tyenv_3)) \scomb
\tyenv_4 = \makereturnable{\plainenv'} \\
\inferrule*
\tseq{\tyenvb_1 + \tyenv_3}{M \{ V / x \}}{\tyb}
\tseq{\tyenvb_1 + (\tyenvb_2 \scomb \tyenv_3)}{M \{ V / x \}}{\tyb}
\\
\stackseq{\tyenv_4}{\tyb}{\framestack}
\cseq
{\thread{M \{ V / x \}}{\framestack} }
\cseq{\plainenv}{\thread{M \{ V / x \}}{\framestack} }
\end{mathpar}

as required.
\end{proofcase}

\begin{proofcase}{E-App}

\begin{mathpar}
\inferrule*
\makereturnable{\plainenv} = \tyenv_1 \scomb \tyenv_2 \\
\inferrule*
\inferrule*
\prog(f) = \tyfun{\seq{\tya}}{\tyb} \\
{ \tseq{\tyenv'_1 + \cdots + \tyenv'_n}{\fnapp{f}{\seq{V}}}{\tyb}} \\
{ \tseq{\tyenv_1}{\fnapp{f}{\seq{V}}}{\tyb}} \\
\stackseq{\tyenv_2}{\tyb}{\framestack}
{ \cseq{\plainenv}{\thread{\fnapp{f}{\seq{V}}}{\framestack}} }
\end{mathpar}

Since we also assume $\progseq{\prog}$, we know by definition typing that:

\begin{mathpar}
\inferrule
\tseq[\prog]{\seq{x : \tya}}{\tma}{\tyb}
{ \defseq[\prog]{\fndef{f}{\seq{x : \tya}}{\tyb}{\tma}} }
\end{mathpar}

By Lemma~\ref{lem:substitution} we have that $\tseq{\tyenv'_1 + \cdots +
\tyenv'_n}{\tma \{ \seq{V} / \seq{x} \}}{\tyb}$.

Thus we can recompose:

\begin{mathpar}
\inferrule*
\makereturnable{\plainenv} = \tyenv_1 \scomb \tyenv_2 \\
\inferrule*
{ \tseq{\tyenv'_1 + \cdots + \tyenv'_n}{\tma \{ \seq{V} / \seq{x}\}}{\tyb} }
{ \tseq{\tyenv_1}{\tma \{ \seq{V} / \seq{x}\}}{\tyb} } \\
\stackseq{\tyenv_2}{\tyb}{\framestack}
{ \cseq{\plainenv}{\thread{\tma \{ \seq{V} / \seq{x}\}}{\framestack}} }
\end{mathpar}

as required.
\end{proofcase}

\begin{proofcase}{E-New}

\begin{mathpar}
\inferrule*
\inferrule
\scombtwo{\tyenv_1}{\tyenv_2} = \makereturnable{\plainenv'} \\
\inferrule
\inferrule
{ }
{ \tseq{\cdot}{\mbnew}{\retty{\mbrecvone}} }
{ \tseq{\tyenv_1}{\mbnew}{\retty{\mbrecvone}} }
\\
\stackseq{\tyenv_2}{\retty{\mbrecvone}}{\framestack}
{ \cseq{\plainenv'}{\thread{\mbnew}{\framestack}} }
{ \cseq{\plainenv}{\thread{\mbnew}{\framestack}} }
\end{mathpar}

where $\plainenv \subtype \plainenv'$.

\begin{mathpar}
\inferrule*
\inferrule*
\inferrule
\scombtwo{\tyenv_1, a : \retty{\mbrecvone}}{\tyenv_2} = \makereturnable{\plainenv', a : \mbrecvone} \\
\inferrule
\inferrule
{ }
{ \tseq{a : \retty{\mbrecvone}}{a}{\retty{\mbrecvone}} }
{ \tseq{\tyenv_1, a : \mbrecvone}{a}{\retty{\mbrecvone}} }
\\
\stackseq{\tyenv_2}{\retty{\mbrecvone}}{\framestack}
{ \cseq{\plainenv', a : \mbrecvone}{\thread{a}{\framestack}} }
\cseq{\plainenv'}{(\nu a)(\thread{a}{\framestack})}
{ \cseq{\plainenv}{(\nu a)(\thread{a}{\framestack})} }
\end{mathpar}

as required.
\end{proofcase}

\begin{proofcase}{E-Send}

\begin{mathpar}
\inferrule
\inferrule*
\tyenv_1 \scomb \tyenv_2 = \makereturnable{\plainenv}
\\
\tseq{\tyenv_1}{\send{a}{m}{\seq{V}}}{\one}
\\
\stackseq{\tyenv_2}{\one}{\framestack}
{ \cseq{\plainenv'}{\thread{\send{a}{m}{\seq{V}}}{\framestack}} }
{ \cseq{\plainenv}{\thread{\send{a}{m}{\seq{V}}}{\framestack}} }
\end{mathpar}

By Lemma~\ref{lem:disjoint-from-cruft} we have that:
\begin{itemize}
\item $\tyenv_1 = \tyenvb_1, \tyenvb_2$
\item $\tseq{\tyenvb_3}{\send{a}{m}{\seq{V}}}{\one}$
\item $\tyenvb_1$ is cruftless for $\send{a}{m}{\seq{V}}$
and $\tyenvb_1\strictsubty \tyenvb_3$
\item $\cruftpred{\tyenvb_2}$
\end{itemize}

Therefore we have that $\tyenvb_3 = \tyenvb'_3, a : \tysendm$ such

\begin{mathpar}
\inferrule*
\vseq{a : \usablety{\tysendm}}{a}{\tysendm} \\
\vseq{\tyenvb'_3}{\seq{V}}{\seq{\tya}} \\
\seq{\tya} \subtype \prog(\msgtag{m})
{ \tseq{\tyenvb'_3, a : \usablety{\tysendm}}{\send{a}{m}{\seq{V}}}{\one} }
\end{mathpar}

\[
\bl
\plainenv' \\
\quad = \text{(expanding)} \\
\strip{\tyenv_1 \scomb \tyenv_2} \\
\quad = \text{(expanding)} \\
\strip{(\tyenvb_1, \tyenvb_2) \scomb \tyenv_2} \\
\quad = \text{(expanding)} \\
\strip{(\tyenvb'_1, a : \usablety{\tysendm}, \tyenvb_2) \scomb \tyenv_2} \\
\quad = \text{(Lemma~\ref{lem:disjoint-scomb})} \\
\strip{(\tyenvb'_1, a : \usablety{\tysendm} \scomb \tyenvb_2) \scomb \tyenv_2} \\
\quad = \text{(Lemma~\ref{lem:scomb-env-assoc})}\\
\strip{\tyenvb'_1, a : \usablety{\tysendm} \scomb (\tyenvb_2 \scomb \tyenv_2)} \\
\quad = \text{(Lemma~\ref{lem:scomb-to-pcomb})} \\
\strip{\tyenvb'_1, a : \usablety{\tysendm}} \pcomb \strip{(\tyenvb_2 \scomb \tyenv_2)} \\
\quad = \text{($\pcomb$ is commutative)} \\
\strip{\tyenvb_2 \scomb \tyenv_2} \pcomb \strip{\tyenvb'_1, a :
\usablety{\tysendm}} \\
\el
\]

\begin{mathpar}
\inferrule*
\inferrule*
\inferrule*
\tyenvb_2 \scomb \tyenv_2 =
\makereturnable{
\strip{\tyenvb_2 \scomb \tyenv_2}
\\
\vseq{\tyenvb_2}{()}{\one}
\\
\stackseq{\tyenv_2}{\one}{\framestack}
{ \cseq{\strip{\tyenvb_2 \scomb \tyenv_2}}{\thread{()}{\framestack}} }
\\
\inferrule*
\vseq{a : \tysendm}{a}{\tysendm} \\
\vseq{\makeusable{\tyenvb'_1}}{\seq{V}}{\seq{\tya}} \\
\seq{\tya} \subtype \makeusable{\prog(\msgtag{m})}
\cseq{\strip{\tyenvb'_1, a : \tysendm}}{\sentmsg{a}{m}{\seq{V}}}
\cseq
\strip{\tyenvb_2 \scomb \tyenv_2} \pcomb \strip{\tyenvb'_1, a : \tysendm}
\parallel
\sentmsg{a}{m}{\seq{V}}}
{ \cseq{\plainenv}{\thread{()}{\framestack}
\parallel
\sentmsg{a}{m}{\seq{V}}}
\end{mathpar}

as required.
\end{proofcase}

\begin{proofcase}{E-Spawn}

\begin{mathpar}
\inferrule*
\inferrule
\scombtwo{\makeusable{\tyenv_1}}{\tyenv_2} = \makereturnable{\plainenv'} \\
\inferrule
\inferrule
{ \tseq{\tyenv'_1}{M}{\one} }
{ \tseq{\tyenv_1}{M}{\one} }
{ \tseq{\makeusable{\tyenv_1}}{\spawn{M}}{\one} }
\\
\stackseq{\tyenv_2}{\one}{\framestack}
{ \cseq{\plainenv'}{\thread{\spawn{M}}{\framestack}} }
{ \cseq{\plainenv}{\thread{\spawn{M}}{\framestack}} }
\end{mathpar}

where $\tyenv_1 \subtype \tyenv'_1$.

By Lemma~\ref{lem:disjoint-from-cruft}, there exist $\tyenvb_1,
\tyenvb_2, \tyenvb_3$ such that:

\begin{itemize}
\item $\tyenv_1 = \tyenvb_1, \tyenvb_2$
\item $\tseq{\tyenvb_3}{M}{\one}$
\item $\tyenvb_1$ is cruftless for $\tma$ and $\tyenvb_1 \strictsubty \tyenvb_3$
\item $\cruftpred{\tyenvb_2}$
\end{itemize}

We now prove that
$\plainenv' \subtype \strip{\tyenvb_2 \scomb \tyenv_2} \pcomb \strip{\tyenvb_1}$.

\[
\bl
\plainenv' \\
\quad = \text{(expanding)} \\
\strip{\makeusable{\tyenv_1} \scomb \tyenv_2} \\
\quad = \text{(expanding)} \\
\strip{\makeusable{\tyenvb_1, \tyenvb_2} \scomb \tyenv_2} \\
\quad = \text{($\tyenvb_2$ cruft, so usable)} \\
\strip{(\makeusable{\tyenvb_1}, \tyenvb_2) \scomb \tyenv_2} \\
\quad = \text{(Lemma~\ref{lem:disjoint-scomb})} \\
\strip{(\makeusable{\tyenvb_1} \scomb \tyenvb_2) \scomb \tyenv_2} \\
\quad = \text{(Lemma~\ref{lem:scomb-env-assoc})} \\
\strip{\makeusable{\tyenvb_1} \scomb (\tyenvb_2 \scomb \tyenv_2)} \\
\quad = \text{(Lemma~\ref{lem:scomb-to-pcomb})} \\
\strip{\makeusable{\tyenvb_1}} \pcomb \strip{(\tyenvb_2 \scomb \tyenv_2)} \\
\quad = \text{($\pcomb$ is commutative)} \\
\strip{(\tyenvb_2 \scomb \tyenv_2)} \pcomb \strip{\makeusable{\tyenvb_1}}  \\
\quad = \text{($\strip{-}$ cancels $\makeusable{-}$)} \\
\strip{(\tyenvb_2 \scomb \tyenv_2)} \pcomb \strip{\tyenvb_1}
\el
\]

It follows that since $\returnable \subtype \usable$ and
$\tyenvb_1 \strictsubty \tyenvb_3$, that
$\makereturnable{\tyenvb_1} \subtype \tyenvb_3$.

From that, we can construct the following derivation:
\begin{mathpar}
\inferrule*
\inferrule*
\inferrule
\inferrule
\scombtwo{\tyenvb_2}{\tyenv_2} =
\makereturnable{\strip{\scombtwo{\tyenvb_2}{\tyenv_2}}}
\\
\inferrule*
{ \tseq{\cdot}{()}{\one} }
{ \tseq{\tyenvb_2}{()}{\one} }
\\
\stackseq{\tyenv_2}{\one}{\framestack}
\cseq{\strip{\scombtwo{\tyenvb_2}{\tyenv_2}}}{\thread{()}{\framestack}}
\\
\inferrule
\scombtwo{\makereturnable{\strip{\tyenvb_1}}}{\cdot} =
\makereturnable{\strip{\tyenvb_1}} \\
\inferrule
\tseq{\tyenvb_3}{M}{\one}
{ \tseq{\makereturnable{\tyenvb_1}}{M}{\one} }
\\
\inferrule
{ }
{ \stackseq{\cdot}{\one}{\emptystack} }
{ \cseq{\strip{\tyenvb_1}}{\thread{M}{\emptystack}} }
{ \cseq
{\strip{\scombtwo{\tyenvb_2}{\tyenv_2}} \pcomb
\strip{\tyenvb_1}}
{\thread{()}{\framestack} \parallel \thread{M}{\emptystack}}
{ \cseq{\plainenv'}{\thread{()}{\framestack} \parallel \thread{M}{\emptystack}} }
{ \cseq{\plainenv}{\thread{()}{\framestack} \parallel \thread{M}{\emptystack}} }
\end{mathpar}

as required.
\end{proofcase}

\begin{proofcase}{E-Free}

Assumption (assuming WLOG that the $\calcwd{free}$ guard is the first
guard in the sequence):

\begin{mathpar}
\inferrule*
\inferrule*
\inferrule*
\tyenv_1, a : \retty{\tyrecv{\patb_{\var{env}}}} \scomb \tyenv_2 =
\makereturnable{\plainenv', a : \retty{\tyrecv{\patb_{\var{env}}}}} \\
\tseq{\tyenv_1, a :
\retty{\tyrecv{\patb_{\mathit{env}}}}}{\guardann{a}{\pata}{\free{\tma} \cdot \seq{G}}}{\tya}
\\
\stackseq{\tyenv_2}{\tya}{\framestack}
{ \cseq{\plainenv', a :
\tyrecv{\patb_{\var{env}}}}{\thread{\guardann{a}{\pata}{\free{\tma} \cdot \seq{G}}}{\framestack}} }
{ \cseq{\plainenv, a : \mbrecvone}{\thread{\guardann{a}{\pata}{\free{\tma} \cdot \seq{G}}}{\framestack}} }
{ \cseq{\plainenv}{\resconf{a}{\thread{\guardann{a}{\pata}{\free{\tma} \cdot \seq{G}}}{\framestack}}} }
\end{mathpar}

where $\plainenv \subtype \plainenv'$, and $\mbrecvone \subtype
\tyrecv{\patb}$, and (by Lemma~\ref{lem:returnable-non-aliased}) $a \not\in
\dom{\tyenv_2}$.

\begin{mathpar}
\inferrule*
\inferrule*
\tseq{\tyenvb_1, a : \retty{\tyrecv{\patb{'}_{\var{env}}}}}{a}{\tyrecvp{\mbone \patplus \patb'}} \\
\inferrule*
\inferrule*
{ \tseq{\tyenvb_2}{\tma}{\tya} }
{ \gseq{\mbone}{\tyenvb_2}{\free{\tma}}{\tya} } \\
\gseq{\patb'}{\tyenvb_2}{\tma}{\tya}
{ \gseq{\mbone \patplus \patb'}{\tyenvb_2}{\free{\tma} \cdot \seq{G}}{\tya} }
\tseq
{\tyenvb_1, a : \retty{\tyrecv{\patb{'}_{\var{env}}}} + \tyenvb_2}
{\guardann{a}{\pata}{\free{\tma} \cdot \seq{G}}}
{ \tseq
{\tyenv_1, a :
\retty{\tyrecv{\patb_{\var{env}}}}}
{\guardann{a}{\pata}{\free{\tma} \cdot \seq{G}}}
\end{mathpar}

where $\cruftpred{\tyenvb_1}$.
Thus, $\tyenvb_1 + \tyenvb_2 \subtype
\tyenvb_2$ and $\tseq{\tyenvb_1 + \tyenvb_2}{\tma}{\tya}$. Furthermore,
$\tyenv_1 \subtype \tyenvb_1 + \tyenvb_2$.

Thus, recomposing:

\begin{mathpar}
\inferrule*
\inferrule*
\tyenv_1 \scomb \tyenv_2 = \makereturnable{\plainenv'} \\
\inferrule*
\tseq{\tyenvb_1 + \tyenvb_2}{\tma}{\tya}
{ \tseq{\tyenv_1}{\free{\tma}}{\tya} }
\\
\stackseq{\tyenv_2}{\tya}{\framestack}
{ \cseq{\plainenv'}{\thread{\tma}{\framestack}} }
{ \cseq{\plainenv}{\thread{\tma}{\framestack}} }
\end{mathpar}

as required.
\end{proofcase}

\begin{proofcase}{E-Recv}

\begin{mathpar}
\inferrule*
\inferrule*
\inferrule*
\scombtwo{\tyenv_1}{\tyenv_2} = \makereturnable{\plainenv_1} \\
\deriv{D} \\
\stackseq{\tyenv_2}{\tya}{\framestack}
{ \cseq
\thread
\\
\inferrule*
\tseq{\makeusable{\plainenv_2}}{\seq{V}}{\seq{\tyb}} \\
\seq{\pretyb} \subtype \makeusable{\prog(\msgtag{m})}
{ \cseq{\plainenv_2, a : \tysend{\msgtag{m}}}{\sentmsg{a}{m}{\seq{V}}} }
\cseq
{ \pcombtwo{\plainenv_1}{(\plainenv_2, a : \tysend{\msgtag{m}})} }
\thread
\parallel
\sentmsg{a}{m}{\seq{V}}
\cseq
{ \plainenv }
\thread
\parallel
\sentmsg{a}{m}{\seq{V}}
\end{mathpar}

where $\deriv{D}$ is the following derivation:
\begin{mathpar}
\inferrule*
\tyenv_1 = \tyenv_3 + \tyenv_4 \\
\inferrule*
{ \vseq{a : \retty{\tyrecv{\pata}}}{a}{\retty{\tyrecv{\pata}}} }
{ \vseq{\tyenv_3}{a}{\retty{\tyrecv{\pata_{\mathit{ty}}}}} } \\
\gseq
\\
\pata_{\mathit{ty}} \subpatone {\pata_{\var{ann}}} \\
\pnf{\pata_{\mathit{ty}}}
{ \tseq{\tyenv_1}{\guard{a}{\pata_{\var{ann}}}{\ctx{G}[\receive{m}{\seq{x}}{y}{M}]}}{\tya} }
\end{mathpar}

By Lemma~\ref{lem:disjoint-from-cruft},
$\tyenv_3 = \tyenvb, a : \retty{\tyrecv{\pata_{\mathit{env}}}}$,
\begin{itemize}
\item $\tyrecv{\pata_{\mathit{env}}} \subtype \tyrecv{\pata}$
\item $\tyrecv{\pata} \subtype \tyrecv{\pata_{\mathit{ty}}}$
\end{itemize}
and thus
$\tyrecv{\pata_{\mathit{env}}} \subtype \tyrecv{\pata} \subtype
\tyrecv{\pata_{\mathit{ty}}}$.

Without loss of generality, let us consider the case where the
$\calcwd{receive}$ is the first guard.
We can therefore write $\ctx{G}[\receive{m}{\seq{x}}{y}{M}]$ as
$\receive{m}{\seq{x}}{y}{M} \cdot \seq{G}$ for some sequence $\seq{G}$.

By \textsc{T-GuardSeq} and \textsc{TG-Recv}, and since
$\pnf{\pata_{\mathit{ty}}}$, we have that $\pata_{\mathit{ty}} = \patb_1
\patplus \cdots \patplus \patb_n$, where $\patb_1 = \msgtag{m} \patconcat
\patb'$ and $\patb' \tyequiv \pata_{\mathit{ty}} \without \msgtag{m}$.

\begin{mathpar}
\inferrule
\prog(\msgtag{m}) = \seq{\pretyb'} \\
\un{\tyenv_4} \\
\tseq
{\tyenv_4, \seq{x} : \seq{\makeusable{\pretyb'}},
y : \retty{\tyrecv{\patb'}}}
{ \gseq
{(\msgtag{m} \patconcat \patb')}
\end{mathpar}

Now, by the definition of $\pcomb$, we know that $\pata_{\mathit{env}} =
\msgtag{m} \patconcat \pata_{\mathit{pat}}$ for some pattern

By the definition of $\scomb$, we also know that $a \not\in \dom{\tyenv_4}$.

By Lemma~\ref{lem:balancing}, we have that
$\pata_{\mathit{pat}} \incll[] \pata \without \msgtag{m}$, and thus
$\retty{\tyrecv{\pata_{\mathit{pat}}}} \subtype
\retty{\tyrecvp{\pata \without \msgtag{m}}}$.

Further, it follows that $\tyrecv{\pata \without \msgtag{m}} \subtype
\tyrecv{\patb'}$.

By Lemma~\ref{lem:substitution},
$\tseq{\makeusable{\plainenv_2} + \tyenv_4, a : \retty{\tyrecv{\patb'}}}{\tma \{ \seq{V} / \seq{x}, a / y \}}{\tya}$.

Equational reasoning:
\[
\bl
\plainenv_1 \pcomb (\plainenv_2, a : \tysend{\msgtag{m}}) \\
\quad = \text{(expanding)} \\
\strip{\tyenv_1 \scomb \tyenv_2} \pcomb (\plainenv_2, a : \tysend{\msgtag{m}}) \\
\quad = \text{(expanding)} \\
\strip{(\tyenv_3 + \tyenv_4) \scomb \tyenv_2} \pcomb (\plainenv_2, a : \tysend{\msgtag{m}}) \\
\quad = \text{(expanding)} \\
\strip{(\tyenvb, a : \retty{\tyrecv{\pata_{\mathit{env}}}} + \tyenv_4) \scomb \tyenv_2} \pcomb (\plainenv_2, a : \tysend{\msgtag{m}}) \\
\quad = \text{(expanding)} \\
\strip{(\tyenvb, a : \retty{\tyrecvp{ \msgtag{m} \patconcat \pata_{\mathit{pat}} }} + \tyenv_4) \scomb \tyenv_2} \pcomb (\plainenv_2, a : \tysend{\msgtag{m}}) \\
\quad = \text{(Lemma~\ref{lem:returnable-non-aliased})} \\
\strip{(\tyenvb + \tyenv_4) \scomb \tyenv_2, a : \retty{\tyrecvp{ \msgtag{m} \patconcat \pata_{\mathit{pat}}}}}
\pcomb (\plainenv_2, a : \tysend{\msgtag{m}}) \\
\quad = \text{(Definition of $\pcomb$)} \\
(\strip{(\tyenvb + \tyenv_4) \scomb \tyenv_2} \pcomb \plainenv_2), a : \tyrecv{\pata_{\mathit{pat}}} \\
\quad = \text{(Lemma~\ref{lem:pcomb-to-scomb}, since $\un{\tyenv_4}$)} \\
(\strip{\makeusable{\plainenv_2} \scomb ((\tyenvb + \tyenv_4) \scomb \tyenv_2)}), a : \tyrecv{\pata_{\mathit{pat}}} \\
\quad = \text{(Lemma~\ref{lem:scomb-assoc})} \\
(\strip{(\makeusable{\plainenv_2} \scomb (\tyenvb + \tyenv_4)) \scomb \tyenv_2}), a : \tyrecv{\pata_{\mathit{pat}}} \\
\quad = \text{(Lemma~\ref{lem:scomb-plus-defined})} \\
(\strip{(\makeusable{\plainenv_2} + (\tyenvb + \tyenv_4)) \scomb \tyenv_2}), a : \tyrecv{\pata_{\mathit{pat}}} \\
\quad = \text{($a$ disjoint from environments)} \\
\strip{(\makeusable{\plainenv_2} + (\tyenvb + \tyenv_4), a : \retty{\tyrecv{\pata_{\mathit{pat}}}} ) \scomb \tyenv_2}
\el
\]

Let $\plainenv' =
\strip{(\makeusable{\plainenv_2} + (\tyenvb + \tyenv_4), a : \retty{\tyrecv{\pata_{\mathit{pat}}}} ) \scomb \tyenv_2}

\begin{mathpar}
\inferrule*
\inferrule*
\makereturnable{\plainenv}
\scombtwo
\makeusable{\plainenv_2} + (\tyenvb + \tyenv_4), a : \retty{\tyrecv{\pata_{\mathit{pat}}}}
{ \tyenv_2 }
\\
\tseq
{\makeusable{\plainenv_2} + \tyenv_4, a : \retty{\tyrecv{\patb'}}}
{M \{ \seq{V} / \seq{x}, a / y \}}
\\
\stackseq{\tyenv_2}{\tya}{\framestack}
{ \cseq{\plainenv'}{\thread{M \{ \seq{V} / \seq{x}, a / y \}}{\framestack}} }
{ \cseq{
\plainenv
}{\thread{M \{ \seq{V} / \seq{x}, a / y \}}{\framestack}} }
\end{mathpar}

as required.
\end{proofcase}

\begin{proofcase}{E-Nu}
Follows immediately from the induction hypothesis.
\end{proofcase}

\begin{proofcase}{E-Par}
Follows immediately from the induction hypothesis.
\end{proofcase}

\begin{proofcase}{E-Struct}
Follows immediately from Lemma~\ref{lem:equiv-pres} and the induction
\end{proofcase}
\end{proof}

\newpage
\subsection{Progress}

\begin{lemma}[Canonical forms]
If $\cseq{\cdot}{\config{C}}$ then there exists some $\config{D}$ such that
$\config{C} \equiv \config{D}$ and $\config{D}$ is in canonical form.
\end{lemma}
\begin{proof}
Follows from the structural congruence rules.
\end{proof}

\begin{lemma}[Progress (Thread Reduction)]\label{lem:thread-progress}
If $\cseq[\prog]{\tyenv}{\thread{\tma}{\framestack}}$, then either:
\begin{itemize}
\item $\tma$ is a value and $\framestack = \emptystack$; or
\item there exists some $\tma', \framestack'$ such that $\thread{\tma}{\framestack} \ceval
\thread{\tma'}{\framestack'}$; or
\item $\tma$ is a communication and concurrency construct, \ie\ $\mbnew$, or
$\spawn{\tma}$, or \\$\send{\vala}{m}{\seq{\valb}}$, or $\guardann{\vala}{\pata}{\seq{\gd}}$.
\end{itemize}
\end{lemma}
\begin{proof}
By case analysis on the derivation of
$\cseq{\tyenv}{\thread{\tma}}{\framestack}$ and inspection of the reduction
\end{proof}

\progress*
\begin{proof}
Functional reduction enjoys progress~(\ref{lem:thread-progress}), and the
$\mbnew$, $\spawn{\tma}$, and $\send{a}{m}{\seq{V}}$ can all always reduce.
Therefore, the body of an irreducible thread
$\thread{\tma_k}{\framestack_k}$ must be waiting for a message $\msgtag{m}$ on
some name $a$.
To be waiting, name $a$ must be
returnable, and therefore cannot occur free in $\tma_k$ or $\framestack_k$.
It cannot be the case that message $\msgtag{m}$ for $a$ is
contained in $\msgset$ (in which case the configuration could reduce), so
typing ensures that $a$ is free in one of the other threads. Extending this
reasoning we see that if a configuration contains irreducible non-value
threads, then $\config{C}$ must contain a cyclic inter-thread dependency.
\end{proof}

\newpage
\subsection{Algorithmic Soundness}
\label{sec:soundness}

A solution for a set of constraints is also a solution for a subset of those

\begin{lemma}
\label{lem:pat-subset}
If $\patsubst$ is a solution for a constraint set
$\constrs_1 \cup \constrs_2$,
then $\patsubst$ is a solution for $\constrs_1$.
\end{lemma}
\begin{proof}
Since $\patsubst$ is a solution for $\constrs_1 \cup \constrs_2$,
it follows that $\dom{\constrs_1 \cup \constrs_2} \subseteq \dom{\patsubst}$.
The result follows from the fact that $\dom{\constrs_1} \subseteq
\dom{\constrs_1 \cup \constrs_2} \subseteq \dom{\patsubst}$.
\end{proof}

The pattern variables in an inferred environment must either occur in the type,
program, or constraint set.

\begin{lemma}\label{lem:penv-constrs-subset}
If $\synthseq[\prog]{\tma}{\ptya}{\penv}{\constrs}$ or
then $\pv{\penv} \subseteq \pv{\ptya} \cup \pv{\prog} \cup \pv{\constrs}$.
\end{lemma}
\begin{proof}
By mutual induction on the two derivations, noting that whenever a pattern
variable is introduced fresh, it is always added to the constraint set.
\end{proof}

Application of a usable substitution preserves algorithmic subtyping
in the declarative setting.

\begin{lemma}
\label{lem:subtype-soundness}
If $\subtyseq{\ptya}{\ptyb}{\constrs}$ and
$\patsubst$ is a usable solution of $\constrs$ with $\pv{\ptyb} \subseteq
\dom{\patsubst}$,
then $\subtypetwo{\apppatsubst{\ptya}}{\apppatsubst{\ptyb}}$.
\end{lemma}
\begin{proof}
By case analysis on the derivation of $\subtyseq{\ptya}{\ptyb}{\constrs}$.
\end{proof}

As a direct corollary, we can show that constraints generated by equivalence
preserve subtyping in both directions.

\begin{corollary}
\label{lem:equiv-soundness}
$\equivseq{\ptya}{\ptyb}{\constrs}$ and
$\patsubst$ is a usable solution of $\constrs$ with $\pv{\ptyb} \subseteq
\dom{\patsubst}$,
then both
$\subtypetwo{\apppatsubst{\ptya}}{\apppatsubst{\ptyb}}$ and
\end{corollary}

Similarly, application of a usable substitution preserves unrestrictedness.

\begin{lemma}
\label{lem:unr-soundness}
If $\unrseq{\ptya}{\constrs}$ and $\patsubst$ is a usable solution of
$\constrs$ with $\pv{\ptyb} \subseteq \dom{\patsubst}$, then
there exists some $\tya$ such that $\un{\tya}$ and $\tya \subtype \apppatsubst{\ptya}$.
\end{lemma}
\begin{proof}
By case analysis on the derivation of $\unrseq{\ptya}{\constrs}$, noting
that cases are undefined for linear types, and the result follows
straightforwardly for base types.

The only interesting case is
$\unrseq{\usablety{\tysend{\ppata}}}{\subpatconstr{\mbone}{\ppata}}$; since $\patsubst$
is a usable solution, we have that $\mbone \subpatone
\apppatsubst{\ppata}$ and $\aps{\ppata} \not\incll \mbzero$.

Thus, it follows that $\aps{\ppata} \tyequiv \mbone$ and therefore
$\tysend{\mbone} \subtype \aps{\ppata}$, noting that $\un{\tysend{\mbone}}$
as required.
\end{proof}

Again, this is straightforward to extend to environments.

\begin{corollary}
\label{cor:unr-env-soundness}
If $\patsubst$ is a usable solution of $\unrseq{\penv}{\constrs}$
where $\pv{\penv} \subseteq \dom{\patsubst}$, then
there exists some $\tyenv$ such that $\tyenv \subtype \aps{\penv}$ and
\end{corollary}

If two environments are combinable, and we have a solution for the constraints
generated by their algorithmic combination, then their combination is defined.

\begin{lemma}
\label{lem:combine-sol}
If $\combineseq{\penv_1}{\penv_2}{\penv}{\constrs}$ and
$\patsubst$ is a usable solution of $\constrs$
where $\pv{\penv_1} \cup \pv{\penv_2} \subseteq \dom{\patsubst}$,
then there exists some $\tyenv$
such that $\tyenv \subtype \apppatsubst{\penv_2}$ and
$\apppatsubst{\penv_1} + \tyenv = \apppatsubst{\penv}$.
\end{lemma}
\begin{proof}
By induction on the derivation of

\begin{proofcase}{$\combineseq{\penv_1, x : \ptya}{\penv_2}{\penv}{\constrs}$}

\begin{mathpar}
\inferrule
x \not\in \dom{\penv_2} \\
\combineseq{\penv_1}{\penv_2}{\penv}{\constrs}
{ \combineseq{\penv_1, x : \ptya}{\penv_2}{\penv, x : \ptya}{\constrs} }
\end{mathpar}

We also assume that $\patsubst$ is a usable solution for $\constrs$.

By the IH, we have that there exists some $\tyenv \subtype
\apppatsubst{\penv_2}$ such that
$\apppatsubst{\penv_1} + \tyenv = \apppatsubst{\penv}$.

Since $x \not\in \dom{\penv_2}$, by the definition of $+$ in the declarative
setting, we have that
\[
\apppatsubst{\penv_1}, x : \apppatsubst{\ptya} + \apppatsubst{\penv_2}
\subtype
\apppatsubst{\penv}, x : \apppatsubst{\ptya}
\]
as required.
\end{proofcase}

\begin{proofcase}{$\combineseq{\penv_1}{\penv_2, x : \ptya}{\penv}{\constrs}$}
Symmetric to the first case.
\end{proofcase}

\begin{proofcase}
{$\combineseq{\penv_1, x : \ptya}{\penv_2, x : \ptyb}{\penv}{\constrs}$}

\begin{mathpar}
\inferrule
\combineseq{\penv_1}{\penv_2}{\penv}{\constrs_1} \\
\equivseq{\ptya}{\ptyb}{\constrs_2} \\\\
\unrseq{\ptya}{\constrs_3} \\
\unrseq{\ptyb}{\constrs_4}
{ \combineseq
{\penv_1, x : \ptya}
{\penv_2, x : \ptyb}
{\penv, x : \ptya}
{\constrs_1 \cup \cdots \cup \constrs_4}
\end{mathpar}

We also assume that $\patsubst$ is a usable solution for
$\constrs_1 \cup \cdots \cup \constrs_4$.

By the IH, there exists some $\tyenv$ such that $\tyenv \subtype
\apppatsubst{\penv_2}$ and
\[
\apppatsubst{\penv_1} + \tyenv = \apppatsubst{\penv}
\]

By the definitions of $\equivsymb$ and $\mkwd{unr}(-)$, and knowing that
$\patsubst$ is a usable solution for $\constrs_2 \cup
\constrs_3 \cup \constrs_4$, we have that
either $\ptya = \ptyb = \basety$ for some base type $\basety$ (in which case we can
conclude with logic similar to the previous case),
or $\ptya = \usablety{\tysend{\ppata}}$ and
$\ptyb = \usablety{\tysend{\ppatb}}$ where
$\subpat{\apppatsubst{\ppata}, \apppatsubst{\ppatb}}{\mbone}$.

Since $\patsubst$ is usable, we know that
$\apppatsubst{\ppata}, \apppatsubst{\ppatb} \not\subpatone \mbzero$.
Therefore, we have that $\ptya, \ptyb \subtype
\usablety{\tysend{\mbone}}$.

We can then show that
$\tyenv, x :
\tyenv, x : \apppatsubst{\usablety{\tysend{\ptya}}} \subtype
\apppatsubst{\penv_2}, x : \apppatsubst{\usablety{\tysend{\ptyb}}}$

and further that
$\apppatsubst{\penv_1}, x : \apppatsubst{\usablety{\tysend{\ptya}}} +
\tyenv, x : \apppatsubst{\usablety{\tysend{\ptya}}} =
\apppatsubst{\penv}, x :
\apppatsubst{\usablety{\tysend{\ptya}}}
as required.
\end{proofcase}

\end{proof}

We can generalise the previous result to an $n$-ary combination:

\begin{corollary}\label{cor:combine-many-sol}
If $\combineseqmany{\penv_1 + \ldots + \penv_n}{\penv}{\constrs}$
where $\patsubst$ is a usable solution for $\constrs$ such that
$\pv{\penv_1} \cup \cdots \cup \pv{\penv_n} \subseteq \dom{\patsubst}$,
then there exist $(\tyenv_i \subtype \penv_i)_i$ such that
$\tyenv_1 + \ldots + \tyenv_n = \aps{\penv}$.
\end{corollary}

We now turn our attention to the relation between the algorithmic join and type
combination operators.

\begin{lemma}
\label{lem:scomb-sol}
If $\joinseq{\ptya_1}{\ptya_2}{\ptyb}{\constrs}$
and $\patsubst$ is a usable solution of $\constrs$
such that $\pv{\ptya_1} \cup \pv{\ptya_2} \subseteq \dom{\patsubst}$,
then there exist
$\ptya'_1 \subtype \apppatsubst{\ptya_1}$,
$\ptya'_2 \subtype \apppatsubst{\ptya_2}$
where $\scombtwo{\ptya'_1}{\ptya'_2} = \apppatsubst{\ptyb}$.
\end{lemma}
\begin{proof}
By case analysis on the derivation of

\begin{proofcase}{
{\usageann{\usage_1 \scomb \usage_2}{\tysendp{\patconcattwo{\ppata}{\ppatb}}} }

We can immediately conclude with
\usageann
{\usage_1 \scomb \usage_2}
as required.
\end{proofcase}

\begin{proofcase}

Since $\patsubst$ is a solution for
we have that $\aps{\patconcattwo{\ppata}{\patvara}} \subpatone
\aps{\ppatb}$.

By expansion of $\aps{-}$, we have that
\subpatone
\aps{\ppatb}$.

Since receive mailbox types are covariant in their patterns, we can show
\subtype
\tyrecv{\aps{\ppatb}}$

and we can conclude that
\[
\scombtwo
\usageann{\scombtwo{\usage_1}{\usage_2}}{\tyrecv{\aps{\patvara}}}
\]
as required.
\end{proofcase}

\begin{proofcase}

Symmetric to the previous case.
\end{proofcase}

\begin{proofcase}
\joinseq

Assumption: $\ptya$, $\ptyb$ are not mailbox types and

By Lemma~\ref{lem:subtype-soundness},
Since neither type is a mailbox type we have that $\aps{\ptya} = \ptya =
\ptyb = \aps{\ptyb} = \basety$ for some base type $\basety$, as
\end{proofcase}
\end{proof}

We can extend this result to environments.

\begin{lemma}
\label{lem:scomb-env-sol}
If $\joinseq{\penv_1}{\penv_2}{\penv}{\constrs}$
and $\patsubst$ is a usable solution of $\constrs$
such that $\pv{\penv_1} \cup \pv{\penv_2} \subseteq \dom{\patsubst}$, then there exist
$\tyenv_1 \subtype \apppatsubst{\penv_1}$
$\tyenv_2 \subtype \apppatsubst{\penv_2}$
such that
$\scombtwo{\tyenv_1}{\tyenv_2} = \apppatsubst{\penv}$.
\end{lemma}
\begin{proof}
A direct consequence of Lemma~\ref{lem:scomb-sol}.
\end{proof}

\begin{lemma}
\label{lem:merge-soundness}
and $\patsubst$ is a usable substitution of $\constrs$
such that $\pv{\ptya_1} \cup \pv{\ptya_2} \subseteq \dom{\patsubst}$, then
$\apppatsubst{\ptyb} \subtype \apppatsubst{\ptya_1}$
$\apppatsubst{\ptyb} \subtype \apppatsubst{\ptya_2}$.
\end{lemma}
\begin{proof}
By case analysis on the derivation of

For two mailbox types $\usageann{\usage_1}{\mbtya}$ and
$\usageann{\usage_2}{\mbtya}$, since $\returnable \subtype \usable$
it is always the case that
$\maxusage{\usage_1}{\usage_2} \subtype \usage_1$ and
$\maxusage{\usage_1}{\usage_2} \subtype \usage_2$, so therefore it suffices
to consider the non-usage-annotated merge

\begin{proofcase}{
\mergeseq
{ \tysend{\ppata} }
{ \tysend{\ppatb} }
{ \tysendp{\patplustwo{\ppata}{\ppatb}} }
{ \emptyset}

By appeal to the definition of $\sem{-}$ we have that
$\sem{\patplustwo{\apppatsubst{\ppata}}{\apppatsubst{\ppatb}}} =
\sem{\apppatsubst{\ppata}} \uplus \sem{\apppatsubst{\ppatb}}$ and therefore:
\begin{itemize}
\item ${\sem{\apppatsubst{\ppata}}} \subseteq
{\sem{\patplustwo{\apppatsubst{\ppata}}{\apppatsubst{\ppatb}}}}$; and
\item $\sem{\apppatsubst{\ppatb}} \subseteq
\sem{\patplustwo{\apppatsubst{\ppata}}{\apppatsubst{\ppatb}}}$
\end{itemize}

By the reflexivity of subtyping and the definition of pattern inclusion,
it follows that:

\begin{itemize}
\item ${\apppatsubst{\ppata}} \subpatone
({\patplustwo{\apppatsubst{\ppata}}{\apppatsubst{\ppatb}}})$; and
\item $\apppatsubst{\ppatb} \subpatone
\end{itemize}

Therefore, since output mailbox types are contravariant in their
patterns, it follows that both:

\begin{itemize}
\item $\subtypetwo
{\tysendp{\apppatsubst{\ppata} \patplus \apppatsubst{\ppatb}}}
{\tysendp{\apppatsubst{\ppata}}}$; and
\item $\subtypetwo
{\tysendp{\apppatsubst{\ppata} \patplus \apppatsubst{\ppatb}}}
\end{itemize}
as required.
\end{proofcase}

\begin{proofcase}
\mergeseq
{ \tyrecv{\ppata} }
{ \tyrecv{\ppatb} }
{ \tyrecv{\patvara} }
{ \set
\subpatconstr{\patvara}{\ppata},
\subpatconstr{\patvara}{\ppatb}

(where $\patvara$ fresh).

Since $\patsubst$ is a usable solution, it follows that:
\begin{itemize}
\item $\subpat{\apppatsubst{\patvara}}{\apppatsubst{\ppata}}$; and
\item $\subpat{\apppatsubst{\patvara}}{\apppatsubst{\ppatb}}$
\end{itemize}

Since receive mailbox types are covariant in their pattern arguments, it
follows that:

\begin{itemize}
\item $\tyrecvp{\apppatsubst{\patvara}} \subtype
\tyrecvp{\apppatsubst{\ppata}}$; and
\item $\tyrecvp{\apppatsubst{\patvara}} \subtype
\tyrecvp{\apppatsubst{\ppatb}}$
\end{itemize}

as required.
\end{proofcase}

\begin{proofcase}
{ $\mergeseq
$\ptya, \ptyb$ are not mailbox types and

By Lemma~\ref{lem:equiv-soundness}:
\begin{enumerate}
\item $\apppatsubst{\ptya} \subtype \apppatsubst{\ptyb}$; and
\item $\apppatsubst{\ptyb} \subtype \apppatsubst{\ptya}$.
\end{enumerate}

By the reflexivity of subtyping we have that $\apppatsubst{\ptya}
\subtype \apppatsubst{\ptya}$, and for the second obligation
we can conclude with (2) as required.
\end{proofcase}
\end{proof}

\begin{lemma}
\label{lem:merge-env-sol}
If $\mergeseq{\penv_1}{\penv_2}{\penv}{\constrs}$ and
$\patsubst$ is a usable solution of $\constrs$
such that $\pv{\penv_1} \cup \pv{\penv_2} \subseteq \dom{\patsubst}$,
$\apppatsubst{\penv} \subtype \apppatsubst{\penv_1}$ and
$\apppatsubst{\penv} \subtype \apppatsubst{\penv_2}$.
\end{lemma}
\begin{proof}
By induction on the derivation of
$\mergeseq{\penv_1}{\penv_2}{\penv}{\constrs}$ with appeal to
\end{proof}

\begin{lemma}[Subpattern PNF]\label{lem:subpattern-pnf}
If $\pnftwo{\pata}{\patb}$ and $\subpat{\pata}{\patb}$, then $\pnf{\patb}$.
\end{lemma}
\begin{proof}
For it to be the case that $\pnftwo{\pata}{\patb}$ it must be the case that
$\patb = \patb_1 \patplus \cdots \patplus \patb_n$ where
$\pnflittwo{\pata}{\patb_i}$ for $i \in 1..n$.

It suffices to consider the case where we have some $\patb_j = \msgtag{m}_j
\patconcat \patb'_j$ where $\patb_j \not\subpatone \pata$. In this case, the
following must hold:

\begin{mathpar}
\inferrule*
\patb_j \tyequiv \pata \without \msgtag{m}_j
{ \pnflittwo{\pata}{\msgtag{m}_j \patconcat \patb_j} }
\end{mathpar}

and by the definition of pattern residual and the fact that $\msgtag{m}_j
\not\subpatone \pata$ it must be the case that  $\pata \without \msgtag{m}_j
\tyequiv \mbzero$. Consequently we know that $\patb_j \tyequiv \mbzero$.

To ensure that $\pnf{\patb}$ we need to show $\pnftwo{\patb}{\patb}$ and
therefore that $\mbzero \tyequiv \patb \without \msgtag{m}_j$, which follows
by the definition of pattern derivative as required.
\end{proof}

Algorithmic soundness relies on the following generalised result:

\begin{lemma}[Algorithmic Soundness (Generalised)]
\label{lem:algo-soundness-generalised}
\hfill
\begin{itemize}
\item If $\algoprogseq{\prog}{\constrs_1}$ and
$\synthseq[\prog]{\tma}{\ptya}{\penv}{\constrs_2}$ where $\patsubst$ is a
usable solution of $\constrs_1 \cup \constrs_2$ and
$\pv{\ptya} \cup \pv{\prog} \subseteq \dom{\patsubst}$, then $\tseq
\item If $\algoprogseq{\prog}{\constrs_1}$ and
$\chkseq[\prog]{\tma}{\ptya}{\penv}{\constrs_2}$ where $\patsubst$ is a
usable solution of $\constrs_1 \cup \constrs_2$
and $\pv{\ptya} \cup \pv{\prog} \subseteq \dom{\patsubst}$, then
\item If $\algoprogseq{\prog}{\constrs_1}$
and $\chkgseq[\prog]{\pata}{\gd}{\ptya}{\penv}{\constrs}{\patb}$
$\patsubst$ is a usable solution of $\constrs_1 \cup \constrs_2$
and $\pv{\ptya} \cup \pv{\prog} \subseteq \dom{\patsubst}$, then
{\apppatsubst{\ptya}}$ and
\item If $\algoprogseq{\prog}{\constrs_1}$
and $\chkgseq[\prog]{\pata}{\seq{\gd}}{\ptya}{\penv}{\constrs}{\patb}$
$\patsubst$ is a usable solution of $\constrs_1 \cup \constrs_2$
and $\pv{\ptya} \cup \pv{\prog} \subseteq \dom{\patsubst}$, then
{\apppatsubst{\ptya}}$ and
\end{itemize}

\end{lemma}
\begin{proof}
By mutual induction on all statements. We inline our proof of statement 4
with \textsc{TC-Guard}.

We know in all cases that the solution covers the pattern variables in
the program, return type, and constraints. Therefore by
Lemma~\ref{lem:penv-constrs-subset} we know that any produced environment
will contain pattern variables contained in the solution. We make use of
this fact implicitly throughout the proof.

\paragraph*{Statement 1: Synthesis}

\begin{proofcase}{TS-Base}

\begin{mathpar}
\inferrule
{ c \text{ has base type } D}
{ \synthseq{c}{D}{\cdot}{\emptyset} }
\end{mathpar}

By \textsc{T-Const}:

\begin{mathpar}
\inferrule
{ }
{ \tseq{\cdot}{c}{D} }
\end{mathpar}

noting that:
\begin{itemize}
\item $\un{\cdot}$
\item $\apppatsubst{c} = c$
\item $\apppatsubst{D} = D$
\end{itemize}

as required.
\end{proofcase}
\begin{proofcase}{TS-Unit}
Similar to \textsc{TS-Base}.
\end{proofcase}
\begin{proofcase}{TS-New}
Similar to \textsc{TS-Base}.
\end{proofcase}
\begin{proofcase}{TS-Spawn}

\begin{mathpar}
\inferrule
\chkseq{\tma}{\one}{\penv}{\constrs}
{ \synthseq{\spawn{\tma}}{\one}{\makeusable{\penv}}{\constrs} }
\end{mathpar}

Furthermore, we assume that $\patsubst$ is a usable solution for $\constrs$.

By the IH (2),
\[
\tseq{\apppatsubst{\penv}}{\tma}{\one}
\]

Recomposing by \textsc{T-Spawn}:

\begin{mathpar}
\inferrule
\tseq{\apppatsubst{\penv}}{\tma}{\one}
\tseq
\end{mathpar}

as required.
\end{proofcase}
\begin{proofcase}{TS-Send}
\begin{mathpar}
\inferrule
\proglookup{\msgtag{m}} = \seq{\ppretya} \\
\chkseq{\pvala}{\usablety{\tysend{\algomsg{m}}}}{\penv'}{\constrs} \\\\
(\chkseq{\pvalb_i}{\makeusable{\ppretya_i}}{\penv'_i}{\constrs'_i})_{i \in 1..n} \\
\combineseqmany{\penv' + \penv'_1 + \cdots + \penv'_n}{\penv}{\constrs''}
{ \synthseq
{\constrs \cup \constrs'_1 \cup \cdots \cup \constrs'_n \cup \constrs''}
\end{mathpar}

Also, we assume $\algoprogseq{\prog}{\constrs_{\var{prog}}}$.

Furthermore, we assume that $\patsubst$ is a solution for
$\constrs_{\var{prog}} \cup \constrs \cup \constrs'_1 \cup \cdots \cup \constrs'_n \cup \constrs''$.
By Lemma~\ref{lem:pat-subset}, we have that $\patsubst$ is also a
solution for each constraint set individually.

Thus, by the IH:

\begin{itemize}
\item
{ \apppatsubst{\penv'} }
{ \vala }
{ \usablety{\tysend{\msgtag{m}}} }$
\item
{ \apppatsubst{\penv'_i} }
{ \valb_i }
{ \makeusable{\apppatsubst{\ppretya_i}}}$ for $i \in 1..n$
\end{itemize}

By Corollary~\ref{cor:combine-many-sol},
there exist $ \tyenv' \subtype \aps{\penv'}$ and
$\tyenv'_i \subtype \aps{\penv'_i}$ for $i \in 1..n$ such that
$\tyenv' + \tyenv'_1 + \ldots + \tyenv'_n = \aps{\penv}$.

\begin{mathpar}
\inferrule
\proglookup[\aps{\prog}]{\msgtag{m}} = \seq{\aps{\ppretya}} \\
\inferrule
{ \tseq{\aps{\penv'}}{\vala}{\usablety{\tysend{\algomsg{m}}}} }
{ \tseq{\tyenv'}{\vala}{\usablety{\tysend{\algomsg{m}}}} } \\
\inferrule
{ (\tseq{\aps{\penv'_i}}{\valb_i}{\aps{\tya_i}})_{i \in 1..n} }
{ (\tseq{\tyenv'_i}{\valb_i}{\aps{\tya_i}})_{i \in 1..n} } \\
{ \tseq
{\tyenv' + \tyenv'_1 + \ldots +  \tyenv'_n }
\end{mathpar}

as required.
\end{proofcase}
\begin{proofcase}{TS-App}

\begin{mathpar}
\inferrule
\proglookup{f} = {\tyfun{\seq{\ptya}}{\ptyb}} \\\\
(\chkseq{\pvala_i}{\ptya_i}{\penv_i}{\constrs_i})_{i \in 1..n} \\
\combineseqmany{\penv_1 + \cdots + \penv_n}{\penv}{\constrs}
{ \synthseq
{ \fnapp{f}{\seq{\vala}} }
{\constrs \cup \constrs_1 \cup \ldots \cup \constrs_n}
\end{mathpar}

Also, we assume $\algoprogseq{\prog}{\constrs_{\var{prog}}}$.

We can also assume that there exists some $\patsubst$ which is a usable solution of
$\constrs_{\var{prog}} \cup \constrs_1 \cup \ldots \cup \constrs_n$.

By Lemma~\ref{lem:pat-subset}, we have that $\patsubst$ is a solution
for all $\constrs_i$ individually.

By the IH,
for all $i$.

By Corollary~\ref{cor:combine-many-sol}, there exist $(\tyenv_i \subtype
\penv_i)_{i \in 1..n}$ such that $\tyenv_1 + \ldots + \tyenv_n =
\aps{\penv}$.

Thus by \textsc{T-Sub} and \textsc{T-App}:

\begin{mathpar}
\inferrule
\aps{\funlookup{f}} = {\tyfun{\seq{\aps{\ptya}}}{\aps{\ptyb}}} \\
\inferrule*
(\vseq{\aps{\penv_i}}{\vala_i}{\aps{\ptya_i}})_{i \in
{ (\vseq{\tyenv_i}{\vala_i}{\aps{\ptya_i}})_{i \in
1..n} }
{ \tseq{\tyenv_1 + \cdots + \tyenv_n}{\fnapp{f}{\seq{\vala}}}{\aps{\ptyb}} }
\end{mathpar}
as required.
\end{proofcase}

\paragraph*{Statement 2: Checking}
\begin{proofcase}{TC-Var}
\begin{mathpar}
\inferrule
{ }
{ \chkseq{x}{\ptya}{x : \ptya}{\emptyset} }
\end{mathpar}

By \textsc{T-Var}:

\begin{mathpar}
\inferrule
{ }
{ \tseq
{x : \apppatsubst{\ptya}}
\end{mathpar}
as required.
\end{proofcase}

\begin{proofcase}{TC-Let}
\begin{mathpar}
\inferrule
\chkseq{\tma}{\makereturnable{\pretya}}{\penv_1}{\constrs_1} \\
\chkseq{\tmb}{\ptyb}{\penv_2}{\constrs_2} \\\\
\checkenvseq{\penv_2}{x}{\makereturnable{\pretya}}{\constrs_3} \\
\joinseq{\penv_1 \envwithout x}{\penv_2}{\penv}{\constrs_4}
\chkseq
{ \ptyb }
{ \penv }
{ \constrs_1 \cup \cdots \cup \constrs_4 }
\end{mathpar}

We also assume that we have some usable solution $\patsubst$ for
$\constrs_1 \cup \cdots \cup \constrs_4$, and by Lemma~\ref{lem:pat-subset},
we know that $\patsubst$ is a usable solution for all $\constrs_i$

By the IH, we have that:
\begin{itemize}
\item $\tseq{\aps{\penv_1}}{\tma}{\makereturnable{\aps{\pretya}}}$
\item $\tseq{\aps{\penv_2}}{\tmb}{\aps{\ptyb}}$
\end{itemize}

Since $\pretya$ does not contain any type variables we have that
$\aps{\makereturnable{\pretya}} = \makereturnable{\pretya}$.

By Lemma~\ref{lem:scomb-env-sol}, there exist some $\tyenv_1, \tyenv_2$ such that
$\tyenv_1 \subtype \aps{\penv_1 \envwithout x}$,
$\tyenv_2 \subtype \aps{\penv_2}$
and $\tyenv_1 \scomb \tyenv_2 = \aps{\penv}$

By the definition of $\mkwd{check}$, we have two subcases based on
whether $x \in \dom{\penv_2}$:

\begin{subcase}{$x \not\in \dom{\penv_2}$}
In this case we have that

By Lemma~\ref{lem:unr-soundness}, we have that

Thus by \textsc{T-Let} and \textsc{T-Sub}:

\begin{mathpar}
\inferrule
\tseq{\aps{\penv_1}}{\tma}{\makereturnable{\pretya}} \\
\inferrule*
\inferrule*
{ \tseq{\aps{\penv_2}}{\tmb}{\aps{\ptyb}} }
{ \tseq{\aps{\penv_2}, x : \makereturnable{\pretya}}{\tmb}{\aps{\ptyb}} }
\tseq{\tyenv}{\tmb}{\aps{\ptyb}}
\tseq
{ \aps{\penv} }
{ \letin[\pretya]{x}{\tma}{\tmb}}
{ \aps{\ptyb} }
\end{mathpar}

as required.
\end{subcase}
\begin{subcase}{$x \in \dom{\penv_2}$}
In this case, we have that
$x : \makereturnable{\pretya} \in \penv_2$ and

By Lemma~\ref{lem:subtype-soundness},
$\makereturnable{\pretya} \subtype \aps{\ptyb}$.

Thus by \textsc{T-Let} and \textsc{T-Sub}:

\begin{mathpar}
\inferrule
\tseq{\aps{\penv_1}}{\tma}{\makereturnable{\pretya}} \\
\inferrule*
\tseq
{\aps{\penv_2}, x : \makereturnable{\pretya}}
\tseq{\tyenv}{\tmb}{\aps{\ptyb}}
\tseq
{ \aps{\penv} }
{ \letin[\pretya]{x}{\tma}{\tmb}}
{ \aps{\ptyb} }
\end{mathpar}

as required.
\end{subcase}

\end{proofcase}

\begin{proofcase}{TC-Guard}

\begin{mathpar}
\inferrule
\inferrule
{ (\chkgseq
{\patb_i})_{i \in 1..n} \\\\
\manymergeseq
{\constrs} \\
\constrs' = \bigcup_{i \in 1..n} \constrs_i
{ \chkgseq
{\constrs \cup \constrs'}
{\patb_1 \patplus \ldots \patplus \patb_n}
} \\
\chkseq{\tma}{\retty{\tyrecv{\patb}}}{\penv'}{\constrs_2} \\
\combineseq{\nullableenv}{\penv'}{\penv}{\constrs_3}
{ \chkseq
{\constrs \cup \constrs' \cup \constrs_2 \cup \constrs_3 \cup
\set{\subpatconstr{\pata}{\patb}}}
\end{mathpar}
where $\patb = \patb_1 \patplus \cdots \patplus \patb_n$.

Since guards must be unique we know that there will be at most one
$\fail$ branch in $\seq{G}$.  Without loss of generality assume that
$\gd_1 = \fail$ (the order of guards does not matter, and the argument
is the same if there is no $\fail$ guard).

Let us assume without loss of generality that $n > 1$ (i.e., $\fail$ is
not the only guard).

Thus we have that:
\begin{itemize}
\item $\chkgseq{\pata}{\fail}{\ptya}{\noenv}{\emptyset}{\mbzero}$ (i.e.,
$\nullableenv_1 = \noenv, \constrs_1 = \emptyset, \patb_1 = \mbzero$)
\item $\chkgseq{\pata}{\gd_i}{\ptya}{\penv_i}{\constrs_i}{\patb_i}$ for $2 \le i \le n$
\item $\manymergeseq{\penv_2}{\penv_n}{\penv}{\constrs}$
\end{itemize}

By repeated use of the induction hypothesis (statement 3),
we have that
{\apppatsubst{\ptya}}$ where $\pnflittwo{\pata}{\patb_i}$ for
$2 \le i \le n$.

Since $\patb = \patb_1 \patplus \cdots \patplus \patb_n$ and
$\pnflittwo{\pata}{\patb_i}$ for $i \in 1..n$, it follows by the
definition of pattern normal form that $\pnftwo{\pata}{\patb}$.

Since $\patsubst$ is a usable solution of the constraint set we have
that $\subpat{\pata}{\patb}$.

Now since $\pnftwo{\pata}{\patb}$ and $\subpat{\pata}{\patb}$, by
Lemma~\ref{lem:subpattern-pnf} we have that $\pnf{\patb}$.

By Lemma~\ref{lem:merge-env-sol}, we have that there exists some
$\tyenv$ such that $\subtypetwo{\tyenv}{\penv_i}$ for each $i$. Thus, by
\textsc{T-Sub}, we can show:

Therefore, by \textsc{T-GuardSeq} we can show that
\gseq
{ \patb }
{ \tyenv }
{ \fail \cdot \gd_2 \cdot \ldots \cdot \gd_n }
{ \aps{\ptya} }

By the IH (statement 2), we have that

By Lemma~\ref{lem:combine-sol}, there exists some $\penv'' \subtype
\penv'$ such that $\tyenv + \aps{\penv''} = \aps{\penv}$.

Thus, we can show:
\begin{mathpar}
\inferrule
\inferrule
{ \tseq{\aps{\penv'}}{\vala}{\retty{\tyrecv{\patb}}} }
{ \tseq{\aps{\penv''}}{\vala}{\retty{\tyrecv{\patb}}} }
\\
\gseq{\patb}{\tyenv}{\fail \cdot \seq{G}}{\aps{\ptya}}
\\
\pata \subpatone \patb \\
\pnf{\patb}
{ \tseq
{\aps{\penv''} + {\tyenv}}
{\guardann{\vala}{\pata}{\fail \cdot \seq{G}}}
\end{mathpar}

as required.

\end{proofcase}
\begin{proofcase}{TC-Sub}
\begin{mathpar}
\inferrule
{ \synthseq{\tma}{\ptya}{\penv}{\constrs_1} \\
\subtyseq{\ptya}{\ptyb}{\constrs_2}
{ \chkseq{\tma}{\ptyb}{\penv}{\constrs_1 \cup \constrs_2} }
\end{mathpar}

By the IH (statement 1),

By Lemma~\ref{lem:subtype-soundness}, $\apppatsubst{\ptya} \subtype
\apppatsubst{\ptyb}$.

Therefore by \textsc{T-Sub}:

\begin{mathpar}
\inferrule
\tseq
\tseq
\end{mathpar}
as required.
\end{proofcase}

\paragraph*{Statement 3: Guards}

Note that there is no case for \textsc{TCG-Fail} since (contrary to the
theorem statement) it is not typable under a non-null typing environment.

\begin{proofcase}{TCG-Free}
\begin{mathpar}
\inferrule
{ \chkseq{\tma}{\ptya}{\penv}{\constrs} }
{ \chkgseq{\pata}{\free{\tma}}{\ptya}{\penv}{\constrs}{\mbone} }
\end{mathpar}

By the IH (statement 2), we have that

Trivially, $\pnflittwo{\pata}{\mbone}$.

Therefore, we can reconstruct by \textsc{TG-Free}:

\begin{mathpar}
\inferrule
\tseq{\aps{\penv}}{\tma}{\aps{\ptya}}
{ \gseq{\mbone}{\aps{\penv}}{\free{\tma}}{\aps{\ptya}} }
\end{mathpar}

as required.
\end{proofcase}
\begin{proofcase}{TCG-Recv}

\begin{mathpar}
\inferrule
\chkseq{\tma}{\ptyb}{\penv', y : \retty{\tyrecv{\ppatb}}}{\constrs_1} \\
\proglookup{\msgtag{m}} = {\seq{\ppretya}} \\
\penv = \penv' \envwithout \seq{x} \\
\base{\seq{\ppretya}} \vee \base{\penv'} \\
\checkenvseq{\penv'}{\seq{x}}{\seq{\makeusable{\ppretya}}}{\constrs_3}
{ \chkgseq
{\constrs_1 \cup \constrs_2 \cup \constrs_3 \cup
\set{\subpatconstr{\pata \without \msgtag{m}}{\ppatb}}
{\algomsg{m} \patconcat (\pata \without \msgtag{m})}
\end{mathpar}
We also assume that we have some usable solution $\patsubst$
\constrs_1 \cup \constrs_2 \cup \constrs_3 \cup
\set{\subpatconstr{\pata \without \msgtag{m}}{\ppatb}}

As usual, by Lemma~\ref{lem:pat-subset} we can assume that $\patsubst$
is a usable solution for all $\constrs_i$.

By the IH,
{ \aps{\penv'}, y : \retty{\tyrecv{\aps{\ppatb}}}}
{ \tma }
{ \aps{\ptyb} }$.

$\penv' = \penv, x_1 : \ptya_1, \ldots, x_m : \ptya_m$ and
$\seq{x} = x_1, \ldots, x_m$.

Then by the definition of $\mkwd{check}$ we have that:
\begin{itemize}
\item $(\subtyseq{\ptya_i}{\makeusable{\ppretya_i}}{\constrs'_i})_{i
\in 1..m}$
\item $(\unrseq{\ptya_i}{\constrs'_i})_{i \in m + 1..n}$
\end{itemize}

Thus by Lemma~\ref{lem:subtype-soundness},
$\makeusable{\aps{\ppretya_i}} \subtype \aps{\ptya_i}$ for each $i \in

By Lemma~\ref{lem:unr-soundness}, there exist $\tya_j \subtype
\aps{\ptya_j}$ such that
$\un{\tya_j}$ for $j \in {m + 1} .. n$.

Thus it follows by the definition of environment subtyping that
$\aps{\penv} \subtype \aps{\penv'}$.

It follows from the fact that pattern substitution preserves type shape
that if $\base{\seq{\pretya}} \vee \base{\penv'}$, we have that
$\base{\seq{\aps{\pretya}}} \vee \base{\aps{\penv'}}$.

Since $\patsubst$ is a usable solution of
$\subpatconstr{\pata \without \msgtag{m}}{\ppatb}$ we know that
$\pata \without \msgtag{m} \subpatone \aps{\ppatb}$ and therefore that
$\tyrecvp{\pata \without \msgtag{m}} \subtype \tyrecvp{\aps{\ppatb}}$.

It remains to be shown that $\pnflittwo{\pata}{\msgtag{m} \patconcat
(\pata \without \msgtag{m})}$:

\begin{mathpar}
\inferrule
\msgtag{m} \patconcat (\pata \without \msgtag{m})
\tyequiv
\pata
{ \pnflittwo{\pata}{\msgtag{m} \patconcat (\pata \without \msgtag{m})}}
\end{mathpar}

The pattern residual and concatenation cancel, so the premise holds and
therefore we can conclude that
$\pnflittwo{\pata}{\msgtag{m} \patconcat (\pata \without \msgtag{m})}$.

Finally, we can reconstruct using \textsc{TG-Recv}:

\begin{mathpar}
\inferrule
\proglookup[\aps{\prog}]{\msgtag{m}} = \seq{\aps{\ppretya}} \\
\base{\seq{\aps{\ppretya}}} \vee \base{\aps{\penv}} \\
\inferrule*
\tseq
{\aps{\penv'}, y : \retty{\tyrecv{\aps{\ppatb}}}}
{ \tma }
\tseq
y : \retty{\tyrecvp{\pata \without \msgtag{m}}},
\seq{x} : \seq{\makeusable{\pretya}}}
{ \tma }
\gseq
{\msgtag{m} \patconcat (\pata \without \msgtag{m})}
\end{mathpar}

as required.

\end{proofcase}
\end{proof}

\algosoundness*
\begin{proof}
A direct consequence of Lemma~\ref{lem:algo-soundness-generalised}.
\end{proof}

\newpage
\subsection{Algorithmic Completeness}
\label{sec:completeness}

Every $\tyenv$ is also a valid $\penv$ and every $\tya$ is a valid
$\ptya$. We will therefore allow ourselves to use $\tyenv$ and $\tya$ in
algorithmic type system derivations directly.

\begin{definition}[Closed program]
A program $\progdef{\sigs}{\seq{D}}{\tma}$ is \emph{closed}
if $\pv{\sigs} = \emptyset$ and $\pv{\seq{D}} = \emptyset$.
\end{definition}

\subsubsection{Useful auxiliary lemmas}

We begin by stating two useful results. The first lemma states that values are
typable in the algorithmic system without constraints.

\begin{lemma}\label{lem:val-completeness}
If $\tseq{\tyenv}{\vala}{\tya}$, then there exists some
$\tyenv'$ such that $\tyenv \subtype \tyenv'$ and
\end{lemma}
\begin{proof}
The proof is by induction on the derivation of $\tseq{\tyenv}{\vala}{\tya}$.

\begin{proofcase}{T-Var}
We assume that $\tseq{x : \tya}{x}{\tya}$.
By \textsc{TC-Var} we can show $\chkseq{x}{\tya}{x : \tya}{\emptyset}$,
as required.
\end{proofcase}
\begin{proofcase}{T-Const}
We assume that $\tseq{\cdot}{c}{\basety}$, where $c$ has base type
$\basety$. By \textsc{TS-Base}, we can show that
Finally, by \textsc{TC-Sub} (noting that
$\subtyseq{\basety}{\basety}{\emptyset}$) we have that
$\chkseq{c}{\basety}{\cdot}{\emptyset}$, as required.
\end{proofcase}
\begin{proofcase}{T-Sub}
\begin{mathpar}
\inferrule
{ \tyenv \subtype \tyenv' \\
\tya \subtype \tyb \\
\tseq{\tyenv'}{\vala}{\tya}
{ \tseq{\tyenv}{\vala}{\tyb} }
\end{mathpar}

By the IH, there exists some $\tyenv''$ such that
$\tyenv' \subtype \tyenv''$

By the transitivity of subtyping, we have that
$\tyenv \subtype \tyenv' \subtype \tyenv''$, as required.
\end{proofcase}
\end{proof}

\begin{lemma}\label{lem:synth-to-chk}
If $\synthseq{\tma}{\ptya}{\penv}{\constrs}$, then
\end{lemma}
\begin{proof}
Follows from the definition of \textsc{TC-Subs}, noting that the subtyping
constraint is instantiated as $\subtyseq{\ptya}{\ptya}{\constrs}$.
There are two ways we can create a derivation of
$\subtyseq{\ptya}{\ptya}{\constrs}$: either if $\ptya = \basety$ and we have
$\subtyseq{\ptya}{\ptya}{\emptyset}$, or if $\ptya$ is a mailbox type (take an
output mailbox type here, although the reasoning is the same for an input
mailbox). In this case, we would have a derivation of
Since $\subpatconstr{\ppata}{\ppata}$ is a tautology, it follows that we
need not add an additional constraint and can show

Using \textsc{TC-Subs} we can construct:
\begin{mathpar}
\inferrule
{ \synthseq{\tma}{\ptya}{\penv}{\constrs}
\\
\subtyseq{\ptya}{\ptya}{\emptyset}
{ \chkseq{\tma}{\ptya}{\penv}{\constrs} }
\end{mathpar}
as required.
\end{proof}

\subsubsection{Completeness of auxiliary definitions}

We now need to show completeness for all auxiliary judgements (e.g., subtyping,
environment combination).

\begin{lemma}[Completeness of type join]\label{lem:join-completeness-types}

\begin{itemize}
\item $\tya_1 \scomb \tya_2  = \tyb$,
\item $\tya_1 \subtype \aps[\patsubst_1]{\ptya_1}$,
\item $\tya_2 \subtype \aps[\patsubst_2]{\ptya_2}$; and
\item $\pv{\patsubst_1} \cap \pv{\patsubst_2} = \emptyset$
\end{itemize}
then there exist $\penv, \constrs$ such that
and there exists a usable solution $\patsubst \supseteq \patsubst_1 \cup
\patsubst_2$ of $\constrs$
such that $\tyb \subtype \aps{\ptyb}$.
\end{lemma}
\begin{proof}
We proceed by case analysis on the derivation of
$\tya_1 \scomb \tya_2 = \tyb$.
Base types follow straightforwardly, so we concentrate on mailbox types.

\begin{proofcase}
{$\tya_1 = \usageann{\usage_1}{\tysend{\pata_1}}$, $\tya_2 =
\usageann{\usage_2}{\tysend{\pata_2}}$}

\begin{mathpar}
\inferrule
\inferrule
{ }
{ \scombtwo{\tysend{\pata_1}}{\tysend{\pata_2}} =
\tysend{\patconcattwo{\pata_1}{\pata_2}} }
{ \usageann{\usage_1}{\tysend{\pata_1}}
\scomb
\usageann{\usage_2}{\tysend{\pata_2}}
\usageann{\usage_1 \scomb
\usage_2}{\tysendp{\patconcattwo{\pata_1}{\pata_2}}}
\end{mathpar}

Since the domains of $\patsubst_1, \patsubst_2$ are disjoint, let
$\patsubst = \patsubst_1 \cup \patsubst_2$.

In order for $\tysend{\pata_i} \subtype \aps[\patsubst_i]{\ptya_i}$ (for $i \in
1,2$) to hold, it must be the case that $\ptya_i = \tysend{\ppata_i}$
with $\aps[\patsubst]{\ppata_i} \subpatone \pata_i$.

In this case we can construct a derivation:

\begin{mathpar}
\inferrule
\joinseq
{ \tysend{\ppata_1}}
{ \tysend{\ppata_2}}
{ \tysendp{\patconcattwo{\ppata_1}{\ppata_2}}}
{\emptyset }
\joinseq
{\usageann{\usage_1 \scomb
\usage_2}{\tysendp{\patconcattwo{\ppata_1}{\ppata_2}}}}
{ \emptyset }
\end{mathpar}

Noting that $\aps[\patsubst]{\ppata_i} \subpatone \pata_i$,
it follows by the definition of pattern semantics that
$\aps{\patconcattwo{\ppata_1}{\ppata_2}} \subpatone
\patconcattwo{\pata_1}{\pata_2}$
and therefore that
{\usage_1 \scomb \usage_2}
{\tysendp{\ppata_1 \patconcat \ppata_2}}
\subtype
\usageann
{\usage_1 \scomb \usage_2}
{\aps{\tysendp{\ppata_1 \patconcat
\ppata_2}}}$

with $\patsubst \supseteq \patsubst_1 \cup \patsubst_2$ and a solution
of $\emptyset$, as required.

\end{proofcase}

\begin{proofcase}{$\tya_1 = \usageann{\usage_1}{\tysend{\pata}}, \tya_2 =
\usageann{\usage_2}{\tyrecvp{\pata \patconcat \patb}}$}

\begin{mathpar}
\inferrule*
\inferrule*
{ }
{ \scombtwo{\tysend{\pata}}{\tyrecvp{\pata \patconcat \patb}}  =
\tyrecv{\patb}}
{ \scombtwo
{\usageann{\usage_2}{\tyrecvp{\pata \patconcat \patb}}}
\usageann{\usage_1 \scomb \usage_2}{\patb}
\end{mathpar}

Since the domains of $\patsubst_1, \patsubst_2$ are disjoint, let
$\patsubst = \patsubst_1 \cup \patsubst_2$.

In order for
$\tysend{\pata} \subtype \aps[\patsubst_1]{\ptya_1}$
to hold, it must be the case that $\ptya_1 = \tysend{\ppata}$
with $\aps[\patsubst_1]{\ppata} \subpatone \pata$.

Similarly, for
$\tyrecvp{\pata \patconcat \patb} \subtype \aps[\patsubst_2]{\ptya_2}$
to hold, it must be the case that $\ptya_2 = \tyrecv{\ppatb}$
with $(\pata \patconcat \patb) \subpatone \aps[\patsubst_2]{\ppatb}$.

In this case we can construct a derivation:
Using algorithmic type joining, we can construct the following

\begin{mathpar}
\inferrule*
\inferrule*
{ \patvara \text{ fresh}}
\joinseq
{ \tysend{\ppata}}
{ \tyrecv{\ppatb}}
{ \tyrecv{\patvara}}
{ \set{\subpatconstr{\ppatb \patconcat \patvara}{\ppatb}} }
{ \joinseq
{ \usageann{\usage_1}{\tysend{\ppata}} }
{ \usageann{\usage_2}{\tyrecv{\ppatb}} }
{ \usageann{\usage_1 \scomb \usage_2}{\tyrecv{\patvara}} }
{ \set{\subpatconstr{\ppata \patconcat \patvara}{\ppatb}} }
\end{mathpar}

At this point we know that the domains of $\patsubst_1$ and
$\patsubst_2$ are disjoint. Let us construct $\patsubst = \patsubst_1
\cup \patsubst_2 \cup \patvara \mapsto \patb$.

It remains to be shown that $\patsubst$ is a solution; it suffices to
show that $(\aps{\ppata} \patconcat \patb) \subpatone \aps{\ppatb}$.

By the transitivity of pattern inclusion we have that
\[
(\aps{\ppata} \patconcat \patb)
\subpatone
(\pata \patconcat \patb)
\subpatone
\aps{\ppatb}
\]

We have that $\aps{\tyrecv{\patvara}} = \tyrecv{\patb}$

and therefore we have that (trivially)
$\tyrecv{\patb} \subtype \tyrecv{\patb}$

with $\patsubst \supset \patsubst_1 \cup \patsubst_2$ a solution for the
constraint set, as required.

\end{proofcase}

\begin{proofcase}{$\tya_1 = \usageann{\usage_1}{\tyrecv{\pata \patconcat
\patb}}, \tya_2 =
\usageann{\usage_2}{\tysend{\pata}}$}
Similar to the above case.
\end{proofcase}

\end{proof}

\begin{lemma}[Completeness of environment join]\label{lem:join-completeness}

\begin{itemize}
\item $\tyenv_1 \scomb \tyenv_2 = \tyenv$,
\item $\tyenv_1 \strictsubty \aps[\patsubst_1]{\penv_1}$,
\item $\tyenv_2 \strictsubty \aps[\patsubst_2]{\penv_2}$; and
\item $\pv{\patsubst_1} \cap \pv{\patsubst_2} = \emptyset$
\end{itemize}
then there exist $\penv, \constrs$ such that
and there exists a usable solution $\patsubst \supseteq \patsubst_1 \cup
\patsubst_2$ of $\constrs$
such that $\tyenv \subtype \aps{\penv}$.
\end{lemma}
\begin{proof}
By induction on the derivation of $\tyenv_1 \scomb \tyenv_2$, with appeal to
\end{proof}

\begin{lemma}[Completeness of disjoint environment combination]\label{lem:combine-completeness}

\begin{itemize}
\item $\tyenv_1 + \tyenv_2 = \tyenv$,
\item $\tyenv_1 \strictsubty \aps[\patsubst_1]{\penv_1}$,
\item $\tyenv_2 \strictsubty \aps[\patsubst_2]{\penv_2}$; and
\item $\pv{\patsubst_1} \cap \pv{\patsubst_2} = \emptyset$
\end{itemize}
then there exist $\penv, \constrs$ such that
and there exists a usable solution $\patsubst \supseteq \patsubst_1 \cup
\patsubst_2$ of $\constrs$
such that $\tyenv \subtype \aps{\penv}$.
\end{lemma}
\begin{proof}
By induction on the derivation of $\tyenv_1 + \tyenv_2 = \tyenv$.

\begin{proofcase*}{$\tyenv_1 = \cdot$ and $\tyenv_2 = \cdot$}
\begin{mathpar}
\inferrule
{ }
{ \pluscombtwo{\cdot}{\cdot} = \cdot }
\end{mathpar}

By the definition of environment subtyping, the only environment that can
be a supertype of the empty environment is $\cdot$. Therefore,
we can immediately conclude with the corresponding base case in
algorithmic type environment combination:

\begin{mathpar}
\inferrule
{ }
{ \combineseq{\cdot}{\cdot}{\cdot}{\emptyset} }
\end{mathpar}
\end{proofcase*}

\begin{proofcase*}{$x \not\in \dom{\tyenv_2}$}
\begin{mathpar}
\inferrule
{ x \not\in \dom{\tyenv_2} \\
\pluscombtwo{\tyenv_1}{\tyenv_2} = \tyenv
{ \pluscombtwo{\tyenv_1, x : \tya}{\tyenv_2} = \tyenv, x : \tya }
\end{mathpar}

\begin{itemize}
\item $\tyenv_1, x : \tya \strictsubty \aps[\patsubst_1]{\penv_1}$
\item $\tyenv_2 \strictsubty \aps[\patsubst_2]{\penv_2}$
\item $\pv{\patsubst_1} \cap \pv{\patsubst_2} = \emptyset$
\end{itemize}

Since we are considering strict subtyping on environments rather than
general subtyping, we can assume that $x : \tya \in \dom{\penv_1}$.
Therefore, let $\penv_1 = \penv'_1, x : \ptya$ with $\tya
\subtype \aps[\patsubst_1]{\ptya}$.

By the IH,
for some $\penv, \constrs$ and
there exists some usable solution
$\patsubst \supseteq \patsubst_1 \cup \patsubst_2$ of $\constrs$
such that $\tyenv_1 + \tyenv_2 \subtype \aps{\penv}$.

Since $\tya \subtype \aps[\patsubst_1]{\ptya}$ and $\patsubst_1
\subseteq \patsubst$, it follows that $\tya \subtype \aps{\ptya}$.

Therefore it follows that $\tyenv_1 + \tyenv_2, x : \tya \subtype
\aps{\penv, x : \ptya}$ as required.
\end{proofcase*}

\begin{proofcase*}{$x \not\in \dom{\tyenv_1}$}
\begin{mathpar}
\inferrule
{ x \not\in \dom{\tyenv_1} \\
\pluscombtwo{\tyenv_1}{\tyenv_2} = \tyenv
{ \pluscombtwo{\tyenv_1}{\tyenv_2, x : \tya} = \tyenv, x : \tya }
\end{mathpar}

Symmetric to the above case.
\end{proofcase*}

\begin{proofcase*}{$x \in \dom{\tyenv_1} \cap \dom{\tyenv_2}$}
\begin{mathpar}
\inferrule
{ \un{\tya} \\
\pluscombtwo{\tyenv_1}{\tyenv_2} = \tyenv
{ \pluscombtwo{\tyenv_1, x : \tya}{\tyenv_2, x : \tya} = \tyenv, x : \tya }
\end{mathpar}

In this case, we have that:
\begin{itemize}
\item $\penv_1, = \penv'_1, x : \ptyb_1$
\item $\penv_2 = \penv'_2, x : \ptyb_2$
\end{itemize}

By the IH, there exist $\penv, \constrs$ such that
and some usable solution $\patsubst \supseteq \patsubst_1 \cup
\patsubst_2$ of $\constrs$
such that $\tyenv \subtype \aps{\penv}$.

By algorithmic environment combination we have:
\begin{mathpar}
\inferrule
\combineseq{\penv'_1}{\penv'_2}{\penv}{\constrs_1} \\
{\equivseq{\ptyb_1}{\ptyb_2}{\constrs_2}} \\
{\unrseq{\ptyb_1}{\constrs_3}} \\
{ \combineseq
{\penv'_1, x : \ptyb_1}
{\penv'_2, x : \ptyb_2}
{\penv, x : \tyb_1 }
{\constrs_1 \cup \constrs_2 \cup \constrs_3 \cup \constrs_4}
\end{mathpar}

From $\un{\tya}$, we have two subcases based on whether $\tya$ is a base type
$\basety$, or a mailbox type $\usablety{\mbsendone}$.

\begin{subcase}{$\tya = \basety$}
In this case, by the definition of subtyping we have that
$\tyb_1 = \tyb_2 = \basety$ and therefore:

\begin{mathpar}
\inferrule
\combineseq{\penv'_1}{\penv'_2}{\penv}{\constrs} \\
{\equivseq{\basety}{\basety}{\emptyset}} \\
{\unrseq{\basety}{\emptyset}} \\
{ \combineseq
{\penv'_1, x : \basety}
{\penv'_2, x : \basety}
{\penv, x : \basety }
\end{mathpar}

with $\patsubst$ remaining a usable solution of $\constrs$.

It follows that $\penv'_1, x : \basety + \penv'_2, x : \basety
\subtype \aps{\penv}, x : \basety$, as required.
\end{subcase}

\begin{subcase}{$\tya = \usablety{\mbsendone}$}

In this case, we have that
$\tyb_1 = \usablety{\tysend{\ppatb_1}}$ and
$\tyb_2 = \usablety{\tysend{\ppatb_2}}$.

\begin{mathpar}
\inferrule
\combineseq{\penv'_1}{\penv'_2}{\penv}{\constrs} \\
\subpatconstr{\ppatb_2}{\ppatb_1}}}} \\
{\unrseq{\ppatb_1}{\set{\subpatconstr{\ppatb_1}{\mbone}}}} \\
{ \combineseq
{\penv'_1, \usablety{\tysend{\ppatb_1}}}
{\penv'_2, \usablety{\tysend{\ppatb_2}}}
{\penv, x : \usablety{\tysend{\ppatb_1}} }
{\constrs \cup
\set{
\subpatconstr{\ppatb_1}{\ppatb_2},
\subpatconstr{\ppatb_2}{\ppatb_1},
\subpatconstr{\ppatb_1}{\mbone},
\subpatconstr{\ppatb_2}{\mbone}
\end{mathpar}

Let $\patsubst' = \patsubst[\ppatb_1 \mapsto \mbone, \ppatb_2
\mapsto \mbone]$, which is now a usable solution for the
additional constraints.

Finally, we have that $\tyenv, x : \usablety{\mbsendone}
\subtype \apppatsubst[\patsubst']{\penv, x :
\usablety{\tysend{\ppatb_1}}}
\subtype
\apppatsubst
{\penv}, x : \usablety{\mbsendone}$, as required.
\end{subcase}
\end{proofcase*}
\end{proof}

As a corollary we can show the completeness of combining nullable environments:

\begin{corollary}\label{cor:combine-completeness-nullable}

\begin{itemize}
\item $\tyenv_1 + \tyenv_2 = \tyenv$,
\item $\tyenv_1 \subtype \aps[\patsubst_1]{\nullableenv_1}$,
\item $\tyenv_2 \subtype \aps[\patsubst_2]{\nullableenv_2}$; and
\item $\pv{\patsubst_1} \cap \pv{\patsubst_2} = \emptyset$
\end{itemize}
then there exist $\penv, \constrs$ such that
and there exists a usable solution $\patsubst \supseteq \patsubst_1 \cup
\patsubst_2$ of $\constrs$
such that $\tyenv \subtype \aps{\penv}$.
\end{corollary}

Next, we need to show completeness of merging.

\begin{lemma}\label{lem:merge-completeness-types}
\begin{itemize}
\item $\tya \subtype \aps[\patsubst_1]{\ptya_1}$,
\item $\tya \subtype \aps[\patsubst_2]{\ptya_2}$; and
\item $\pv{\patsubst_1} \cap \pv{\patsubst_2} = \emptyset$
\end{itemize}

then there exist $\ptya, \constrs$ such that
and there exists a usable solution
$\patsubst \supseteq \patsubst_1 \cup \patsubst_2$ of $\constrs$
such that $\tya \subtype \aps{\ptyb}$.
\end{lemma}
\begin{proof}
By case analysis on the structure of $\tya$.

Base types follow directly, so we need instead to examine mailbox types.

\begin{proofcase}{$\tya = \usageann{\usage}{\tysend{\pata}}$}
In this case, by the definition of subtyping, we have that:

\begin{itemize}
\item
$\usageann{\usage}{\tysend{\pata}} \subtype
\aps[\patsubst_1]{\usageann{\usage_1}{\tysend{\ppata}}}$
\item
$\usageann{\usage}{\tysend{\pata}} \subtype
\aps[\patsubst_2]{\usageann{\usage_2}{\tysend{\ppatb}}}$
\end{itemize}

We first show that $\usage \subtype \maxusage{\usage_1}{\usage_2}$.
If $\usage = \usable$ then it must be the case that $\usage_1,