基于结构化通信编程的会话类型和类型安全验证

理论计算机科学电子笔记171（2007）73-93www.elsevier.com/locate/entcs基于结构化通信编程的语言原语和类型规则两个系统高阶会话通信吉田伸子伦敦帝国理工学院瓦斯科·T Vasconcelos2里斯本大学摘要会话原语和类型为结构化交互提供了一种灵活的编程风格，并用于静态检查以通信为中心的分布式软件中协议的安全性和一致性不幸的是，作者工作的会话类型最近意识到，一些以前公布的系统不能满足基本定理的主题减少和类型安全。本文讨论了高阶会话通信所涉及的问题，给出了递归类型的公式，并证明了Honda-Vasconcelos-Kubo在ESOP'98中提出的原始会话类型系统它还提出了一个变体，允许更自由的高阶会话通信，基于Gay和Hole的想法。关键词：Pi演算，会话类型，协议分析，主题归约定理，类型安全，重写系统1引言会话原语和类型为结构化交互提供了一种灵活的编程风格，并用于静态检查以通信为中心的分布式软件中协议的安全性和一致性。它们已经被研究用于π演算[2，11，12，13，17，20，23]，Ambients [6]，CORBA接口[21]，多线程函数语言[15，23，24]，Web描述语言[3，4，14]，1电子邮件地址：yoshida@doc.ic.ac.uk2 电子邮件地址：vv@di.fc.ul.pt1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2007.02.05674N. 吉田，V.T.Vasconcelos/Electronic Notes in Theoretical Computer Science 171（2007）73分布式[8]和多线程Java [7]，以及行业级别的WC 3- CDL [5，25]和pi 4 Tech [16]。本文报道了近年来在会话类型研究中对两个基本理论--主题归约和类型安全的讨论。在存在高阶会话通信的情况下，会话实例化动态地改变会话的结构，使得预服务可类型性变得不平凡不幸的是，上述作者最近意识到，以前的一些系统不能满足这些基本定理。有趣的是，类型保持的微妙之处与π演算重写规则中通信通道的处理有关。在讨论了高阶会话通信中涉及的问题之后，该报告还提出了一种会话类型系统，该系统允许更自由的高阶会话通信，该系统基于Gay和Hole [12]的工作并已在[23]中使用。这两个定理的充分证明首先在本报告中给出，这也澄清了[13]中缺少的一些定义。为什么现在的作者应该在九年后重新证明的动机是发现了一个微妙的反例，这个反例是在考虑工作之后发表的一些关于会话类型的工作中的结果，尽管不是原始系统的结果[13]。我们将在第3节中详细解释这个问题。本报告的技术贡献包括：递归类型的公式化，Honda-Vasconcelos-Kubo [13]在原始会话类型系统中证明了主语归约和类型安全定理，以及提出了一个更自由的系统和相应的证明。论文的大纲很简单。下一节回顾了员工持股计划'98系统，为上述结果提供了证据。第3节介绍了更自由的制度。第四部分是论文的结论。2Honda-Vasconcelos-Kubo会话打字系统Honda-Vasconcelos-Kubo我们首先非正式地回顾了ESOP系统的语法、操作语义和类型系统。然后，我们陈述并证明了主要定理，主题约简和类型安全。语言和打字系统的详细示例和解释可以在参考文献[13]中找到2.1语义和操作语义会话是两方之间的一系列相互交互，可能具有分支和递归，并且用作描述交互的抽象单元。属于会话的通信通过特定于该会话的端口执行，称为通道。在启动每个会话时生成一个新的信道，用于安全通信。N. 吉田，V.T.Vasconcelos/Electronic Notes in Theoretical Computer Science 171（2007）7375P：：=在P会话请求中请求a（k）| accept a (k) in Psession acceptance| k! [e];Pdat a sending| k? （x）在Pdataretion中| k l; Plabel selection| k D {l1: P1 [] ··· [] ln: Pn}label branching| throw k [kJ]; Pchannel sending| catch k (kJ) in Pchannel reception| if e then P else Qconditional branch| P|Q平行合成| inactinaction| (νu) Pname/channel hiding| def D in Precursion| X[e˜k˜]processvariablese：：=c常数| e + eJ| e−eJ| e×e| 不（e）|......这是什么？运营商D：：=X1（x<$1k<$1）=P1和·· ·和Xn（x<$nk<$n）=PnFig. 1. 语法我们使用以下基集：名称，由a，b，x，y，z ...... ;通道，范围为k，kJ;常量（包括名称、整数和布尔值），范围为c，cJ，. 标签，由l，LJ，. 和过程变量，由X、Y、. 字母u，uJ，. 将名称和频道一起表示。然后，过程，由P，Q…，和表达式，由e，eJ，. 由图1中的语法给出。图6中的类型化系统确保在进程X[e]中，chan_n_el_i_n_iP<$Q如果P<$αQP|不起作用的PP|QQ |P（P|Q）|RP|（Q|R）（νu）P|Q（νu）（P |Q）如果u/∈ fu（Q）（v u）inactinactdefDininactinact（νu）defDinP<$defDin（νu）Pifu/∈ fu（D）（defDinP）|在（P）中的Q定义D|Q） 如果dpv（D）= fpv（Q）defDin（defDJinP）如果dpv（D）≠ dpv（DJ）= 0，则在P中定义D和D j。图二、结构同余76N. 吉田，V.T.Vasconcelos/Electronic Notes in Theoretical Computer Science 171（2007）73对一个人的约束是什么？（x∈ k）在P中，X（x∈k）=P，且d（νa）P;N. 吉田，V.T.Vasconcelos/Electronic Notes in Theoretical Computer Science 171（2007）7377（接受P1中的a（k））|（要求在P2中列入a（k）） → （νk）（P1|P2）[L INK]（k！[e];P1）|（k？（x）inP2）→P1|P2[c/x]（e↓c）[COM]（千美元）（i; P）|（kD{l1：P1 []···[] ln：Pn}）→P|Pi （1 ≤i ≤ n）[L ABEL]（throwk [kJ]; P1）| （在P 2中捕获k（kJ））→P1|P2[PASS]ifethenP1elseP2→ P1（e ↓ true）[I F 1]ifethenP1elseP2→ P2（e ↓ false）[I F2] defDin（X[ek]|Q）→defDin（P[c/x]|Q）（e<$↓c<$，X（x<$k<$）=P∈D）[DEF]P→PJ⇒（νu）P→（νu）PJ[SCOP]P→Pj P|Q→PJ|Q[PAR]P→PjdefDinP→defDinPJ[DEFIN]P<$PJ andPJ→QJ andQJ<$Q<$P→Q[STR]图三. 减少其中，对于过程变量，则是在P中请求a（k），在P中接受a（k），在P中捕获k（kJ），X（x<$k<$）=P，以及（v k）P;衍生出的约束和自由标识符、alpha等价性和替换的概念是标准的。对于P进程，fpv（P）表示自由进程变量集，fn（P）表示自由名称集，fc（P）表示自由通道集。 我们还定义了fu（P）= fn（P）<$fc（P）。我们还需要讨论在声明中引入的流程变量集dpv（X1（x<$1k<$1）=P1and·· ·andXn（x<$nk<$n）=Pn）={X1， . . ，Xn}。结构全等是包含图2中方程的过程的最小全等关系。操作语义由归约关系给出，记为P→Q，这是由图3中的规则生成的过程上的最小关系，其中e↓c表示表达式e的值为常数c。规则[LINK]通过共享名称a在P1中的服务器接受a（k）和P2中的客户端请求a（k）之间建立新会话。规则[COM]在私有信道上在客户端和服务器之间传输值，以便在双方之间确保值传递的确定性。规则[PASS]是允许更高阶会话通信的关键规则，即会话信道发送和接收，用它来表达各种协议，允许复杂的嵌套结构通讯例如，要显示频道和名称之间的差异在P1中接受a（k）|在P2中接受a（k）|在Q中请求a（k）被类型系统接受，而throwk [kJ]; P1|throwk [kJ]; P2|catchk（kJ）in Q78N. 吉田，V.T.Vasconcelos/Electronic Notes in Theoretical Computer Science 171（2007）73是禁止的，因为上下文中同时出现了两个字母k。N. 吉田，V.T.Vasconcelos/Electronic Notes in Theoretical Computer Science 171（2007）7379SortS：：= nat| bool| α，αTypeα：：=？[S];α|什么？[α];β|&{11：α1， . . . ，ln：αn}|端|⊥|！[S]; α|！[α]; β|{11：α1， . . ，ln：αn}|不|μ t。α见图4。 类型的语法与π-演算规则[PASS]的本质与π演算的一个变体的操作语义规则中的“技巧”有关此演算将名称传递限制为绑定（私有）名称传递。从语法上讲，它将输出限制为以下形式：（vy）（x y）|P）在具有智能的情况下（1）where y =y1. . . 虽然我不想让任何人知道我的意思，|dénotesparallcomposi-tion，anddxbrowserisanasynchronous utut（ora m e ss age）. 我们将（1）中的过程写成x（y）。P. 这一天，一个微处理器通过对绑定输出的剩余约束来获得流。x（y）。P|x（y）。Q→（νyθ）（P|（2）不一定要在输入和输出端中进行预处理，而是在通信之前隐式地执行预处理可以容易地观察到该规则与规则[LINK]和[PASS]之间的相似性：通道k总是新生成的在规则[L_INK]中，并且规则[P_ASS]中的通道k_J已经被创建并绑定在以前的互动。 因此，在（2）、[LINK]或[PASS]中不执行替换。2.2类型学科基于结构化通信的编程允许超越传统通信原语的复杂交互结构的清晰描述。交互变得越复杂，就越难捕捉整个交互行为并编写正确的程序。会话类型规程提供了一个简单的静态检查框架，以保证在这种情况下通信模式的正确性。它保证了良好类型的程序在交互模式中不受不兼容性的影响。类型给定一组类型变量，其范围为t，tJ，. ，图4中的文法定义了由S，SJ，. . ，而类型集T的取值范围为α，β，. .你说什么？[S];arettebhaviorofittingaluss[α]; β表示一个简单的字符串，其中字符串是在字符串中输入的（字符串）;类型是！[S];αand！[α];βaredualof？[S];αnd！[α];β，在茶的提取过程中，TYPE80N. 吉田，V.T.Vasconcelos/Electronic Notes in Theoretical Computer Science 171（2007）73！[S];α =？[S];α{li：αi}i∈I=&{li：αi}i∈I！[α];β=？[α];β？[S];α =！[S];α&{li：αi}i∈I=<${li：αi}i∈I？[α];β=！[α];βend=endμt.α=μt.α t=t图五. 同类型一个类型&{11：α1，.，ln：αn}描述了一个分支行为：它等待n个选项，如果第i个操作被选择（外部选择），则表现为类型α i;类型{l1：α1，.，ln：αn}则表示将选择l i中的一个并且然后根据所选择的li（内部选择）表现为α i的行为。 类型end表示不作为，作为顺序组合的单位;μt.α表示递归行为，表示从执行α开始的行为，当遇到t时，递归到 再次是α;最后，α是一个特殊类型，表明在给定的名称上不可能有进一步的相互作用。对于一个不出现α的类型α，我们定义α，α的余型（或对偶），通过交换！然后呢？和和。归纳定义见图5。递归类型本摘要的贡献之一是对递归类型的精确定义和不动点定理，这在原始论文中被省略了我们遵循递归类型的标准共归纳处理[18]。μ运算符是一个绑定器，以标准的方式产生了绑定变量和自由变量以及α等价的概念。我们不区分阿尔法转换类型。 此外，我们对类型采取等递归的观点，而不是区分类型μt.α与其展开α[μt.α/t]之间的关系我们感兴趣的是收缩只有类型。定义2.1（压缩）一个类型是压缩的，如果对于它的每个子表达式μt.μt1.μtn.α，物体α不是t。我们假设所有类型都是收缩的。定义2.2（类型等价）两个类型α和β被称为等价，如果对（α，β）在单调函数F的最大定点：P（T × T）→N. 吉田，V.T.Vasconcelos/Electronic Notes in Theoretical Computer Science 171（2007）7381P（T × T）定义为：F（R）={（end，end），（n，n）}{（？[S]; α，？[S]; β）|（α，β）∈R}{（！[S]; α，！[S]; β）|（α，β）∈R}{（？[α];β，？[αJ]; βJ）|（α，αJ），（β，βJ）∈R}{（！[α];β，！[αJ]; βJ）|（α，αJ），（β，βJ）∈R}<${（<${li：αi}i∈I，<${li：βi}i∈I）|（αi，βi）∈R，<$i ∈ I}<${（&{li：αi}i∈I，&{li：βi}i∈I）|（αi，βi）∈ R，<$i ∈ I}{（μt.α，β）|（α [μt.α/t]，β）∈R}{（α，μt.β）|（α，β [μt.β/t]）∈R}定理2.3函数F的最大不动点是一个等价关系。证据对于这三种情况（反射性、对称性、传递性）中的每一种，我们遵循[18]，定理21.3.6-7。以对称性为例。一个关系R是对称的，如果它在单调函数Sym（R）={（α，β}）下是闭的|（β，α）∈R}.我们首先注意到（cf。[18]，定理21.3.6）：Sym（F（R））<$F（Sym（R））意味着F的最大不动点是对称的。然后我们证明Sym（F（R））<$F（Sym（R））。设（α，β）∈Sym（F（R））.通过Sym的定义，存在（β，α）∈F（R）. 我们的目标是证明（β，α）∈F（Sym（R））. 考虑α的所有可能形状。我们只关注两个案例，其余的都是类似的。情况α =结束。 由于（β，α）∈ F（R），F的定义意味着β = end或β = μt.γ，其中（α，γ [β/t]）∈ R。在第一种情况下，注意对于任何R，特别是对于F（Sym（R）），（end，end）∈F（R在第二种情况下，我们知道（γ[β/t]，α）∈Sym（R）（根据Sym的定义），因此（β，α）∈F（Sym（R））（根据F的定义）。情形α =&{li：αi}i∈I。 由于（β，α）∈F（R），F的定义意味着：β={li：βi}i∈I或β=μt.γ，其中（α，γ[β/t]）∈R.在第一种情况下，根据定义，对于Sym，对于所有i∈I，我们有（βi，αi）∈Sym（R），因此（{li：βi}i∈I，{li：αi}i∈I）∈F（Sym（R））。 在第二种情况下，按上述方法进行。阻碍类型被理解为直到类型等价，因此，例如，在类型推导中，类型μt.α和α[μt.α/t]可以互换使用。由于在类型（{l1：α1，.，ln：αn}，&{l1：α1，.，ln：αn}），我们不追求将类型解释为正则有限树（感兴趣的读者可以参考[22]了解这种解释）。分型系统排序（分别为a打字，abasis）是一个从名称到排序的有限部分映射（分别为从渠道到类型，从变量到排序和类型的序列）。我们让Γ，Γ J，. （分别）Δ，Δ J，.. . ，相应地。Θ，Θ J，. . ）范围超过排序（分别打字，基地）。82N. 吉田，V.T.Vasconcelos/Electronic Notes in Theoretical Computer Science 171（2007）73Γ·a：SadSΓ1dnatΓtrue，falsedbool我的祖国Γ1+e2dnatΘ;rP dΔ·k：结束Δ完成[名称I]，[NAT]，[BOOL]，[SUM][BOT]，[INACT]Θ;rPdΔ·k：θ;rinactdΔradα，αθ;rP dΔ·k：αΘ; Γθ在P d Δ中接受a（k）radα，αθ;rP dΔ·k：αΘ; r_i在P d Δ中请求a（k）[ACC][RE q]ΓedSθ;ΓPdΔ·k：α你好！[e];PdΔ·k：！[S];α[SEND]Θ;Γ·x：SPdΔ·k：αΘ;rk？（x）inPdΔ·k：？[S];α[RCV]Θ;ΓP1dΔ·k：α1···Θ;ΓPndΔ·k：αnΘ;r = k D {11：P1 []···[] ln：Pn} d Δ·k：&{11：α1，. ，ln：αn}[BR]Θ; ΓP dΔ·k：αjΘ;rklj; P d Δ·k：n {l1：α1，.，ln：αn}Θ; rP dΔ·k：β（1≤j≤n）[SEL][THR]Θ; r=throwk [kJ];Pd Δ·k：！[α];β·kJ：αΘ;ΓP dΔ·k：β·kJ：αΘ; Γ在Pd Δ·k中捕捉k（kJ）：[α];β[CAT]Θ; rP dΔΘ; rQdΔJJΘ;γP|QdΔ ΔJ（Δ= Δ）[C ONC]Γ-化boolΘ; Γ-化Pd Δ Θ; Γ-化Qd Δ如果e则P，否则QdΔ[IF]Θ; r·a：SPdΔ Θ; r（νa）P dΔΘ; rP dΔ·k：θΘ; γ （νk）P dΔ[NRES]，[CRES]ΔcompletedredSΘ·X：S<$α<$; Γ<$X[e<$k<$]dΔ·k<$：α<$[VAR]Θ·X：Sα; Γ·x：SPdk：αθ·X：Sα; ΓQ dΔΘ;rdefX（xk）=PinQ dΔ[DEF]见图6。 分型系统定义2.4（型代数）类型Δ 0和Δ 1相容，记为Δ 0=Δ 1，如果Δ 0（k）= Δ 1（k）对N. 吉田，V.T.Vasconcelos/Electronic Notes in Theoretical Computer Science 171（2007）7383所有k∈ dom（Δ 0）dom（Δ 1）。当Δ 0=Δ 1时，Δ 0和Δ 1的合成，记作Δ 0<$Δ 1，给出为一个类型使得（Δ 0<$Δ 1）（k）是（1）<$，如果k∈ dom（Δ 0）<$dom（Δ 1）;（2）Δ i（k），如果k∈ dom（Δ i）\dom（Δ i+1mod2），其中i∈ {0，1};（3）否则未定义。84N. 吉田，V.T.Vasconcelos/Electronic Notes in Theoretical Computer Science 171（2007）73当k/∈dom（Δ）时，我们记为Δ·k：α然后将该符号扩展为Δ· ΔJ。此外，Θ|x表示从Θ取θ |x：Θ（x）的结果同样，对于r\a和Δ\k。类型判断具有形式Θ; ΓP dΔ，其表示：“在条件Θ; Γ下，过程P具有类型Δ"。类型系统由图6中的公理和规则定义。当一个类型只包含结束类型时，我们称之为类型完成[12]。规则[VAR]和[INACT]确保每个派生树中的叶子只包含完整的类型（然后，可以通过规则[BOT]插入）。我们还将递归定义简化为单一情况;将扩展到多个情况。递归是显而易见的。2.3ESOP'98系统的变化对于语法，我们添加了x，y，z，. 到名称的类别，从而将变量的集合合并到名称的集合。我们已经明确了微积分中各种标识符对于结构同余关系，我们用dpv（D）代替了fpv（D），dpv（D）是在声明D中引入的变量集，并且我们在inact中添加了规则defD，以实现灵活性。对于类型，我们将语法从1改为end，从↑改为！，从↓到？， 后[12]。 我们还为递归类型添加了更准确的定义（定义2.1和2.2），澄清。对于打字系统，我们增加了[NAME I]、[NAT]、[BOOL]、[SUM]，并修订了[ACC]、[RE q]、[VAR]、[DEF]。所有这些变化都是改进，并不意味着与[13]有任何技术差异。然而，在打字系统方面有一个重要的补充[13]《易经》：“君子之道，焉可诬也？有始有终。没有[BOT]-规则，主语全等（引理2.9）就不成立。以进程throwk[kJ]; inact为例|不活动结构全等的抛出k[kJ]的;无效的 我们有► 投出k[kJ];不动作|inact dk：！[end]; end·kJ：但是进程throwk[kJ];inact在相同的类型下是不可类型化的[1]。 在[2]中，作者通过在[THR]规则中添加条件βend来解决这个问题我们我相信这里的解决方案提供了额外的灵活性。2.4主题缩减和类型安全我们从一些辅助结果开始;主题缩减在第11页，类型安全在第13页。引理2.5（弱化引理）设Θ; r ∈P d Δ。(i) 若X/∈dom（Θ），则有 X：S<$α<$; Γ<$PdΔ.(ii) 如果a/∈ dom（Γ），则Θ; Γ，a：S <$P d Δ。(iii) 若k/∈dom（Δ）且α =∞或α =end，则Θ; Γ∈ Pd Δ·k：α.证据对每一个图的导出树作了简单的归纳。对于iii，我们注意到在[INACT]和[VAR]中，Δ只包含end。N. 吉田，V.T.Vasconcelos/Electronic Notes in Theoretical Computer Science 171（2007）73851引理2.6（加强引理）设Θ; r ∈P d Δ。(i) 若X/∈ fpv（P），则Θ\X;Γ ∈ Pd Δ。(ii) 如果a/∈ fn（P），则Θ; r\a ∈ P d Δ。(iii) 如果k/∈fc（P），则Θ; Γ∈ P d Δ\k。证据 标准引理2.7（通道引理）（i）如果Θ; r∈Pd Δ·k：α且k/∈fc（P），则α= α，结束。(ii) 若Θ; Γ ∈Pd Δ且k∈ fc（P），则k∈ dom（Δ）.证据 一个简单的推导树上的每一个图。我们省略了变量和通道的标准重命名属性，但给出了名称的替换引理。注意，我们不需要通道或过程变量的替换引理，因为它们没有被传递。引理2.8（替换引理）如果Θ; Γ，x：S≠P dΔ且 Θ; Γ≠c：S，则Θ; rP [c/x]d Δ证据 标准我们写Δ Δ J，如果我们从Δ得到Δ J，通过替换k1：end，.，kn：end（n≥0）in Δ by k1：n，.，kn：如果Δ≠ ΔJ，我们可以通过应用[BOT]规则零次或多次从Δ获得ΔJ引理2.9（主同余）如果Θ; Γ<$P d Δ且P<$Q，则 Θ; Γ<$QdΔ。证据 用例P|不采取行动 我们证明了，如果Θ; P| inactdΔ，则Θ; r∈P d Δ。假设Θ; r =P d Δ 1和Θ; r=inactd Δ 2。其中Δ1< $Δ2 = Δ。 注意，Δ2仅包含end或end，因此我们可以设置：Δ J{k：end}和dΔ 2=Δ J·{k：end}，其中hΔ J Δ J=Δ J·Δ J和dΔ = ΔJ·Δ J·{k：end}。1 2 1 2 1 2 1 2根据[BOT]-规则，我们有：Θ;rPdΔJ·{k：θ}注意，给定Δabove的m，wenowthatdom（ΔJ）dom（ΔJ·{k：}）=2 1- 是的因此，通过应用弱化，我们有：Θ;rPdΔJ·ΔJ·{k：θ}1 2按要求对于另一个方向，我们在[INACT]中设置Δ=用例P|QQ|P，（P|Q）|RP|（Q|R）。 通过=的交换性和结合性。86N. 吉田，V.T.Vasconcelos/Electronic Notes in Theoretical Computer Science 171（2007）73我21我格（νu）P|Q（νu）（P|Q）如果u/∈ fu（Q）. 当u是一个名字时，这种情况是标准的。假设u是信道k，并且假设Θ; |Q）d Δ。我们有Θ; rP dΔJΘ; rQdΔJ1 2Θ; γP|Qd Δ J·k：其中ΔJ·k：Δ j= ΔJ< $ΔJ，ΔJ< $Δ由[BOT]。首先要注意k可以是1 2J或两者。有趣的情况是，当它发生在两个;从引理2.7（i）和k/∈fc（Q），我们知道ΔJ=Δ1·k：结束和ΔJ= Δ2·k：结束。然后，通过将[BOT]-规则应用于P中的k，我们有Θ; ΓP d Δ1·k：θ，并且通过应用[CRES]我们得到Θ; Γε（νk）P dΔ1。另一方面，通过加强，我们有Θ; Γ<$Qd Δ2。然后，应用[C ONC]得到Θ; Γ（νk）P|Qd Δ J。然后，通过应用[BOT]-规则，我们得到Θ;|Qd Δ，根据需要。另一个方向很容易。格（νu）不起作用不起作用。标准是弱化和强化。案件定义D在不起作用。类似于第一种情况，使用削弱和加强。如果u /∈ fu（D），则（νu）defDin（νu）P<$def D in（νu）P。类似于使用弱化和增强的范围打开情况。病例（P中定义为D）|在（P）中的Q定义D|Q）如果dpv（D）≠ fpv（Q）= 0。与使用弱化和增强的范围打开情况类似。定理2.10（主语归约）如果Θ; Γ≠P d Δ且P→P_Q，则 Θ; Γ ≠P_d Δ，QdΔ。证据我们假设关 于 我 们和e↓c意 味Γ∈cdS（3），并在最后一条规则上用归纳法证明了结果Case [L INK]（接受P1中的a（k））|（在P 2中请求a（k））→（νk）（P1|P2）。Sup- pose Θ; r（在P1中接受a（k））|（求P2中的a（k））d Δ。 然后，假设推导自：radα，αθ;rP1dΔJ·k：αradα，αθ;rP2dΔJ·k：α1J和2JΘ;r在P1d Δ1Θ中接受a（k）;r在P2dΔ2中请求a（k）[B OT]具有Δ J<$Δ i，[C ONC]具有Δ 1<$Δ 2= Δ J，[B OT]具有Δ J<$Δ。然后将[BOT]应用于P1和P2，我们有：Θ;rP1dΔJ·k：αΘ;rP2dΔJ·k：α1Θ;rP1d Δ1·k：α和2Θ;rP2d Δ2·k：α然后我们将[CONC]应用于P1和P2以获得：Θ;ΓP1d Δ1·k：αΘ; ΓP2d Δ2·k：αN. 吉田，V.T.Vasconcelos/Electronic Notes in Theoretical Computer Science 171（2007）7387Θ;Γ β1|P2d ΔJ·k：88N. 吉田，V.T.Vasconcelos/Electronic Notes in Theoretical Computer Science 171（2007）731212我21122我121现在应用[CRES]和[BOT]，我们就完成了。Case[COM]（k！[e];P1）|（k？（x）inP2）→P1|P2[c/x]，带e↓c。 该假设源自：Γ►e˜dS˜Θ;rP1dΔJ·k：α和Θ;Γ·xθ：SθθP2dΔJ·k：α你好！[e];P1dΔJ·k：！[S];αΘ; Γk？（x∈）在P2dΔJ·k中：？[S];α[BOT]具有hΔJ <$Δi，[CNC]具有hΔ1<$Δ2·k：<$=ΔJ，[BOT]具有hΔJ <$Δ。通过（3），我们知道了新的定义。通过将子项设置为Lemma，我们有：Θ;rP2[c/x]dΔJ·k：α在[Bot]和[CONC]对P1和P2[cn/xn]的应用中，[BOT]完成了这一情况。Case[LABEL]（kli; P1）|（kD{l1：P1 []···[] ln：Pn}） → P| Pi （1 ≤i≤ n）。类似于上面的案例。Case [P ASS]（throwk [kJ]; P1）|（catchk（kJ）inP2）→ P1| P2. 该假设源自：和Θ;rP1dΔJ·k：βΘ; r=throwk [kJ];P1d ΔJ·k：！[α];β·kJ：αΘ;ΓP2dΔJ·k：β·kJ：αΘ; Γ在P2dΔ J·k中捕捉k（k j）：？[α];β[BOT]具有Δ J<$Δ i，[CONC]具有Δ 1<$Δ 2·k：<$·kJ：α = Δ J，[BOT]具有ΔJ<$Δ。 注意，k，kJ/∈ dom（Δ 1，Δ 2，Δ J，Δ J）。通过将[BOT]、[CONC]应用于P1，1 2和P2，然后通过[BOT]，我们得到所需的结果。情况[I F 1]、[I F 2]。小事一桩。Case[DEF]defDin（X[ek]|Q）→defDin（P[c/x]|Q），其中e∈C，且dX （x∈k）=P∈D. 简 单 地说，如果将所述结果定义为所述情况，则设置D=（X （x_k_i）=P）。该系统由以下部分组成：Θ·X：S<$α<$; Γ<$X[e<$k<$]dΔJ·k<$：α<$Θ·X：S<$α<$; Γ<$Q dΔJΘ·X：Sα;Γ·x：SPdk：αΘ·X：S<$α<$; Γ<$X[e<$k<$]|Q dΔJJ·k：αΔJJΔJΘ;rdefX（xk）=Pin（X[ek]|Q）dΔJ·k：α其中hΔ0=ΔJ·k：α，ΔJ=ΔJΔJ和dΔ0Δ。NotethatΔJ只包含一个1 2 1端 然后将替换引理应用于P，我们有：Θ·X：S<$α<$; Γ<$P[c<$/x<$]dk<$：α<$注意ethatkdom（ΔJ）=，since（ΔJΔJ）·k：αs定义d。在我们的帮助下，1 1 2我们有：Θ·X：S<$α<$; Γ<$P[c<$/x<$]dΔJ·k<$：α<$N. 吉田，V.T.Vasconcelos/Electronic Notes in Theoretical Computer Science 171（2007）73891212到[CONC]，我们有Θ·X：S<$α<$; Γ<$P[c<$/x<$]|Q dΔJJ·k：α最后由[BOT]（ΔJJ<$ ΔJ），然后由[DEF]，我们得到：Θ;rdefX（xk）=Pin（P[c/x]|Q）dΔJ·k：α然后我们可以应用[BOT]来获得Δ，如所期望的。案例[S TR]。 主题一致。为了形式化类型安全，我们需要以下概念。一 个k-进程是一个由subjec t k（suchask！[e];Panddcatchk（kJ）inP）. 其次，一个k-re-dex是这两个工作过程的一个部分，即。e. ith erofform（k！[e];P|k？（x∈Q），（kl; P|kD{l1：Q1 []··[] ln：Qn} ） ， 或 （ throwk [kJ]; P|catchk （ kJJ ） inQ ） . 则 P 是 一 个 R RifP∈ （ vu∈ ）（defDin（Q|其中Q对于某些k来说是不形成k -redex的两个k -过程或三个或更多个k-过程的完全组合。然后我们有：定理2.11（类型安全）一个可类型化的程序永远不会减少到一个错误。证据通过主语归约，它表明可键入的程序不是错误。证明是通过反证法，假设错误过程是可类型化的。SupposethatΘ;radefDin（vu）（P|Q）dΔ。总之，我们得出结论，对于某个ΔJ，Θ;r∈P d ΔJ。现在我们分析两类误差过程。当P = P1时|P2是两个不形成redex的k -进程的并行合成，有几种情况需要考虑。他们都是一样的;举个例子标签选择/抛出对。 在P上应用[CONC]，我们有Θ; Γ<$P1d ΔJ和其中Δ j <$Δ J<$Δ J。 将[SEL]应用于P1，将[THR]应用于P2，得出结论，k：n {l1：α1，...，ln：αn} ∈Δ J和k：！[α];β∈ΔJ. 但之后ΔJ<$ΔJ1 2 1 2如果没有定义d，则在（νu）（P）中定义D |Q）这不是一个简单的问题。当P是三个或更多个k-过程的平行合成时，我们集中讨论三个过程的情况，因为其余的情况简化为这个。因此，设P=（P1）|P2）|P3. 应用[C ONC]，我们知道θ; Γ <$P1|P2d和Θ; r P3d J，Δ j J。如果P1|P2不是k-redex，我们使用上面的情况.否则，必须是k：k ∈k的情况。由引理2.7（ii）可知，k∈ dom（v_J），tu_s_d_J不定义，h_e_c_e_d在（v_u_j）（P）中定义|Q）这不是一个简单的问题。3更自由的会话传递风格原ESOP'98系统中的规则[PASS]（throwk [kJ]; P1）| （catchk（kJ）inP2） → P1|P290N. 吉田，V.T.Vasconcelos/Electronic Notes in Theoretical Computer Science 171（2007）73不允许任意信道的传输在大多数情况下，P2中的进程catchk（kJJ）可以在通信3之前进行alpha转换，以便绑定变量kJJ在语法上匹配抛出进程中的自由变量kJ当kJ在P2中是自由的时候，异常就发生了：alpha转换变得不可能（因为它会捕获自由变量kJ），并且通信不能发生。一个更自由的规则将允许传输一个任意的通道，在客户端实现一个替代。（throwk [kJ]; P1）|（在P 2中捕获k（kJJ））→P1|P2 [KJ/KJJ]不幸的是，这个规则破坏了主语归约（定理2.10）。一个计数器-一个例子是这样一种工艺，其拥有通道的一端，接收第二端。过程：掷出k [kJ]|在k jj中捕获k（kJJ）？（y）在kJ！[1]（4）在类型k：k，kJ：k下是可类型化的，但简化为处理kJ？（x）inkJ！[1]第一章这是不可能的，在同一类型下[7]。人们可能认为上述问题的最简单的解决方案是将边条件kJ/∈fc（P2）添加到上述规则提案中。然而，该归约规则意味着在运行时检查空闲通道的条件，与静态类型检查的目的相矛盾，以保持主题减少。同样的情况也发生在ESOP'98系统中，其中，在存在过程抛出k [ k j ]的情况下，|在P 2中捕获k（kJJ），运行时系统必须检查是否kJ∈fc（P2），以便在应用规则[PASS]之前对catch以上一个不同的替代方法是用不同的类型来输入合同。在上面的例子中，对于redex中的catch进程，我们有kJ：！[nat];end，andkJJ：？[nat];end.在合同中，通道kJ和kJJ是别名，如何从前提中构建正确的类型并不明显？[nat];！[nat];end forkJ.Gay和Hole [12]提出的解决方案明确区分了通道的两端。对于通道κ，它的两端表示为κ+和κ−。通道现在是由规则[LINK]创建的运行时实体（它们不应该出现在程序中），它变成：（接受P1中的a（x））|（在P 2中请求a（x））→（νκ）（P1[κ+/x]|P2[κ−/x]）同步给定通道上的两个进程的规则被更新，以便每个进程显式地提到其中一个端点。例如，规则[THR]变为：（throwκp [kJ]; P1）|（catchκp（x）inP2） → P1|P2 [kJ/x][3]参见段落关系与2.1节中π-演算的重写规则。N. 吉田，V.T.Vasconcelos/Electronic Notes in Theoretical Computer Science 171（2007）7391其中p表示κ的一端（一个极性），p表示另一端。进一步的改变允许类型Δ包含κ+的一个类型和κ−的不同