However, the current definition of $ \vee $ breaks this property as
the counterexample to the static gradual guarantee above shows.  Also,
as we can see from the counterexample to the dynamic gradual guarantee,
join with a more precise type can yield a supertype—that is,
$\ottnt{T_{{\mathrm{1}}}} \, \sqsubseteq \,  \DYN $ and $ \DYN   \vee  \ottnt{T_{{\mathrm{2}}}}  \Sub  \ottnt{T_{{\mathrm{1}}}}  \vee  \ottnt{T_{{\mathrm{2}}}}$ hold.

One possible workaround is to adapt the “lifted join” operation
$\AGTjoin$ of the GTFL${}_\lesssim$ language [28]
to .  Like $ \vee $,
$  \unit    \rightarrow _{  \lin  }   \unit   \AGTjoin   \unit    \rightarrow _{  \un  }   \unit   =   \unit    \rightarrow _{  \lin  }   \unit  $ but, unlike $ \vee $,
$ \DYN  \AGTjoin   \unit    \rightarrow _{  \un  }   \unit   =  \DYN $.  Thus, the lifted
join would perhaps recover the gradual guarantee.  However, it seems
that the lifted join is the least upper bound operation for no known
ordering between types and we would lose the minimal type property of
if we used $\AGTjoin$.  Also, the lifted join has the
following property: $\ottnt{T} \AGTjoin \DYN$ is $\ottnt{T}$ only if $\ottnt{T}$
does not have nontrivial supertypes; otherwise $\ottnt{T} \AGTjoin \DYN$
is $\DYN$.  For example, $ \unit  \AGTjoin \DYN =  \unit $ and
$  \unit    \rightarrow _{  \lin  }   \unit   \AGTjoin \DYN =   \unit    \rightarrow _{  \lin  }   \unit  $ but
$  \unit    \rightarrow _{  \un  }   \unit   \AGTjoin \DYN = \DYN$ (because
$  \unit    \rightarrow _{  \un  }   \unit   \Sub   \unit    \rightarrow _{  \lin  }   \unit  $).  It means that the
standard narrowing property—if $\Gamma  \ottsym{,}  \ottmv{x}  \ottsym{:}  \ottnt{T_{{\mathrm{1}}}}  \vdashG  \mathbb{e}  \ottsym{:}  \ottnt{T}$ and
$\ottnt{T_{{\mathrm{2}}}}  \Sub  \ottnt{T_{{\mathrm{1}}}}$, then $\Gamma_{{\mathrm{1}}}  \ottsym{,}  \ottmv{x}  \ottsym{:}  \ottnt{T_{{\mathrm{2}}}}  \vdashG  \mathbb{e}  \ottsym{:}  \ottnt{T}$—does not hold.  We
leave more detailed analysis of the problem and possible remedy for
future work.

§ RELATED WORK

§.§ Gradual Typing

Findler and Felleisen Findler-Felleisen-2002 introduced two seminal ideas:
higher-order contracts that dynamically monitor conformance to
a type discipline, and blame to indicate whether it is the
library or the client which is at fault if the contract is violated.
Siek and Taha Siek-Taha-2006,DBLP:conf/ecoop/SiekT07 introduced gradual types to integrate
untyped and typed code, while Flanagan Flanagan-2006 introduced
hybrid types to integrate simple types with refinement types.  Both
used target languages with explicit casts and similar translations
from source to target; both exploit contracts, but neither allocates
blame.  Motivated by similarities between gradual and hybrid types,
Wadler and Findler Wadler-Findler-2009 introduced blame calculus, which unifies
the two by encompassing untyped, simply-typed, and refinement-typed
code. As the name indicates, it also restores blame, which enables a
proof of blame safety: blame for type errors always lays with
less-precisely typed code—“well-typed programs can't be blamed”.

While the first investigations of gradual typing were based on
simply-typed calculi, subsequent work has explored gradual
typing for a range of typing features. Polymorphism
[1, 44, 86] has
proved to be quite tricky, with one important question about
the Jack-of-All-Trades Principle [1] still open.
A gradual treatment of record types may be found in the paper on
Abstract Gradual Typing (AGT) [28]. Variant types have
proved elusive, but union types have been considered
[76] along with intersection types and polymorphism as
part of a set-theoretical reevaluation of gradual principles

Moving towards session types, systems with gradual typestate have been
considered [99, 27],
they extend an object-oriented
language with typestate by a dynamic type and define a suitable
translation to an internal language with casts. The additional
complication is to track the current typestate at run time.
Thiemann DBLP:conf/tgc/Thiemann14 describes a system with gradual types and
session types, but in it only types (and not session types) can be

Effect systems have been gradualized based on ideas from abstract
interpretation  by Banados Schwerter and others
Banados-et-al-2014. While the former work only presented a
gradualization of effects themselves a subsequent extension adds a
full treatment of types [71].
Related ideas are explored by Thiemann and Fennell
[81] who present an approach to
gradualize annotated type systems, like units and security
labels. Following an earlier approach for gradual security typing for
simply-typed lambda calculus [17], Thiemann and
Fennell DBLP:conf/csfw/FennellT13 developed gradual
security for an ML core language with references and subsequently for
a Java core language LJGS with polymorphic security labels [22]. Toro and
others DBLP:journals/toplas/ToroGT18 developed a gradual
calculus with slightly different features from first principles using
the AGT [28] approach. In each
of these approaches, special measures have to be taken to ensure the
key property of non-interference.
Gradual type systems related to session types also include
the run-time enforcement of affine typing of  Tov and Pucella Tov-Pucella-2010.

As noted in the introduction, gradual typing may be
important as a bridge to type systems that go beyond what is currently
available, including dependent, effect, and session types.
There is a range of gradual type systems for dependent types.
Ou and others Ou-et-al-2004 bridge the gap between
simply-typed lambda calculus and a calculus with indexed types.
In Flanagan's hybrid typing [24] subtyping judgments are
either proved or disproved statically by SMT theorem proving or
residualized as run-time checks.
Greenberg and others Greenberg-et-al-2010 consider
different styles of contracts in simply-typed and dependently-typed settings.
Lehmann and Tanter
DBLP:conf/popl/LehmannT17 present an approach that uses
the AGT methodology to obtain a gradual system that mediates between
simple types and dependent refinement types. This work has been
augmented with type inference by Vazou and others
DBLP:journals/pacmpl/VazouTH18 and it has been extend to verification
[2] where specifications may contains
unknown subformulas. Jafery and Dunfield
[45] consider gradualized refinements for
sum types with the goal to control errors in pattern matching.

Gradual ownership types [72] is a
gradualization of the Owners as Dominators principle of ownership. Its
theory is built with similar principles as other gradual languages,
but its flavor is different as ownership is not a semantic property,
but a structure imposed by the programmer.

Siek and others Siek-et-al-2015-criteria review desirable properties of
gradually-typed languages, while Wadler Wadler-2015 discusses
history of the blame calculus and why blame is important.
These papers provide overviews of the field, each with many further
citations. Many of the above-cited works strive to fulfill the
properties of Siek and others, not all of them are successful, but
further discussion of the properties exceeds the scope of this survey
of related work.

TypeScript TPD [97] applies contracts to
monitor the gradual typing of TypeScript, and evaluates the successes
and shortcomings of contracts in this context.

§.§ Session Types

Session types were introduced by Honda, Vasconcelos, and Kubo
Honda-1993,Honda-et-al-1998. The original system addressed
binary sessions, whereby types describe the interaction between two
partners. Binary sessions were eventually extended to the more general
setting of multiparty session types [39].
Recent years have seen the introduction of session types in
programming languages, and software development tools. We review the
most important works.

Session types inspired the design of several programming languages.
Sing# [19] constitutes one of the first
attempts to introduce session types in programming languages. An
extension of C, Sing# was used to implement Singularity, an operating
system based on message passing.
Gay and others Gay-et-al-2010 propose attaching session types to class
definitions, allowing to treat channels as objects for session-based
communication in distributed systems.
SePi [26] is a concurrent, message-passing
programming language based on the pi-calculus, featuring a simple form
of refinement types.
SILL [84, 65] is a
higher-order session functional programming language, featuring
process expressions as first class objects via a linear contextual
Concurrent C0 [98] is a type-safe C-like
programming language equipped with channel communication governed by
session types.
Links [53] is a functional programming language
designed for tierless web applications that natively
supports binary session types.

Proposals have been made to retroactively introduce session types in
mainstream programming languages.
Session Java [41] introduces API-based session
primitives in Java, while [42] presents a Java
language extension and type discipline for session-based event-driven
Featherweight Erlang [56] imposes a
session-based type system to discipline message passing in Erlang.
Mungo [49] is a tool for checking Java
code against session types, presented in the form of typestates.
Embedding of session types have
been proposed for Haskell
[62, 68, 69, 67, 51],
OCaml [64], Scala [70], and
Rust [46].
Most of these embeddings delegate linearity checks to the run-time system.

Session types can be used in the software development process under
different forms, including languages to describe protocols,
specialised libraries to invoke session-based communication
primitives, provision for run-time monitoring against session types,
and extended type checkers.
Scribble [35] is a language-agnostic protocol description
formalism used in many different tools.
Multiparty Session C [60] uses Scribble, a
compiler plug-in, and a C library to validate against
session types.
Hu and Yoshida Hu-Yoshida-2016 generate protocol-specific Java APIs from
multiparty session types described in Scribble.
SPY [59] generates run-time monitors for endpoint
communication from Scribble protocols.
Neykova and Yoshida Neykova-Yoshida-2014 designed and implemented a session actor
library in Python together with a run-time verification mechanism.
Bocchi and others Bocchi-et-al-2013 present a theory that incorporates both
static typing and dynamic monitoring of session types.
Fowler Fowler-2016b describes a framework for monitoring Erlang
applications against multiparty session types.
Neykova and Yoshida Neykova-Yoshida-2017 investigate failure handling for
Erlang processes in a system that dynamically monitors session

§ CONCLUSIONS

We presented the design of ,
which combines a session-typed language along the lines of Gay and Vasconcelos Gay-Vasconcelos-2010
with a blame calculus along the lines of Wadler and Findler Wadler-Findler-2009,
and with dynamic enforcement of linearity along the lines of Tov and Pucella
We established expected results for such
a language, including type safety and blame safety.
Although the gradual guarantee does not hold, it seems that it is not
clear how it can be recovered without losing other good properties.

Much remains to be done; we consider just one future direction here.
The embedding of linear types in the unrestricted dynamic type relies
on an indirection through a cell in the store. In our
present work, these cells are used once and then discarded. This
one-shot policy imposes a certain usage pattern on linear
values embedded in the unityped language. In particular, the send and receive operations on a channel
need to be chained as in $(\close{(\send{v_2}{(\send{v_1}{c})})})$.
However, one could imagine a unityped language where one
may use the channel non-linearly in an imperative style as in $(\send{v_1}{c};
\send{v_2}{c};\close{c})$, mimicking the style of network programming in
conventional languages. This style can also be supported by a variant
of  with a
multi-shot policy that restores an updated channel to the same
cell from which it was extracted. We leave the full formalisation of
this policy to future work.

We would like to thank Alceste Scalas and Nobuko Yoshida for comments
and pointing out errors in the definition of subtyping rules, Kaede
Kobayashi for pointing out subtle errors in the operational semantics,
and anonymous reviewers for constructive comments.  We are also
grateful to Hannes Saffrich for implementing a type checker for the
calculus in this paper. This work was supported in part by the JSPS
KAKENHI Grant Number JP17H01723 (Igarashi), by FCT through the LASIGE
Research Unit ref. UID/CEC/00408/2019 and project Confident ref.PTDC/EEI-CTP/4503/2014 (Vasconcelos), and by EPSRC programme grant
EP/K034413/1 (Wadler).

[1]
Ahmed, Amal, Findler, Robert Bruce, Siek, Jeremy G., & Wadler, Philip. (2011).
Blame for all.
Pages  201–214 of: Ball, Thomas, & Sagiv, Mooly (eds), Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of
Programming Languages, POPL 2011, Austin, TX, USA, January 26-28, 2011.

[2]
Bader, Johannes, Aldrich, Jonathan, & Tanter, Éric. (2018).
Gradual program verification.
Pages  25–46 of: Dillig, Isil, & Palsberg, Jens (eds), Verification, Model Checking, and Abstract Interpretation - 19th
International Conference, VMCAI 2018, Los Angeles, CA, USA, January 7-9,
2018, Proceedings.
Lecture Notes in Computer Science, vol. 10747.

[3]
Bañados Schwerter, Felipe, Garcia, Ronald, & Tanter, Éric. (2014).
A theory of gradual effect systems.
Pages  283–295 of: International Conference on Functional
Programming (ICFP).

[4]
Barendregt, H.P.(̇1984).
The Lambda Calculus: Its Syntax and Semantics.

[5]
Bierman, Gavin, Abadi, Martín, & Torgersen, Mads. (2014).
Understanding TypeScript.
Pages  257–281 of: European Conference on Object-Oriented
Programming (ECOOP).
LNCS, vol. 8586.

[6]
Bierman, Gavin M., Meijer, Erik, & Torgersen, Mads. (2010).
Adding dynamic types to C#.
Pages  76–100 of: European Conference on Object-Oriented
Programming (ECOOP).

[7]
Bocchi, Laura, Chen, Tzu-Chun, Demangeon, Romain, Honda, Kohei, & Yoshida,
Nobuko. (2013).
Monitoring networks through multiparty session types.
Pages  50–65 of: Formal Techniques for Distributed

[8]
Bocchi, Laura, Chen, Tzu-Chun, Demangeon, Romain, Honda, Kohei, & Yoshida,
Nobuko. (2017).
Monitoring networks through multiparty session types.
Theoretical computer science, 699, 33–58.

[9]
Brady, Edwin. (2013).
Idris, a general-purpose dependently typed programming language:
Design and implementation.
Journal of functional programming, 23(05), 552–593.

[10]
Caires, Luís, & Pfenning, Frank. (2010).
Session types as intuitionistic linear propositions.
Pages  222–236 of: International Conference on
Concurrency Theory (CONCUR).

[11]
Caires, Luis, Pfenning, Frank, & Toninho, Bernardo. (2014).
Linear logic propositions as session types.
Mathematical structures in computer science, 26(03),

[12]
Castagna, Giuseppe, Lanvin, Victor, Petrucciani, Tommaso, & Siek, Jeremy G.
Gradual typing: A new perspective.
PACMPL, 3(POPL), 16:1–16:32.

[13]
Chaudhuri, Avik, Vekris, Panagiotis, Goldman, Sam, Roch, Marshall, & Levi,
Gabriel. (2017).
Fast and precise type checking for JavaScript.
PACMPL, 1(OOPSLA), 48:1–48:30.

[14]
Cimini, Matteo, & Siek, Jeremy G. (2016).
The Gradualizer: A methodology and algorithm for generating gradual
type systems.
Pages  443–455 of: Proceedings of the 43rd Annual ACM
SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL
2016, St. Petersburg, FL, USA, January 20 - 22, 2016.

[15]
Cooper, Ezra, Lindley, Sam, Wadler, Philip, & Yallop, Jeremy. (2007).
Links: Web programming without tiers.
Pages  266–296 of: Formal Methods for Components and

[16]
Demangeon, Romain, Honda, Kohei, Hu, Raymond, Neykova, Rumyana, & Yoshida,
Nobuko. (2015).
Practical interruptible conversations: distributed dynamic
verification with multiparty session types and python.
Formal methods in system design, 46(3), 197–225.

[17]
Disney, Tim, & Flanagan, Cormac. (2011).
Gradual information flow typing.
Workshop on From Scripts to Program (STOP).

[18]
Ernst, Erik, Møller, Anders, Schwarz, Mathias, & Strocco, Fabio. (2017).
Message safety in Dart.
Sci. comput. program., 133, 51–73.

[19]
Fähndrich, Manuel, Aiken, Mark, Hawblitzel, Chris, Hodson, Orion, Hunt,
Galen C., Larus, James R., & Levi, Steven. (2006).
Language support for fast and reliable message-based communication in
Singularity OS.
Pages  177–190 of: European Conference on Computer
Systems (EuroSys).

[20]
Fennell, Luminous, & Thiemann, Peter. (2012).
The blame theorem for a linear lambda calculus with type dynamic.
Pages  37–52 of: Trends in Functional Programming.
LNCS, vol. 7829.

[21]
Fennell, Luminous, & Thiemann, Peter. (2013).
Gradual security typing with references.
Pages  224–239 of: 2013 IEEE 26th Computer Security
Foundations Symposium, New Orleans, LA, USA, June 26-28, 2013.
IEEE Computer Society.

[22]
Fennell, Luminous, & Thiemann, Peter. (2016).
LJGS: gradual security types for object-oriented languages.
Pages  9:1–9:26 of: Krishnamurthi, Shriram, & Lerner,
Benjamin S. (eds), 30th European Conference on Object-Oriented
Programming, ECOOP 2016, July 18-22, 2016, Rome, Italy.
LIPIcs, vol. 56.
Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik.

[23]
Findler, Robert Bruce, & Felleisen, Matthias. (2002).
Contracts for higher-order functions.
Pages  48–59 of: International Conference on Functional
Programming (ICFP).

[24]
Flanagan, Cormac. (2006).
Hybrid type checking.
Pages  245–256 of: Principles of Programming Languages

[25]
Fowler, Simon. (2016).
An Erlang implementation of multiparty session actors.
Pages  36–50 of: Interaction and Concurrency Experience.

[26]
Franco, Juliana, & Vasconcelos, Vasco Thudichum. (2013).
A concurrent programming language with refined session types.
Pages  15–28 of: SEFM.
LNCS, vol. 8368.

[27]
Garcia, Ronald, Tanter, Éric, Wolff, Roger, & Aldrich, Jonathan. (2014).
Foundations of typestate-oriented programming.
ACM trans. program. lang. syst., 36(4), 12:1–12:44.

[28]
Garcia, Ronald, Clark, Alison M., & Tanter, Éric. (2016).
Abstracting gradual typing.
Pages  429–442 of: Principles of Programming Languages

[29]
Gay, Simon, & Hole, Malcolm. (2005).
Subtyping for session types in the pi calculus.
Acta informatica, 42(2-3), 191–225.

[30]
Gay, Simon, & Vasconcelos, Vasco. (2010).
Linear type theory for asynchronous session types.
Journal of functional programming, 20(01), 19–50.

[31]
Gay, Simon J., Vasconcelos, Vasco Thudichum, Ravara, António, Gesbert,
Nils, & Caldeira, Alexandre Z. (2010).
Modular session types for distributed object-oriented programming.
Pages  299–312 of: Principles of Programming Languages

[32]
Girard, Jean-Yves. (1987).
Linear logic.
Theoretical computer science, 50(1), 1–101.

[33]
Gommerstadt, Hannah, Jia, Limin, & Pfenning, Frank. (2018).
Session-typed concurrent contracts.
Pages  771–798 of: Ahmed, Amal (ed), Programming
Languages and Systems - 27th European Symposium on Programming, ESOP 2018,
Held as Part of the European Joint Conferences on Theory and Practice of
Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018,
Lecture Notes in Computer Science, vol. 10801.

[34]
Greenberg, Michael, Pierce, Benjamin C., & Weirich, Stephanie. (2010).
Contracts made manifest.
Pages  353–364 of: Principles of Programming Languages

[35]
Honda, K., Mukhamedov, A., Brown, G., Chen, T., & Yoshida, N. (2011).
Scribbling interactions with a formal foundation.
Pages  55–75 of: ICDCIT.
LNCS, vol. 6536.

[36]
Honda, Kohei. (1993).
Types for dyadic interaction.
Pages  509–523 of: International Conference on
Concurrency Theory (CONCUR).
LNCS, vol. 715.

[37]
Honda, Kohei, Vasconcelos, Vasco, & Kubo, Makoto. (1998).
Language primitives and type discipline for structured
communication-based programming.
Pages  122–138 of: European Symposium on Programming

[38]
Honda, Kohei, Yoshida, Nobuko, & Carbone, Marco. (2008).
Multiparty asynchronous session types.
Pages  273–284 of: Principles of Programming Languages

[39]
Honda, Kohei, Yoshida, Nobuko, & Carbone, Marco. (2016).
Multiparty asynchronous session types.
Journal of the acm, 63(1), 9.

[40]
Hu, Raymond, & Yoshida, Nobuko. (2016).
Hybrid session verification through endpoint API generation.
Pages  401–418 of: Fundamental Approaches to Software
Engineering (FASE).
LNCS, vol. 9633.

[41]
Hu, Raymond, Yoshida, Nobuko, & Honda, Kohei. (2008).
Session-based distributed programming in Java.
Pages  516–541 of: European Conference on Object-Oriented
Programming (ECOOP).
LNCS, vol. 5142.

[42]
Hu, Raymond, Kouzapas, Dimitrios, Pernet, Olivier, Yoshida, Nobuko, & Honda,
Kohei. (2010).
Type-safe eventful sessions in Java.
Pages  329–353 of: European Conference on Object-Oriented
Programming (ECOOP).
LNCS, vol. 6183.

[43]
Igarashi, Atsushi, Thiemann, Peter, Vasconcelos, Vasco T., & Wadler, Philip.
Gradual session types.
PACMPL, 1(ICFP), 38:1–38:28.

[44]
Igarashi, Yuu, Sekiyama, Taro, & Igarashi, Atsushi. (2017b).
On polymorphic gradual typing.
PACMPL, 1(ICFP), 40:1–40:29.

[45]
Jafery, Khurram A., & Dunfield, Joshua. (2017).
Sums of uncertainty: Refinements go gradual.
Pages  804–817 of: Castagna, Giuseppe, & Gordon, Andrew D.
(eds), Proceedings of the 44th ACM SIGPLAN Symposium on Principles
of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017.

[46]
Jespersen, Thomas Bracht Laumann, Munksgaard, Philip, & Larsen, Ken Friis.
Session types for Rust.
Pages  13–22 of: Workshop on Generic Programming (WGP).

[47]
Jia, Limin, Gommerstadt, Hannah, & Pfenning, Frank. (2016).
Monitors and blame assignment for higher-order session types.
Pages  582–594 of: Bodík, Rastislav, & Majumdar, Rupak
(eds), Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium
on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA,
January 20 - 22, 2016.

[48]
Kobayashi, Naoki, Pierce, Benjamin C., & Turner, David N. (1999).
Linearity and the pi-calculus.
ACM trans. program. lang. syst., 21(5), 914–947.

[49]
Kouzapas, Dimitrios, Dardha, Ornela, Perera, Roly, & Gay, Simon J. (2016).
Typechecking protocols with Mungo and StMungo.
Pages  146–159 of: Principles and Practice of Declarative
Programming (PPDP).

[50]
Lehmann, Nico, & Tanter, Éric. (2017).
Gradual refinement types.
Pages  775–788 of: Castagna, Giuseppe, & Gordon, Andrew D.
(eds), Proceedings of the 44th ACM SIGPLAN Symposium on Principles
of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017.

[51]
Lindley, Sam, & Morris, J. Garrett. (2016a).
Embedding session types in Haskell.
Pages  133–145 of: Symposium on Haskell.

[52]
Lindley, Sam, & Morris, J Garrett. (2016b).
Talking bananas: Structural recursion for session types.
Pages  434–447 of: International Conference on Functional
Programming (ICFP).

[53]
Lindley, Sam, & Morris, J. Garrett. (2017).
Behavioural types: from theory to tools.
River Publishers.
Chap. Lightweight functional session types.

[54]
Melgratti, Hernán C., & Padovani, Luca. (2017).
Chaperone contracts for higher-order sessions.
PACMPL, 1(ICFP), 35:1–35:29.

[55]
Milner, Robin, Parrow, Joachim, & Walker, David. (1992).
A calculus of mobile processes, I.
Information and computation, 100(1), 1–40.

[56]
Mostrous, Dimitris, & Vasconcelos, Vasco T. (2011).
Session typing for a featherweight Erlang.
Pages  95–109 of: Coordination Models and Languages
LNCS, vol. 6721.

[57]
Neykova, Rumyana, & Yoshida, Nobuko. (2014).
Multiparty session actors.
Pages  131–146 of: Coordination Models and Languages
LNCS, vol. 8459.

[58]
Neykova, Rumyana, & Yoshida, Nobuko. (2017).
Let it recover: Multiparty protocol-induced recovery.
Pages  98–108 of: International Conference on Compiler
Construction (CC).

[59]
Neykova, Rumyana, Yoshida, Nobuko, & Hu, Raymond. (2013).
SPY: local verification of global protocols.
Pages  358–363 of: International Conference on Runtime
Verification (RV).
LNCS, vol. 8174.

[60]
Ng, Nicholas, Yoshida, Nobuko, & Honda, Kohei. (2012).
Multiparty Session C: Safe parallel programming with message
Pages  202–218 of: International Conference on Modelling
Techniques and Tools for Computer Performance Evaluation (TOOLS).
LNCS, vol. 7304.

[61]
Norell, Ulf. (2009).
Dependently typed programming in Agda.
Pages  1–2 of: Proceedings of the 4th International
Workshop on Types in Language Design and Implementation.
TLDI '09.

[62]
Orchard, Dominic, & Yoshida, Nobuko. (2016).
Effects as sessions, sessions as effects.
Pages  568–581 of: Principles of Programming Languages

[63]
Ou, Xinming, Tan, Gang, Mandelbaum, Yitzhak, & Walker, David. (2004).
Dynamic typing with dependent types.
Pages  437–450 of: IFIP International Conference on
Theoretical Computer Science,  vol. 155.

[64]
Padovani, Luca. (2017).
A simple library implementation of binary sessions.
Journal of functional programming, 27, e4.

[65]
Pfenning, Frank, & Griffith, Dennis. (2015).
Polarized substructural session types.
Pages  3–22 of: International Conference on Foundations
of Software Science and Computation Structures.
LNCS, vol. 9034.

[66]
Pierce, Benjamin C. (2002).
Types and programming languages.
MIT Press.

[67]
Polakow, Jeff. (2015).
Embedding a full linear lambda calculus in Haskell.
Pages  177–188 of: Symposium on Haskell.

[68]
Pucella, Riccardo, & Tov, Jesse A. (2008).
Haskell session types with (almost) no class.
Pages  25–36 of: Symposium on Haskell.

[69]
Sackman, Matthew, & Eisenbach, Susan. (2008).
Session types in Haskell: Updating message passing for the
21st century.

[70]
Scalas, Alceste, & Yoshida, Nobuko. (2016).
Lightweight session programming in Scala.
Pages  21:1–21:28 of: European Conference on
Object-Oriented Programming (ECOOP).
Schloss Dagstuhl.

[71]
Schwerter, Felipe Bañados, Garcia, Ronald, & Tanter, Éric. (2016).
Gradual type-and-effect systems.
J. funct. program., 26, e19.

[72]
Sergey, Ilya, & Clarke, Dave. (2012).
Gradual ownership types.
Pages  579–599 of: Seidl, Helmut (ed), Programming
Languages and Systems - 21st European Symposium on Programming, ESOP 2012,
Held as Part of the European Joint Conferences on Theory and Practice of
Software, ETAPS 2012, Tallinn, Estonia, March 24 - April 1, 2012.
Lecture Notes in Computer Science, vol. 7211.

[73]
Siek, Jeremy, Thiemann, Peter, & Wadler, Philip. (2015a).
Blame and coercion: Together again for the first time.
Pages  425–435 of: Programming Language Design and
Implementation (PLDI).

[74]
Siek, Jeremy G., & Taha, Walid. 2006 (Sept.).
Gradual typing for functional languages.
Pages  81–92 of: Scheme and Functional Programming
Workshop (Scheme).

[75]
Siek, Jeremy G., & Taha, Walid. (2007).
Gradual typing for objects.
Pages  2–27 of: ECOOP.
Lecture Notes in Computer Science, vol. 4609.

[76]
Siek, Jeremy G., & Tobin-Hochstadt, Sam. (2016).
The recursive union of some gradual types.
Pages  388–410 of: Lindley, Sam, McBride, Conor, Trinder,
Philip W., & Sannella, Donald (eds), A List of Successes That Can
Change the World - Essays Dedicated to Philip Wadler on the Occasion of His
60th Birthday.
Lecture Notes in Computer Science, vol. 9600.

[77]
Siek, Jeremy G., Vitousek, Michael M., Cimini, Matteo, & Boyland, John T.
Refined criteria for gradual typing.
Pages  274–293 of: Summit on Advances in Programming
Languages (SNAPL).
LIPIcs, vol. 32.
Schloss Dagstuhl.

[78]
The Coq Development Team. 2019 (Jan.).
The coq proof assistant, version 8.9.0.

[79]
The Dart Team. (2014).
Dart programming language specification.
Google, 1.2 edition.

[80]
Thiemann, Peter. (2014).
Session types with gradual typing.
Pages  144–158 of: TGC.
LNCS, vol. 8902.

[81]
Thiemann, Peter, & Fennell, Luminous. (2014).
Gradual typing for annotated type systems.
Pages  47–66 of: Shao, Zhong (ed), Programming Languages
and Systems - 23rd European Symposium on Programming, ESOP 2014, Held as
Part of the European Joint Conferences on Theory and Practice of Software,
ETAPS 2014, Grenoble, France, April 5-13, 2014, Proceedings.
Lecture Notes in Computer Science, vol. 8410.

[82]
Tobin-Hochstadt, Sam, & Felleisen, Matthias. (2008).
The design and implementation of typed Scheme.
Pages  395–406 of: Necula, George C., & Wadler, Philip (eds),
Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles
of Programming Languages, POPL 2008, San Francisco, California, USA,
January 7-12, 2008.

[83]
Toninho, Bernardo, & Yoshida, Nobuko. (2018).
Depending on session-typed processes.
Pages  128–145 of: FoSSaCS.
Lecture Notes in Computer Science, vol. 10803.

[84]
Toninho, Bernardo, Caires, Luís, & Pfenning, Frank. (2013).
Higher-order processes, functions, and sessions: A monadic
Pages  350–369 of: European Symposium on Programming
LNCS, vol. 7792.

[85]
Toro, Matías, Garcia, Ronald, & Tanter, Éric. (2018).
Type-driven gradual security with references.
ACM trans. program. lang. syst., 40(4), 16:1–16:55.

[86]
Toro, Matías, Labrada, Elizabeth, & Tanter, Éric. (2019).
Gradual parametricity, revisited.
PACMPL, 3(POPL), 17:1–17:30.

[87]
Tov, Jesse A., & Pucella, Riccardo. (2010).
Stateful contracts for affine types.
Pages  550–569 of: European Symposium on Programming
LNCS, vol. 6012.

[88]
Vasconcelos, Vasco Thudichum. (2012).
Fundamentals of session types.
Information and computation, 217, 52–70.

[89]
Vazou, Niki, Tanter, Éric, & Horn, David Van. (2018).
Gradual liquid type inference.
PACMPL, 2(OOPSLA), 132:1–132:25.

[90]
Verlaguet, Julien. (2013).
Facebook: Analysing PHP statically.
Workshop on Commercial Uses of Functional Programming (CUFP).

[91]
Vitousek, Michael M., Swords, Cameron, & Siek, Jeremy G. (2017).
Big types in little runtime: Open-world soundness and collaborative
blame for gradual type systems.
Pages  762–774 of: Castagna, Giuseppe, & Gordon, Andrew D.
(eds), Proceedings of the 44th ACM SIGPLAN Symposium on Principles
of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017.

[92]
Wadler, Philip. (2012).
Propositions as sessions.
Pages  273–286 of: International Conference on Functional
Programming (ICFP).

[93]
Wadler, Philip. (2014).
Propositions as sessions.
Journal of functional programming, 24(2-3), 384–418.

[94]
Wadler, Philip. (2015).
A complement to blame.
Pages  309–320 of: 1st Summit on Advances in Programming
Languages (SNAPL).
LIPIcs, vol. 32.
Schloss Dagstuhl.

[95]
Wadler, Philip, & Findler, Robert Bruce. (2009).
Well-typed programs can't be blamed.
Pages  1–16 of: European Symposium on Programming
LNCS, vol. 5502.

[96]
Walker, David. (2005).
Advanced topics in types and programming languages.
MIT Press.
Chap. Substructural Type Systems, pages  3–43.

[97]
Williams, Jack, Morris, J. Garrett, Wadler, Philip, & Zalewski, Jakub. (2017).
Mixed messages: Measuring conformance and non-interference in
Pages  28:1–28:29 of: European Conference on
Object-Oriented Programming (ECOOP).
LIPIcs, vol. 74.
Dagstuhl, Germany: Schloss Dagstuhl.

[98]
Willsey, Max, Prabhu, Rokhini, & Pfenning, Frank. (2017).
Design and implementation of concurrent C0.
Pages  73–82 of: International Workshop on Linearity.
EPTCS, vol. 238.

[99]
Wolff, Roger, Garcia, Ronald, Tanter, Éric, & Aldrich, Jonathan. (2011).
Gradual typestate.
Pages  459–483 of: European Conference on Object-Oriented
Programming (ECOOP).
LNCS, vol. 6813.

[100]
Yoshida, Nobuko, & Vasconcelos, Vasco. (2007).
Language primitives and type discipline for structured
communication-based programming revisited: Two systems for higher-order
session communication.
Entcs, 171(4), 73–93.

[101]
Yoshida, Nobuko, Hu, Raymond, Neykova, Rumyana, & Ng, Nicholas. (2014).
The Scribble protocol language.
Pages  22–41 of: International Symposium on Trustworthy
Global Computing.
LNCS, vol. 8358.

§ TYPECHECKING ALGORITHM FOR THE EXTERNAL LANGUAGE

We give a typechecking algorithm for  and show that it is correct.
The typechecking algorithm is slightly involved due to linearity:
$ \textsc{\tyexp}( \Gamma ,  \mathbb{e} ) $ outputs a pair of type $T$ and a
set $X$ of variables, containing the linear variables occurring free in $\mathbb{e}$.

Theorem <ref> states soundness of the typechecking algorithm.
A few lemmas are required in preparation.
Let $ \remove( \Gamma ,  \ottnt{X} ) $ denote
the operation that removes variables $\ottnt{X}$
from a type environment $\Gamma$.

Suppose $y\colon U \in \Gamma$ with $\lin(U)$.

If $ \textsc{\tyexp}( \Gamma ,  \mathbb{e} ) =  \ottnt{T} ,  \ottnt{X} $ and $y \notin X$, then
$ \textsc{\tyexp}(  \remove( \Gamma ,  \ottsym{\{}  \ottmv{y}  \ottsym{\}} )  ,  \mathbb{e} ) =  \ottnt{T} ,  \ottnt{X} $.

By induction on $\mathbb{e}$.
We show one important case below.

Case $\mathbb{e}  \ottsym{=}  \mathbb{e}_{{\mathrm{1}}} \, \mathbb{e}_{{\mathrm{2}}}$: We are given

\[
\Gamma(y) = U \gap
\lin(U) \gap
\textsc{\tyexp}( \Gamma ,  \mathbb{e}_{{\mathrm{1}}} \, \mathbb{e}_{{\mathrm{2}}} ) =  \ottnt{T} ,  \ottnt{X}  \gap
y \notin X.
\]

By the definition of the algorithm,
$ \textsc{\tyexp}( \Gamma ,  \mathbb{e}_{\ottmv{i}} ) =  \ottnt{T_{\ottmv{i}}} ,  \ottnt{X_{\ottmv{i}}} $ for $i = 1, 2$ and

\[
\matching{  \ottnt{T_{{\mathrm{1}}}}  }{   \ottnt{T_{{\mathrm{11}}}}   \rightarrow _{ \ottnt{m} }  \ottnt{T_{{\mathrm{12}}}}   }  \gap
\ottnt{T_{{\mathrm{2}}}}  \lesssim  \ottnt{T_{{\mathrm{11}}}} \gap
\ottnt{T}  \ottsym{=}  \ottnt{T_{{\mathrm{12}}}} \gap
X = X_1 \uplus X_2.
\]

Since $y \notin X$, we have $y \notin X_1$ and $y \notin X_2$.

By $ \textsc{\tyexp}( \Gamma ,  \mathbb{e}_{\ottmv{i}} ) =  \ottnt{T_{\ottmv{i}}} ,  \ottnt{X_{\ottmv{i}}} $ and $y \notin X_i$ and the IH
for $i = 1, 2$, we have

\[
\textsc{\tyexp}(  \remove( \Gamma ,  \ottsym{\{}  \ottmv{y}  \ottsym{\}} )  ,  \mathbb{e}_{{\mathrm{1}}} ) =  \ottnt{T_{{\mathrm{1}}}} ,  \ottnt{X_{{\mathrm{1}}}}  \gap
\textsc{\tyexp}(  \remove( \Gamma ,  \ottsym{\{}  \ottmv{y}  \ottsym{\}} )  ,  \mathbb{e}_{{\mathrm{2}}} ) =  \ottnt{T_{{\mathrm{2}}}} ,  \ottnt{X_{{\mathrm{2}}}} .
\]

Thus, by the definition of the algorithm,
$ \textsc{\tyexp}(  \remove( \Gamma ,  \ottsym{\{}  \ottmv{y}  \ottsym{\}} )  ,  \mathbb{e}_{{\mathrm{1}}} \, \mathbb{e}_{{\mathrm{2}}} ) =  \ottnt{T} ,  \ottnt{X} $.

Suppose $ \flv{ \Gamma }  = X_1 \uplus X_2$.
If $\Gamma_{{\mathrm{1}}}  \ottsym{=}   \remove( \Gamma ,  \ottnt{X_{{\mathrm{2}}}} ) $ and $\Gamma_{{\mathrm{2}}}  \ottsym{=}   \remove( \Gamma ,  \ottnt{X_{{\mathrm{1}}}} ) $, then
$\Gamma  \ottsym{=}   \Gamma_{{\mathrm{1}}}  \circ  \Gamma_{{\mathrm{2}}} $ and
$ \flv{ \Gamma_{{\mathrm{1}}} }   \ottsym{=}  \ottnt{X_{{\mathrm{1}}}}$ and $ \flv{ \Gamma_{{\mathrm{2}}} }   \ottsym{=}  \ottnt{X_{{\mathrm{2}}}}$.

By induction on $\Gamma$.

If $ \textsc{\tyexp}( \Gamma ,  \mathbb{e} ) =  \ottnt{T} ,  \ottnt{X} $ and $ \flv{ \Gamma }   \ottsym{=}  \ottnt{X}$, then
$\Gamma  \vdashG  \mathbb{e}  \ottsym{:}  \ottnt{T}$.

By induction on $\mathbb{e}$.
We show main cases below.

Case $\mathbb{e}  \ottsym{=}   \lambda  _ \ottnt{m}   \ottmv{x} {:} \ottnt{T_{{\mathrm{1}}}} .\,  \mathbb{e}_{{\mathrm{1}}} $: We are given

\[
\textsc{\tyexp}( \Gamma ,   \lambda  _ \ottnt{m}   \ottmv{x} {:} \ottnt{T_{{\mathrm{1}}}} .\,  \mathbb{e}_{{\mathrm{1}}}  ) =  \ottnt{T} ,  \ottnt{X}  \gap
\flv{ \Gamma }   \ottsym{=}  \ottnt{X}.
\]

We consider only when $m = \un$ and $ \lin   \ottsym{(}  \ottnt{T_{{\mathrm{1}}}}  \ottsym{)}$.

By the definition of the algorithm,

\[
\textsc{\tyexp}( \ottsym{(}  \Gamma  \ottsym{,}  \ottmv{x}  \ottsym{:}  \ottnt{T_{{\mathrm{1}}}}  \ottsym{)} ,  \mathbb{e}_{{\mathrm{1}}} ) =  \ottnt{T_{{\mathrm{2}}}} ,  \ottsym{\{}  \ottmv{x}  \ottsym{\}}  \gap
X = \emptyset.
\]

So, $ \flv{ \Gamma }   \ottsym{=}  \ottnt{X} = \emptyset$.
By $ \lin   \ottsym{(}  \ottnt{T_{{\mathrm{1}}}}  \ottsym{)}$, we have $ \flv{ \Gamma  \ottsym{,}  \ottmv{x}  \ottsym{:}  \ottnt{T_{{\mathrm{1}}}} }   \ottsym{=}  \ottsym{\{}  \ottmv{x}  \ottsym{\}}$.

Thus, by the IH, we have $\Gamma  \ottsym{,}  \ottmv{x}  \ottsym{:}  \ottnt{T_{{\mathrm{1}}}}  \vdash  \mathbb{e}_{{\mathrm{1}}}  \ottsym{:}  \ottnt{T_{{\mathrm{2}}}}$.

Here, by $ \flv{ \Gamma }  = \emptyset$, we have $ \un   \ottsym{(}  \Gamma  \ottsym{)}$.
So, $ \super{   \un   }{  \Gamma  } $.
We finish by

\[
\Gamma  \ottsym{,}  \ottmv{x}  \ottsym{:}  \ottnt{T_{{\mathrm{1}}}}  \vdash  \mathbb{e}_{{\mathrm{1}}}  \ottsym{:}  \ottnt{T_{{\mathrm{2}}}} \gap
\super{   \un   }{  \Gamma  }
\]

and the abstraction rule.

Case $\mathbb{e}  \ottsym{=}  \mathbb{e}_{{\mathrm{1}}} \, \mathbb{e}_{{\mathrm{2}}}$: We are given

\[
\textsc{\tyexp}( \Gamma ,  \mathbb{e}_{{\mathrm{1}}} \, \mathbb{e}_{{\mathrm{2}}} ) =  \ottnt{T} ,  \ottnt{X}  \gap
\flv{ \Gamma }   \ottsym{=}  \ottnt{X}.
\]

By the definition of the algorithm,
$ \textsc{\tyexp}( \Gamma ,  \mathbb{e}_{\ottmv{i}} ) =  \ottnt{T_{\ottmv{i}}} ,  \ottnt{X_{\ottmv{i}}} $ for $i = 1,2$ and

\[
\matching{  \ottnt{T_{{\mathrm{1}}}}  }{   \ottnt{T_{{\mathrm{11}}}}   \rightarrow _{ \ottnt{m} }  \ottnt{T_{{\mathrm{12}}}}   }  \gap
\ottnt{T_{{\mathrm{2}}}}  \lesssim  \ottnt{T_{{\mathrm{11}}}} \gap
\ottnt{T}  \ottsym{=}  \ottnt{T_{{\mathrm{12}}}} \gap
X = X_1 \uplus X_2.
\]

Let $\Gamma_{{\mathrm{1}}}  \ottsym{=}   \remove( \Gamma ,  \ottnt{X_{{\mathrm{2}}}} ) $ and $\Gamma_{{\mathrm{2}}}  \ottsym{=}   \remove( \Gamma ,  \ottnt{X_{{\mathrm{1}}}} ) $.
By Lemma <ref>,
$\Gamma  \ottsym{=}   \Gamma_{{\mathrm{1}}}  \circ  \Gamma_{{\mathrm{2}}} $ and
$ \flv{ \Gamma_{{\mathrm{1}}} }   \ottsym{=}  \ottnt{X_{{\mathrm{1}}}}$ and $ \flv{ \Gamma_{{\mathrm{2}}} }   \ottsym{=}  \ottnt{X_{{\mathrm{2}}}}$.

By $ \textsc{\tyexp}( \Gamma ,  \mathbb{e}_{\ottmv{i}} ) =  \ottnt{T_{\ottmv{i}}} ,  \ottnt{X_{\ottmv{i}}} $ and Lemma <ref>, we have $ \textsc{\tyexp}( \Gamma_{\ottmv{i}} ,  \mathbb{e}_{\ottmv{i}} ) =  \ottnt{T_{\ottmv{i}}} ,  \ottnt{X_{\ottmv{i}}} $  for $i = 1,2$.

By $ \flv{ \Gamma_{\ottmv{i}} }   \ottsym{=}  \ottnt{X_{\ottmv{i}}}$ and $ \textsc{\tyexp}( \Gamma_{\ottmv{i}} ,  \mathbb{e}_{\ottmv{i}} ) =  \ottnt{T_{\ottmv{i}}} ,  \ottnt{X_{\ottmv{i}}} $ and the IH, we have $\Gamma_{\ottmv{i}}  \vdash  \mathbb{e}_{\ottmv{i}}  \ottsym{:}  \ottnt{T_{\ottmv{i}}}$ for $i = 1,2$.
We finish by

\[
\Gamma_{{\mathrm{1}}}  \vdash  \mathbb{e}_{{\mathrm{1}}}  \ottsym{:}  \ottnt{T_{{\mathrm{1}}}} \gap
\Gamma_{{\mathrm{2}}}  \vdash  \mathbb{e}_{{\mathrm{2}}}  \ottsym{:}  \ottnt{T_{{\mathrm{2}}}} \gap
\matching{  \ottnt{T_{{\mathrm{1}}}}  }{   \ottnt{T_{{\mathrm{11}}}}   \rightarrow _{ \ottnt{m} }  \ottnt{T_{{\mathrm{12}}}}   }  \gap
\ottnt{T_{{\mathrm{2}}}}  \lesssim  \ottnt{T_{{\mathrm{11}}}}
\]

and the application rule.

We will also show the converse of the theorem above. Completeness
states that $ \textsc{\tyexp}( \Gamma ,  \mathbb{e} ) $ computes a minimal type with respect to
negative subtyping.

If $\Gamma  \vdashG  \mathbb{e}  \ottsym{:}  \ottnt{T}$, then
$ \textsc{\tyexp}( \Gamma ,  \mathbb{e} ) =  \ottnt{T'} ,  \ottnt{X} $ and $ \ottnt{T'}   \Sub^{-}   \ottnt{T} $ and $ \flv{ \Gamma }   \ottsym{=}  \ottnt{X}$ for some $\ottnt{T'}$.

To prove this theorem, we need a stronger statement, namely Lemma <ref>.
We define environment positive consistent subtyping, written $ \Gamma'   \Sub^{-}   \Gamma $, as
$\dom(\Gamma) \subseteq \dom(\Gamma')$ and $\Gamma(\ottmv{x})     \Sub^{-}     \Gamma'(\ottmv{x})$, for any
$\ottmv{x} \in \dom(\Gamma)$.
the theorem follows from the fact that $    \Sub^{-}    $ on type environments
is reflexive.
We start with a few lemmas about $    \Sub^{-}    $.

* If $ \ottnt{T'_{{\mathrm{1}}}}   \Sub^{-}   \ottnt{T_{{\mathrm{1}}}} $ and
$ \matching{  \ottnt{T_{{\mathrm{1}}}}  }{   \ottnt{T_{{\mathrm{11}}}}   \rightarrow _{ \ottnt{m} }  \ottnt{T_{{\mathrm{12}}}}   } $, then there exist some
$\ottnt{T'_{{\mathrm{11}}}}$, $\ottnt{T'_{{\mathrm{12}}}}$, and $n$ such that
$\Call{MatchingFun}{T_1'} =  \ottnt{T'_{{\mathrm{11}}}}   \rightarrow _{ \ottnt{n} }  \ottnt{T'_{{\mathrm{12}}}} $ and
$  \ottnt{T'_{{\mathrm{11}}}}   \rightarrow _{ \ottnt{n} }  \ottnt{T'_{{\mathrm{12}}}}    \Sub^{-}    \ottnt{T_{{\mathrm{11}}}}   \rightarrow _{ \ottnt{m} }  \ottnt{T_{{\mathrm{12}}}}  $.

* If $ \ottnt{T'_{{\mathrm{1}}}}   \Sub^{-}   \ottnt{T_{{\mathrm{1}}}} $ and
$ \matching{  \ottnt{T_{{\mathrm{1}}}}  }{   \ottnt{T_{{\mathrm{11}}}}   \times _{ \ottnt{m} }  \ottnt{T_{{\mathrm{12}}}}   } $, then there exist some
$\ottnt{T'_{{\mathrm{11}}}}$, $\ottnt{T'_{{\mathrm{12}}}}$, and $n$ such that
$\Call{MatchingProd}{T_1'} =  \ottnt{T'_{{\mathrm{11}}}}   \times _{ \ottnt{n} }  \ottnt{T'_{{\mathrm{12}}}} $ and
$  \ottnt{T'_{{\mathrm{11}}}}   \times _{ \ottnt{n} }  \ottnt{T'_{{\mathrm{12}}}}    \Sub^{-}    \ottnt{T_{{\mathrm{11}}}}   \times _{ \ottnt{m} }  \ottnt{T_{{\mathrm{12}}}}  $.

* If $ \ottnt{T'_{{\mathrm{1}}}}   \Sub^{-}   \ottnt{T_{{\mathrm{1}}}} $ and
$ \matching{  \ottnt{T_{{\mathrm{1}}}}  }{   \pl{ \ottnt{T_{{\mathrm{11}}}} }  \ottnt{S_{{\mathrm{12}}}}   } $, then there exist some
$\ottnt{T'_{{\mathrm{11}}}}$ and $\ottnt{S'_{{\mathrm{12}}}}$ such that

$\Call{MatchingSend}{T_1'} =  \pl{ \ottnt{T'_{{\mathrm{11}}}} }  \ottnt{S'_{{\mathrm{12}}}} $ and
$  \pl{ \ottnt{T'_{{\mathrm{11}}}} }  \ottnt{S'_{{\mathrm{12}}}}    \Sub^{-}    \pl{ \ottnt{T_{{\mathrm{11}}}} }  \ottnt{S_{{\mathrm{12}}}}  $.

* If $ \ottnt{T'_{{\mathrm{1}}}}   \Sub^{-}   \ottnt{T_{{\mathrm{1}}}} $ and
$ \matching{  \ottnt{T_{{\mathrm{1}}}}  }{   \qu{ \ottnt{T_{{\mathrm{11}}}} }  \ottnt{S_{{\mathrm{12}}}}   } $, then there exist some
$\ottnt{T'_{{\mathrm{11}}}}$ and $\ottnt{S'_{{\mathrm{12}}}}$ such that

$\Call{MatchingReceive}{T_1'} =  \qu{ \ottnt{T'_{{\mathrm{11}}}} }  \ottnt{S'_{{\mathrm{12}}}} $ and
$  \qu{ \ottnt{T'_{{\mathrm{11}}}} }  \ottnt{S'_{{\mathrm{12}}}}    \Sub^{-}    \qu{ \ottnt{T_{{\mathrm{11}}}} }  \ottnt{S_{{\mathrm{12}}}}  $.

* If $ \ottnt{T'_{{\mathrm{1}}}}   \Sub^{-}   \ottnt{T_{{\mathrm{1}}}} $ and
$ \matching{  \ottnt{T_{{\mathrm{1}}}}  }{   \oplus    \br{  \ottmv{l_{\ottmv{j}}}  :  \ottnt{S_{\ottmv{j}}}  }    } $, then there exist some
$\ottnt{S'_{\ottmv{j}}}$ such that

$\Call{MatchingSelect}{T_1', l_j} =  \oplus    \br{  \ottmv{l_{\ottmv{j}}}  :  \ottnt{S'_{\ottmv{j}}}  }  $ and
$  \oplus    \br{  \ottmv{l_{\ottmv{j}}}  :  \ottnt{S'_{\ottmv{j}}}  }     \Sub^{-}    \oplus    \br{  \ottmv{l_{\ottmv{j}}}  :  \ottnt{S_{\ottmv{j}}}  }   $.

* If $ \ottnt{T'_{{\mathrm{1}}}}   \Sub^{-}   \ottnt{T_{{\mathrm{1}}}} $ and
$ \matching{  \ottnt{T_{{\mathrm{1}}}}  }{   \&    \br{  \ottmv{l_{{\mathrm{1}}}} : \ottnt{S_{{\mathrm{1}}}} , \dots ,  \ottmv{l_{\ottmv{k}}} : \ottnt{S_{\ottmv{k}}}  }    } $, then there exist some
$\ottnt{S'_{{\mathrm{1}}}}, \ldots, \ottnt{S'_{\ottmv{k}}}$ such that
$\Call{MatchingCase}{T_1', \br{l_1,\ldots, l_k}} =  \&    \br{  \ottmv{l_{{\mathrm{1}}}} : \ottnt{S'_{{\mathrm{1}}}} , \dots ,  \ottmv{l_{\ottmv{k}}} : \ottnt{S'_{\ottmv{k}}}  }  $ and
$  \&    \br{  \ottmv{l_{{\mathrm{1}}}} : \ottnt{S'_{{\mathrm{1}}}} , \dots ,  \ottmv{l_{\ottmv{k}}} : \ottnt{S'_{\ottmv{k}}}  }     \Sub^{-}    \&    \br{  \ottmv{l_{{\mathrm{1}}}} : \ottnt{S_{{\mathrm{1}}}} , \dots ,  \ottmv{l_{\ottmv{k}}} : \ottnt{S_{\ottmv{k}}}  }   $.

By case analysis on $ \matching{  \ottnt{T}  }{  \ottnt{U}  } $.

If $ \ottnt{T}   \Sub^{-}   \ottnt{U} $ and $ \un   \ottsym{(}  \ottnt{U}  \ottsym{)}$, then $ \un   \ottsym{(}  \ottnt{T}  \ottsym{)}$.

By case analysis on $ \ottnt{T}   \Sub^{-}   \ottnt{U} $.

* If $ \ottnt{T_{{\mathrm{1}}}}   \Sub^{-}   \ottnt{T_{{\mathrm{2}}}} $ and $\ottnt{T_{{\mathrm{2}}}}  \lesssim  \ottnt{T_{{\mathrm{3}}}}$, then $\ottnt{T_{{\mathrm{1}}}}  \lesssim  \ottnt{T_{{\mathrm{3}}}}$.

* If $\ottnt{T_{{\mathrm{1}}}}  \lesssim  \ottnt{T_{{\mathrm{2}}}}$ and $ \ottnt{T_{{\mathrm{2}}}}   \Sub^{+}   \ottnt{T_{{\mathrm{3}}}} $, then $\ottnt{T_{{\mathrm{1}}}}  \lesssim  \ottnt{T_{{\mathrm{3}}}}$.

Both items are proved by simultaneous induction on $ \lesssim $.

If $\Gamma  \vdashG  \mathbb{e}  \ottsym{:}  \ottnt{T}$ and $ \Gamma'   \Sub^{-}   \Gamma $, then
there exists $\ottnt{T'}$ such that
$ \textsc{\tyexp}( \Gamma' ,  \mathbb{e} ) =  \ottnt{T'} ,  \ottnt{X} $ and $ \ottnt{T'}   \Sub^{-}   \ottnt{T} $ and $ \flv{ \Gamma }   \ottsym{=}  \ottnt{X}$.

By induction on $\mathbb{e}$.  We show main cases below.

Case $\mathbb{e} = \mathbb{e}_{{\mathrm{1}}} \, \mathbb{e}_{{\mathrm{2}}}$:

By inversion of the typing relation,
$\Gamma_{{\mathrm{1}}}  \vdashG  \mathbb{e}_{{\mathrm{1}}}  \ottsym{:}  \ottnt{T_{{\mathrm{1}}}}$ and
$\Gamma_{{\mathrm{2}}}  \vdashG  \mathbb{e}_{{\mathrm{2}}}  \ottsym{:}  \ottnt{T_{{\mathrm{2}}}}$ and
$\Gamma = \Gamma_{{\mathrm{1}}} \circ \Gamma_{{\mathrm{2}}}$ and
$ \matching{  \ottnt{T_{{\mathrm{1}}}}  }{   \ottnt{T_{{\mathrm{11}}}}   \rightarrow _{ \ottnt{m} }  \ottnt{T_{{\mathrm{12}}}}   } $ and
$\ottnt{T_{{\mathrm{2}}}}  \lesssim  \ottnt{T_{{\mathrm{11}}}}$
for some $\Gamma_{{\mathrm{1}}}$, $\Gamma_{{\mathrm{2}}}$, $\ottnt{T_{{\mathrm{1}}}}$, $\ottnt{T_{{\mathrm{2}}}}$, $\ottnt{T_{{\mathrm{11}}}}$, $\ottnt{T_{{\mathrm{12}}}}$, and $\ottnt{m}$.

It is easy to show $ \Gamma'   \Sub^{-}   \Gamma_{{\mathrm{1}}} $ and $ \Gamma'   \Sub^{-}   \Gamma_{{\mathrm{2}}} $.

By the induction hypothesis, for some $\ottnt{T'_{{\mathrm{1}}}}$, $\ottnt{T'_{{\mathrm{2}}}}$, $X$, and $Y$,
$T_1', X =$ $\Gamma', \mathbb{e}_{{\mathrm{1}}}$ and $ \ottnt{T'_{{\mathrm{1}}}}   \Sub^{-}   \ottnt{T_{{\mathrm{1}}}} $ and $ \flv{ \Gamma_{{\mathrm{1}}} }   \ottsym{=}  \ottnt{X}$ and
$T_2', Y =$ $\Gamma', \mathbb{e}_{{\mathrm{2}}}$ and $ \ottnt{T'_{{\mathrm{2}}}}   \Sub^{-}   \ottnt{T_{{\mathrm{2}}}} $ and $ \flv{ \Gamma_{{\mathrm{2}}} }   \ottsym{=}  \ottnt{Y}$.

Since $\Gamma_{{\mathrm{1}}} \circ \Gamma_{{\mathrm{2}}}$ is well defined, $X \cap Y$ must be $\emptyset$.

By Lemma <ref>,
$ \ottnt{T'_{{\mathrm{11}}}}   \rightarrow _{ \ottnt{n} }  \ottnt{T'_{{\mathrm{12}}}}  =$ MatchingFun$T_1'$ and
$  \ottnt{T'_{{\mathrm{11}}}}   \rightarrow _{ \ottnt{n} }  \ottnt{T'_{{\mathrm{12}}}}    \Sub^{-}    \ottnt{T_{{\mathrm{11}}}}   \rightarrow _{ \ottnt{m} }  \ottnt{T_{{\mathrm{12}}}}  $ for some $\ottnt{T'_{{\mathrm{11}}}}$ and $\ottnt{T'_{{\mathrm{12}}}}$.

By inversion of $    \Sub^{-}    $,
we have $ \ottnt{T_{{\mathrm{11}}}}   \Sub^{+}   \ottnt{T'_{{\mathrm{11}}}} $ and $ \ottnt{T'_{{\mathrm{12}}}}   \Sub^{-}   \ottnt{T_{{\mathrm{12}}}} $.

Then, $\ottnt{T'_{{\mathrm{2}}}}  \lesssim  \ottnt{T'_{{\mathrm{11}}}}$ is shown by Lemma <ref>.

It is easy to show $X \cup Y =  \flv{ \Gamma } $ because $\Gamma = \Gamma_{{\mathrm{1}}} \circ \Gamma_{{\mathrm{2}}}$.

Finally, $ \ottnt{T'_{{\mathrm{12}}}}   \Sub^{-}   \ottnt{T_{{\mathrm{12}}}} $ finishes the case.

Case $\mathbb{e} =  \case{ \mathbb{e}_{{\mathrm{0}}} }{  \br{  \ottmv{l_{\ottmv{j}}} :  \ottmv{x_{\ottmv{j}}} .\,  \mathbb{e}_{\ottmv{j}}   }_{  \ottmv{j}  \in  \ottnt{J}  }  } $:

By inversion of the typing relation, we have
$\Gamma_{{\mathrm{1}}}  \vdashG  \mathbb{e}_{{\mathrm{0}}}  \ottsym{:}  \ottnt{T_{{\mathrm{0}}}}$ and
$ \matching{  \ottnt{T_{{\mathrm{0}}}}  }{   \&    \br{  \ottmv{l_{\ottmv{j}}}  :  \ottnt{R_{\ottmv{j}}}  }_{  \ottmv{j}  \in  \ottnt{J}  }    } $ and
$(\Gamma_{{\mathrm{2}}}  \ottsym{,}  \ottmv{x_{\ottmv{j}}}  \ottsym{:}  \ottnt{R_{\ottmv{j}}}  \vdashG  \mathbb{e}_{\ottmv{j}}  \ottsym{:}  \ottnt{U_{\ottmv{j}}})_{\ottmv{j} \in \ottnt{J}}$ and
$\ottnt{T} =  \vee \br{\ottnt{U_{\ottmv{j}}}}_{\ottmv{j}\in \ottnt{J}}$ and
$\Gamma = \Gamma_{{\mathrm{1}}} \circ \Gamma_{{\mathrm{2}}}$ for some
$\Gamma_{{\mathrm{1}}}$, $\Gamma_{{\mathrm{2}}}$, $\ottnt{R_{\ottmv{j}}}$, and $\ottnt{U_{\ottmv{j}}}$ (for $\ottmv{j} \in \ottnt{J}$).

It is easy to show $ \Gamma'   \Sub^{-}   \Gamma_{{\mathrm{1}}} $ and $ \Gamma'   \Sub^{-}   \Gamma_{{\mathrm{2}}} $.

By the induction hypothesis,
$T_0', X =$ $\Gamma', \mathbb{e}_{{\mathrm{0}}}$ and $ \ottnt{T'_{{\mathrm{0}}}}   \Sub^{-}   \ottnt{T_{{\mathrm{0}}}} $ and $ \flv{ \Gamma_{{\mathrm{1}}} }   \ottsym{=}  \ottnt{X}$
for some $\ottnt{T'_{{\mathrm{0}}}}$ and $X$.

By Lemma <ref>,
$\Call{MatchingCase}{T_0', \br{l_1,\ldots, l_k}} =  \&    \br{  \ottmv{l_{{\mathrm{1}}}} : \ottnt{R'_{{\mathrm{1}}}} , \dots ,  \ottmv{l_{\ottmv{k}}} : \ottnt{R'_{\ottmv{k}}}  }  $ and
$  \&    \br{  \ottmv{l_{\ottmv{j}}}  :  \ottnt{R'_{\ottmv{j}}}  }_{  \ottmv{j}  \in  \ottnt{J}  }     \Sub^{-}    \&    \br{  \ottmv{l_{\ottmv{j}}}  :  \ottnt{R_{\ottmv{j}}}  }_{  \ottmv{j}  \in  \ottnt{J}  }   $ for some $(\ottnt{R'_{\ottmv{j}}})_{\ottmv{j} \in \ottnt{J}}$.

By inversion of $    \Sub^{-}    $, we have $( \ottnt{R'_{\ottmv{j}}}   \Sub^{-}   \ottnt{R_{\ottmv{j}}} )_{\ottmv{j} \in \ottnt{J}}$.

By the induction hypothesis,  for any $\ottmv{j} \in \ottnt{J}$,
there exist $\ottnt{U'_{\ottmv{j}}}$ and $Y_j$ such that
$U_j', Y_j =$ $(\Gamma', \ottmv{x_{\ottmv{j}}}:\ottnt{R'_{\ottmv{j}}}), \mathbb{e}_{\ottmv{j}}$ and $ \ottnt{U'_{\ottmv{j}}}   \Sub^{-}   \ottnt{U_{\ottmv{j}}} $
and $ \flv{ \Gamma_{{\mathrm{2}}}  \ottsym{,}  \ottmv{x_{\ottmv{j}}}  \ottsym{:}  \ottnt{R_{\ottmv{j}}} }   \ottsym{=}  \ottnt{Y_{\ottmv{j}}}$.

It is easy to show that $x_j \in Y_j$ for any $\ottmv{j} \in \ottnt{J}$
and $Y_1 = \cdots = Y_k$ and $X \cap Y_1 = \emptyset$
because $\ottnt{R_{\ottmv{j}}}$ is linear and $\Gamma_{{\mathrm{1}}} \circ \Gamma_{{\mathrm{2}}}$ is well defined.

It is also easy to show $X \cup (Y_1 \setminus \br{\ottmv{x_{{\mathrm{1}}}}}) =  \flv{ \Gamma } $ because $\Gamma = \Gamma_{{\mathrm{1}}} \circ \Gamma_{{\mathrm{2}}}$.

Finally, $ \vee \br{\ottnt{U'_{\ottmv{j}}}}_{\ottmv{j} \in \ottnt{J}}     \Sub^{-}      \vee \br{\ottnt{U_{\ottmv{j}}}}_{\ottmv{j} \in \ottnt{J}}$
is shown by Lemma <ref>.