理论计算机科学电子笔记138（2005）3-22www.elsevier.com/locate/entcs类型检查安全进程同步Eduardo Bonelli爱德华多·博内利1，3史蒂文斯理工学院和LIFIA6Adriana Compagnoni阿德里安娜·Compagnoni1，4史蒂文斯理工Elsa Gunter艾尔莎·冈特1，2，5伊利诺伊大学香槟分校摘要会话类型描述了多方通信中两方之间的交互。它们构成了一个通信协议，在这个意义上，双方之间的交互顺序和类型是特定的。对于它们来说，对应断言提供了一种同步机制。当会话类型和通信断言相结合时，它们能够描述跨不同通信会话的同步，从而产生用于在多方通信中施加表达性交互模式的丰富本文研究了Iris的类型检查问题，Iris是一种结合了会话类型和对应断言的类型化π演算.我们定义了一个类型检查算法，并证明了它是健全的和完整的类型规则。 此外，我们表明，打字系统满足最小值影响属性。 尽管过去已经对会话类型进行了广泛的研究，几年来，据我们所知，这是第一次证明类型检查的可判定性的类型系统与会话类型。关键词：并发，π演算，类型系统，类型检查。1部分由NSF资助。CCR-0220286 ITR：安全电子交易。2部分由ARO根据第2004/2005号裁决予以支持DAAD-19-01-1-04733电子邮件：ebonelli@cs.stevens-tech.edu4电子邮件：abc@cs.stevens-tech.edu5电子邮件：egunter@cs.uiuc.edu6阿根廷拉普拉塔拉普拉塔大学信息学院1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.05.0024E. Bonelli等人/理论计算机科学电子笔记138（2005）31引言在我们的社会中，我们越来越依赖于处理器来监视和控制我们生活中几乎所有方面的设备。在许多情况下，这些处理器的行为由与其他处理器的通信来管理，其他处理器可以是同一系统的其他组件或者可以位于远程。在空间探索、空中交通管制、医疗设备、银行和电子商务中可以找到非常重要的是，要高度保证管理这些通信和由此产生的决策的软件是正确的。本工作中提出的方法适用于多方之间的通信可以分解为一对一通信的任何情况会话类型[17，18]允许描述双方之间的信息交换。它们描述了正在交换的信息、交换的顺序、发送方、接收方以及信息的类型然而，单独的会话类型在限制进程交互方面是不够例如，在[1，4]中开发了一个涉及过程Client、ATM和Bank的小型系统它说明了会话类型无法捕获的情况，包括：• 当客户从ATM请求存款操作时，ATM可以在不违反基于会话类型的协议描述的情况下将一些资金重定向到不同的帐户• 自动柜员机可能会转发一个与它从客户那里读取的金额不一致的金额。• 自动柜员机可能会收到客户的存款，而不会与银行联系。将会话类型与对应断言[23，12，14]相结合，可以大大增加可能强加在流程上的交互模式的表达能力。 现在可以解决的属性的示例是[1，4]：• 客户收到的余额始终来自银行，银行收到的待存金额始终来自客户。• 自动柜员机应作为一个转发器，不改变从银行或客户收到的数据。• 我们可以检测到ATM正在尝试存款，而不是客户的指示，或试图存入比客户指定的金额更小的金额。Iris是一种基于π演算的静态类型语言，它扩展了[18]与对应断言[11，14]，最早在[1]中引入。在那里，它表明，类型系统允许我们检测并发中的不规则性E. Bonelli等人/理论计算机科学电子笔记138（2005）35−⟨⟩通信，例如未经授权的数据修改、丢失或避免的通信以及额外的非预期通信。在本文中，我们继续研究虹膜的类型检查是可判定的。相关工作。 关于会话类型，它们在过去十年中吸引了相当多的关注，这是由于这种类型系统为协议分析提供的好处。关于会话类型的最初提议是由K.Honda等人[17]。已经研究的这项工作的自然扩展包括亚型[8]和有界多态性[16]。它们也在基于组件的软件开发的背景下进行了研究[22]，并在具有输入/输出操作的λ演算中重新表述[9]。关于类型检查和推理，[7]给出了多进π演算的排序推理算法B. Pierce和D. Turner为PICT定义了一个类型检查和类型推理算法，PICT是一种基于π演算多态版本的并发编程语言The CrypticProject是A.Gordon和A.Je Escherey，包括他们在[12，11，14，13]中开发的语言的类型检查器的实现，其中包括对应断言以及公共和私有数据。将过程视为模型的范式由Chaki等人提出在[6]中，也有一个类型检查器（称为Piper）的实现。本文讨论了[19，20]中泛型类型系统公共部分的类型检查最近，N. Kobayashi，允许无锁分析，无死锁分析，无用代码消除和信息流分析[21]。2虹膜-微积分2.1语法我们假设给定一组名称x，y，z，. 我们区分两种不同类型的名称：表达式名称，写作a，b，c。. . （其范围在会话和整数上）;以及信道名称，书写为k、h、KJ、. 我们也有整型常量...，一，零，一，... 和（分支）标记l，LJ，. 值是表达式名称或整数常数，并且用字母v、vJ、. 断言标签，写为L，LJ，.. . ，是值的元组，并且被写为v1，...，v;过程表达式，用P、Q、. . . 定义如下：7[7]在我们的技术文献[3]中，我们讨论了P中的一个过程分解定义D，其中D 表示X1[a1：T1]=P1， . 且Xn[an：Tn]=Pn，且a个过程都构造X[→v]. 由于篇幅限制，这些内容被省略了。6E. Bonelli等人/理论计算机科学电子笔记138（2005）3[详细 ][详细]⊥⊥⊥⊥P：：=在P中请求a（k）|在P中接受a（k）|k？（x）在P中|国王！[v];P|throwk[kJ];P|在P中捕获k（kJ）|（νa：T）P|（ νk ： <${α ， α} ） P|k<$l;P|k{l1 ： P1Q. Qln ： Pn}| 停 止|P|Q|begin L;P|结束L; P注释2.1括号是结合结构。两个过程表达式只在它们的界限名的名称上不同，称为α-等价的，应认为是相等的。我们用记法P a v表示把P中所有自由出现的a都替换为v的结果，对于P k也是如此kJ。一个进程表达式的自由名的集合，写为fn（P），断言标签，同样写为fn（e），以标准方式定义（参见[2]详情。request原语请求名称a上的会话。当建立该会话时，新的专用信道k将用于消息交换。accept接收同名a的请求，并生成一个新的专用通道，用于建立会话后使用的消息交换。request和accept构造各自绑定后续进程P中紧随其后的通道变量k的所有自由出现。消息的同步发送和接收是通过k！[v];Q和k？（x）在P中，虽然，如[18]中，翻译为具有分支的异步演算是可能的。通过Q中的通道委托结构throwk[kJ];P和catchk（kJ），实现了对通道使用的线性约束的受控侧步。选择一个国家的机制标签和分支可作为kl; P和kD{l1：P1Q... Qln：Pn}。符号P |Q代表P和Q的并发执行;我们也使用stop表示不作为。我们将（νa：T）P或（νk：{α，α}）P用于名称隐藏的常用构造，其中前者用于表达式名称，后者用于通道名称。T表示类型表达式（Def. {α，α}是具有由信道类型α给出的通信协议的“完全”信道类型。 注意{α，α}={α，α}。 开始和结束断言应该在Iris的类型系统中用作类型指令（Sect.2.2.1）：beginL;P只是断言beginL，然后表现为P;同样endL;P断言endL，然后表现为P。Iris的操作语义以一个重新定义的形式出现图1中给出了过程的推导关系。像往常一样，它依赖于结构一致性的概念，其定义在虹膜中是标准的。2.2类型纪律2.2.1会话类型和效果类型系统在一组给定的类型假设下为进程分配一个结果。流程的结果反映了其未决义务。一个E. Bonelli等人/理论计算机科学电子笔记138（2005）37↑↑↑↑↓↓⊥（接受P1中的a（k））|（在P 2中请求a（k））−→（νk：<${α，α}）（P1|P2）跨链路（k！[v]; P1）|（k？（a）在P2中）−→ P1|P2{a <$v}跨通信（k<$li; P）|（k）{11：P1Q. Q ln：Pn}）−→ P |Pi，如果i ∈ 1。n TransBrnch（throwk[kJ];P1）|（catchk（kJJ）inP2）−→P1|P2{kJJ<$kJ} TransCatchbeginL;P −→ PTrans BeginendL;P−→PTrans EndP−→PJ（νx：U）P −→（νx：U）PJTrans ResP−→PJP|Q−→P J|Q跨杆P<$PJ，PJ−→QJ，QJ<$Q<$P−→QTrans<$Fig. 1. 虹膜的无标号约简语义形式为beginL的断言通过从当前对象中删除断言标签L来减少这些义务;同样地，endL用L来增加当前对象。因此，有效性决定了必须出现的开始断言数量的下限。如果进程有一个空的断言，那么所有的结束断言都对应于一个匹配的开始断言。如上所述，为了使两个或多个进程共享关于它们的待决或潜在效应的信息，因此，添加到通道的效应被称为潜在效应。定义2.2[带谓词的类型]断言标签、谓词和类型由以下语法给出：普通类型T：：=Int| σ(α)通道类型α、β：：=↓[a：T]e;α| ↑[a：T]e;α| ↓[α]e; β| ↑ [α]e; β |&{11：α 1，...，ln：αn}e| {11：α1，...，ln：αn}e|1 | ⊥{α,α}E =E，E =J，E =（|L1，...，Ln|）断言标签L，Li：：= 1，.， vn类型可以是普通类型或通道类型;我们使用U，Ui来覆盖类型。一个类型U的自由名的集合，写作fn（U），像通常一样定义（见[2]）。基类型Int是整型常量的类型会话类型被表示为σ（α），并且可以非正式地被视为表示由通道类型α及其对偶α组成的对：↓[a：T]e;α↓[α]e;β&{li：αi}edef=[a：T]e;α[a：T]e;αdef=[α]e;β[α]e;βdef={li：αi}e{li：αi}edef=[a：T]e;α1def=[α]e;βdef={li：αi}edef=1个应将类型α和α分配给通信会话的两个端点。 注意，{α，α}没有定义。 通道类型由一系列输入/输出类型的值或通道或分支/选择类型;假定序列以通道类型终止符终止1. 每一个都伴随着一个潜在的效应。一个断言是一组多个断言标签;我们使用（|......这是什么？|）的多集构造函数。多集减法8E. Bonelli等人/理论计算机科学电子笔记138（2005）3≤ ≤⊥∪--∈∈定义为e\eJ，最小的多集eJJ使得e≤eJ+eJJ，其中多集连接被定义为e∈eJ，最小的多集eJJ使得e eJJ和eJeJJ。 特殊通道类型{α，α}对尚未打开并在两个子进程之间共享目前的进程。2.2.2类型规则环境Γ是一组类型假设x1：U1·. ·Xn：U n，其中X1，.，x n是不同的名字。我们用字母Γ，Δ，. for environments环境. r的定义域，写作dom（r），是集合{x1，.， x n}，并且r的范围，写作ran（r），是集合U1，.，联合国。 此外，我们为Γ分配通道类型的名称子集写domCh（Γ），为Γ分配普通类型的名称子集写domPl（Γ）Γ的自由名，写作fn（Γ），是出现在Γ的定义域中的名的集合，或者是在Γ的范围内的类型中的自由名的集合即fn（Γ）=dom（Γ）U∈ran（Γ）fn（U）.在假设x：U中，x被称为主语;如果分配给主语的类型是普通类型，则假设被认为是简单的假设，否则它是信道假设。我们写Γ·x：U为从扩展Γ得到的环境，类型为假设x：U，对于x∈/dom（Γ）。符号U：U代表从Γ中删除假设x：U而产生的环境，假设它存在。由于存在唯一的U使得对于任意x∈dom（Γ）x：U∈Γ，我们有时可以用Γ\x来表示Γ \x：U。对于任何x∈dom（Γ），我们将使用Γ（x）作为唯一类型，使得（x：Γ（x））∈Γ。定义2.3[取决于]xi：Ui直接取决于在Γ中的xj：Uj（写作（xj：Uj）<$→d（xi：Ui）），如果xj∈fn（Ui）。 如果xi：Ui<$→xj：Uj，则称xi：Ui依赖于xj：Uj，其中<$→表示<$→d的传递闭包。一个环境是良构的，如果它满足以下三个条件：C1. 对于每个xdomPl（r），x是表达式名称，并且对于每个ydomCh（r），y是信道名称。C2. 对于每个i ∈ 1.. n，fn（U i）是随机的（Γ）\{xi}.C3. 关系<$→是不可逆的，即对于所有的xi：U i ∈ Γ，xi：U i<$/→ xi：Ui。第一个条件C1要求只有通道类型被分配给通道名，只有普通类型被分配给表达式名。条件C2要求由Γ赋值的类型中的所有自由名必须在Γ内声明注意，由于通道名称可能不会出现在断言标签中，因此不会出现在fn（Ui）中，因此类型可能只依赖于被分配了普通类型的名称由于通过通道名称的交互受到线性逻辑[10]意义上的线性条件的限制（参见Type Par规则E. Bonelli等人/理论计算机科学电子笔记138（2005）39[详细]下面），这个限制说明我们不允许依赖于线性假设的类型;但是我们允许依赖于共享假设的类型我们的类型学科的预期应用不会受到这样一个限制的干扰，并且不清楚解除它所导致的元理论的技术复杂性是否超过了它的好处。事实上，这种限制已经出现在线性和直觉假设共存的其他环境中，例如[5]的线性逻辑框架最后一个条件C3要求Γ没有循环依赖。这通常通过将环境表示为类型假设的序列来保证，其中假设x：U仅依赖于出现在其左侧的那些这样的表示似乎不适合存在通道类型的设置，因为关于结构规则可接受性的基本结果失败了[3]。Iris型系统由下列判断组成：Γ良型环境 ΓT类型的良好类型值v具有e的良型过程PIris的类型规则如图2所示。规则Type Acpt和Type Requ在环境中引入了一个新的通道名，从而保证了会话使用的是私有通道。请注意，双通道类型用于请求方和接受方。类型Bgn和类型Enda assertion通过消除或添加新的断言标签来处理效果。规则Type Snd和Type Rcv允许为发送和接收数据键入通信原语。请注意，数据仅通过通道另外，注意，在Snd型的右上判断中，k的类型是α av，这反映了信道类型的“其余部分”，即α，可以取决于输出值v的事实。在类型Snd规则中，与k的输出类型相关联的潜在效应成为信用。换句话说，它变成了一个类似的评论适用于类型Rcv规则。然而，请注意，这次输入的参数类型（即“b“）的潜在结果类型Brnch和类型Sel分别输入分支和选择原语;如果待定的结果被视为信用，那么很明显，类型Brnch中每个分支的结果必须被连接。通道委托是通过throw和catch原语来实现的，这些原语通过类型Thr和类型Cat来类型化。规则类型Thr受限制-这限制了渠道的授权，10E. Bonelli等人/理论计算机科学电子笔记138（2005）3⊥通信是可能的，即，没有通道和名称限制（对于非通道名称）按预期方式键入Type Stop键入无动作停止;它要求通过通道名称的所有通信都已完成。Type Subs规则允许增加过程术语所需的Type Par规则对两个进程的并行执行进行一个通道可以由两个进程P或Q中的一个进程使用。这个规则的唯一例外是当P和Q都使用双类型的通道k由于必须限制信道使用以保证这种线性使用，因此要求环境Γ和ΓJ兼容（图4）。请注意，兼容性的概念对于两组不一定形成良好的环境。一旦这个兼容性的概念到位，我们可以定义如何通过环境组合来组合两个环境（图1）。 4）. 的第二个子句中{α，α}的下标环境组成的定义（图4）记录了双通道类型，以及这些双通道类型的名称依赖关系。3类型检查我们定义了一个类型检查函数Ch（Γ，P），其中Γ是一个环境，P是一个过程.函数Ch（Γ，P）通过在P的长度上递归来定义，并且将返回失败或P的最小可能结果。我们使用两个辅助函数：• ChEnv（Γ），它检查上下文的良构，当且仅当Γ不成立时返回真• ChTy（Γ，v，T）检查返回true的值的类型，当且仅当Γ=v：T。ChEnv（r）检查环境r是否是良构的。这需要检查条件C1、C2和C3。为了检查C3，我们构造了一个有向图，它的边从环境定义域中的名字指向环境关联类型中的每个自由名字。（在这个过程中，我们可以很容易地检查条件C1和C2。一旦我们构建了图，我们应用任何标准算法来检查它是否是无圈的。如果v是一个数值常量，ChTy（Γ，v，T）检查T是否=Int;否则它检查v：T是否在环境Γ中，然后调用ChEnv（Γ）。[8]从技术上讲，这使我们能够纠正[18]中存在的一个问题，即主语同余的失败。E. Bonelli等人/理论计算机科学电子笔记138（2005）311Γ·a：σ（α）·k′：α<$P{k←k′}：ek′/∈dom（Γ）Γ·a：σ（α）<$在P：e中接受a（k）Γ·a：σ（α）·k′：α<$P{k←k′}：ek′/∈dom（Γ）类型Acpt类型要求P：efn（L）随机数（Γ）2019-05-2201：01：02（|L|）Bgn型P：efn（L）随机数（Γ）2016 - 05- 25 01：01：02 01：03 01：03|L|）式端Γv：Tfn（e′）\{a}随机域（Γ）Γ·k：α{a←v}<$P：eΓ·k：↑ [a：T]e′;αk！[v];P：e+e′{a←v}Γ·c：T·k：α{a<$c}<$P{b<$c}：e类型Sndfn（e′）\ {a}随机（Γ） c/∈fn（e\e′{a←c}）<$fn（Γ）型RcvΓ·k：↓[a：T]e′; α k？（b）在P中：e\e′{a ← c}r·k：α1 P1：e1. Γ·k：α n<$Pn：enfn（e′）随机域（Γ）r·k：&{11：α1，.，l n：α n}e′ kD{l1：P1，.，l n：P n}：（ei）\e′nΓ·k：α j<$P：e（1≤j≤n）fn（e′）<$fn（α）随机（Γ）类型Brnchi=1类型选择r·k：n {l1：α1，.，l n：α n}e′kl j;P：e+e′Γ·k：α<$P：efn（β）<$fn（e′）随机性（Γ）β=/Γ·k′：β·k：↑[β]e′;α掷k[k′];P：e+e′1类型Thrr·k′′：β·k：α<$P{k′←k′′}：efn（e′）∈dom（r）k′′/∈dom（r）r·k：↓[β]e′;α<$catchk（k′）inP：e\e′Γ·k′：<${α，α}<$P{k←k′}：e k′/∈dom（Γ）型CatΓε（νk：ε{α，α}）P：eΓ·b：T<$P{a←b}：eb/∈fn（Γ）<$fn（e）Γ<$（νa：T）P：eCRes型NRes型Γ► ⬦ ranCh（Γ）<${1，<${α，α}}stop：（||）式截止P：ee≤ e′ fn（e′）随机（Γ）ΓP：e′类型子12E. Bonelli等人/理论计算机科学电子笔记138（2005）3P：eΓ′Q：e′Γ=Γ′Γ Γ′ P |Q：e + e′式停车图二. 良好类型的进程表达式E. Bonelli等人/理论计算机科学电子笔记138（2005）313∈∈\∈∩I·a：TΓ·a：Ta：TWf Val ENAMEΓ► ⬦ n∈Z简体中文Wf Val Int(i)=(ii) Γ= Γ′蕴含′图三. 类型良好的值(i)∅◦∅=∅(ii)（Γ·a：T）（Γ′·a：T）=（Γ Γ′）·a：T(a) Γ·a：T=Γ·a：T（iii）（Γ·k：α）<$（Γ′·k：α）=（Γ<$Γ′）·k：<${α，α}(b) Γ·k：α=Γ′·k：α′ ′ ′(c) Γ·k：α=Γ′，ifk∈/dom（Γ′）(d) r=r′·k：α，ifk∈/dom（r）（iv）（r·k：α）n（r）=（r∈r）·k：α，ifk∈/dom（r）（v）r∈（r′·k：α）=（r∈r′）·k：α，ifk∈/dom（r）图四、兼容环境和环境的组成在定义Ch的分句以进行平行合成时，有几个特殊用途的定义是3.1扩展环境通过允许通道名与形式为σ（α）的普通类型（会话类型）相关联来给定扩展环境Γ，令：domChoice（Γ）={k ∈ domCh（Γ）|对于某些信道类型α }，Γ（k）=σ（α）。如果dom（ΓJ）=dom（Γ），则我们称正则环境ΓJ为扩展环境Γ的特殊化，并且对于所有xdom（Γ）domChoice（Γ），我们 有ΓJ（x）= Γ（x），对于所有k个domChoice（Γ），如果Γ（k）=σ（α），则要么ΓJ（k）=α，要么ΓJ（k）=α。让：（Γ i）={Γ Ji|i是i的特殊化。定义3.2设P和Q是过程，Γ是环境。我们定义Γ关于P和Q的分裂为：• 如果fn（P）≠fn（Q）/dom（Γ），则split（Γ，P，Q）=fail。• 若存在kfn（P）fn（Q）使得split（r，P，Q）=fail.对于任意α，则• 否则，split（r，P，Q）=（r1， r2），其中r1和r2是由以下定义的扩展环境：· dom（r1）dom（r）和dom（r2）dom（r）。· 对所有的a∈domPl（Γ），a∈dom（Γ1），a∈ dom（Γ2），且Γ1（a）= Γ2（a）= Γ（a）.·对于k∈fn（P）<$fn（Q）且Γ（k）=<${α，α}，有Γ 1（k）= Γ 2（k）= σ（α）.· 对除k/∈fn（Q）以外的所有k∈fn（P），k/∈dom（Γ2）且Γ1（k）= Γ（k）.· 对除k/∈fn（P）以外的所有k∈fn（Q），k/∈dom（Γ1）且Γ2（k）= Γ（k）.· 对于所有k∈dom（Γ）\（fn（P）<$fn（Q）），我们将（任意）指派Γ1（k）= Γ（k），并且有k/∈dom（Γ2）。14E. Bonelli等人/理论计算机科学电子笔记138（2005）3⊥⊆联系我们这些定义用于定义Ch（r，P）的子句中。|Q）。函数分裂用于将环境Γ划分为两个扩展环境，Γ1和Γ2，使得对于适当的ΓJ1∈ Σ（Γ1）和ΓJ2∈ Σ（Γ2），Γ = ΓJ1< $ΓJ2。困难在于当Γ（k）={α，α}，我们可能需要将k：α发送给一个而k：α是另一边，但我们不知道哪一边会得到哪些.集合（Γ1）和（Γ2），其中（Γ1， Γ2）=split（Γ，P，Q），允许我们枚举ΓJ1和ΓJ2的可能性的充分集合。在分裂的定义中有几个任意的选择。首先，对于任意或所有k∈dom（Γ）\（fn（P）<$fn（Q）），我们可以发送k：Γ（k）到Γ2。其次，如果Γ（k）=π{1，1}，那么我们有一个额外的选择，将k：1分配给Γ1和Γ2中的每一个。在定义Γ时使用这些任意选择的正当性在于它们不改变类型检查函数Ch（见[3]这一事实的证明3.1定义类型检查函数Ch我们通过对P的长度的归纳来定义Ch（Γ，P）。为了确保良好的定义，我们假设所有类别的名称是完全有序的，并且在选择新名称时，我们选择最不新鲜的名称。如果fn（P）dom（Γ），则Ch（Γ，P）被定义为返回失败。在所有后续情况下，我们将假设fn（P）dom（Γ）。在大多数情况下，Ch的定义可以从类型规则中读取。例如，如果P是Q中的requesta（k），则我们让kJ是不存在的新信道变量 在dom（r）中，定义Ch（r，在P中请求a（k））为：• Ch（Γ·KJ：α，P{k<$KJ}），若Γ（α）=σ（α），且• 失败，否则。平行组成的情况是一个例外，需要进一步注意。 如果split（Γ，P，Q）返回失败，则Ch（Γ，P |Q）也被定义为返回失败。否则，如果split（r，P，Q）/=失败，则令（r1， r2）=split（r，P，Q）。注意，对于上面定义的扩展环境Γ1和Γ2，domChoice（Γ1）=domChoice（Γ2还请注意，作为给定扩展环境的特殊化的正则环境的数量是2|domChoice（Γi）|≤2|domCh（Γi）|. We定义Ch（Γ， P |Q）as：• Ch（Γj1， P）+Ch（Γj2，Q），如果存在Γj1∈ψ（Γ1）和Γj2∈ψ（Γ2），使得Ch（ΓJ1， P）失效和Ch（Γ2J，Q）失效，且对所有k∈dom Choice（Γ1） =domChoice（r2），rJ1（k）= rJ2（k），以及• 失败，否则。注意至多有一个特殊化Γj1∈ P（Γ1）和至多有一个特殊化Γj2∈P（Γ2）使得Ch（Γj1， P）/=fail和Ch（Γj2，Q）/=fail.E. Bonelli等人/理论计算机科学电子笔记138（2005）315/►≤►►►3.2Ch的性质在Ch的定义中有几个要点，其中有两种选择之一：第一种是新鲜名称的选择，第二种出现在平行合成Q的情况下|R，其中我们将环境Γ“拆分”为两个扩展环境Γ 1和Γ 2，然后选择专门化Γj1和ΓJ2是独立的，使得Cn（Γj1，Q）=fail，Cn（Γj2，R）然而，以下结果仍然成立。命题3.3（Ch的良定性）Ch是一个全函数。失败证据这依赖于两个主要引理。第一个声明新鲜名称的选择不会影响Ch的输出。第二个假设是，如果上述的特化ΓJ1和ΓJ2存在，那么它们是唯一的。最后，注意，第三个参数（过程P）的大小在每个过程中减小，递归调用Q为了证明完备性，我们可以假设ΓP：e的类型推导不包括类型子的应用。这是从观察得出的，如果ΓP：e，那么对于某个eJe，ΓP：eJ是可导出的，而不使用类型子。命题3.4（完备性）如果Γ <$P：e，则Ch（Γ，P）Ch（Γ，P）≤e。失败并证据通过对ΓP的推导的归纳，得到了：e.所有的情况下遵循标准引理，除了平行复合的情况。这种情况需要下面的结果，其证明是简单但繁琐的。引理3.5设Γ 1和Γ 2是使得Γ 1= Γ 2的环境，并且设Γ=Γ1<$Γ2。假设Cn（r1， P）/=失效，Cn（r2，q）=/failandsplit（Γ，P，Q）/=对于某些过程P和Q失败。 设（r，P， Q）= split（r，P，Q）. 则存在re，使得rJ1=rJ2，r=rj 1 <$r j 2，且Ch（rJ1， P）=Ch（r1， P）， ch（rJ2，Q）=Ch（r2，Q）.并行组合的证明过程如下：假设Par类型是最后一个应用的规则。则P =Q|存在环境Γ 1和Γ 2以及相应的e1和e2使得Γ 1<$Q：e1和Γ 2<$R：e2和Γ 1= Γ 2和Γ = Γ 1<$Γ 2和e= e1+ e2。通过归纳假设，我们得到：Ch（Γ1，Q）/=fail，Ch（Γ1，Q）≤e1，Ch（Γ2，R）/=fail，并且Ch（Γ2，R）≤e2.由于Ch（Γ1，Q）f=fail且Ch（Γ2，R）fail，我们有fn（Q）dom（Γ1）和fn（R）n（Γ2）.此外，由于Γ = Γ1< $Γ2，我们有fn（Q）<$fn（R）n（r），且对每个k∈fn（Q）<$fn（R），存在α使得16E. Bonelli等人/理论计算机科学电子笔记138（2005）3·{← }·{←{\fnMicrosoftYaHei\fs20\2cHFFFFFF\b0}·{←}/∈Γ（k）=<${α，α}.因此，定义了split（Γ，Q，R），我们可以取（1，2）=split（Γ，Q，R）。根据引理3.5，存在Γ j1∈C1（R1）和Γ j2∈C1（R2）使得Γj1=Γj2和Ch（Γj1，Q）=Ch（Γ1，Q）和dCh（Γj2，R）=Ch（Γ2，R）. 由于Γj1=Γj2，对所有k∈domChoice（Γ1），我们有Γj1（k）=Γ2J（k）. 因此，我们建议，根据Ch的定义，我们有Ch（r，Q|R）失败，Ch（r，Q|R）=Ch（rJ1，Q） +Ch（rJ2，R）=Ch（r1，Q） +Ch（r2，R）≤e1+e2=eQ命题3.6（合理性）如果Ch（Γ，P）/= fail，则Γ ≠P：Ch（Γ，P）。证据通过对Ch（Γ，P）定义的归纳。我们展示了两个案例。• 在P中接受a（k）：通过Ch的定义，Ch（r，在P中接受a（k））= Ch（r kJ：α，PKKJ），其中 kjdom（Γ）和Γ（α）=σ（α）.通过归纳假设，得到了：ΓKJ：αPKKJ：Ch（ΓKJ：α，PkkJ）。通过Ch的定义，并应用Acpt型，Γa：σ（α）在P中接受a（k）：Ch（Γ，在P中接受a（k））。• P|Q：通过定义Ch，Ch（r， P |Q）=Ch（Γj1， P）+Ch（Γj2，Q），其中有Γ j1和Γ j2.通过构造Γ j1和Γ j2，得出了Γ j1= Γ j2和Γ=Γj1<$Γj2，并通过归纳推理得出了Γj1<$P：Ch（Γj1， P）和Γj2<$Q：Ch（Γj2，Q）. 最后，根据TypePar规则，得到如下结果。Q推论3.7（最小效应集）如果ΓP：e，则ΓP：Ch（Γ，P）且Ch（r，P）≤e.证据 这个结果直接适用于健全性（命题3.6）和完备性（命题3.4）。Q我们现在可以陈述我们的主要结果。推论3.8（类型检查的可判定性）给定Γ，Θ，P和e，可判定是否Γ ∈P：e。证据我们首先通过命题3.3调用总是终止的Ch（Γ，P）。如果Ch（Γ，P）=fail，通过完备性（命题3.4），ΓP：e不可导。如果Ch（Γ，P）/=失败，我们检验多重集包含Ch（Γ，P）≤e，它也是若Ch（Γ，P）≤e成立，则根据可靠性（命题3.6）和类型子，Γ∈P：e. 若Ch（Γ，P）/≤e，根据完备性（命题3.4），Γ∈P：e不可导。QE. Bonelli等人/理论计算机科学电子笔记138（2005）3174结论和今后的工作会话类型描述多方通信中两方之间的交互.它是一种通信协议，描述了双方之间交互的顺序和类型。Iris是一个类型化的π演算，它是由会话类型与对应断言的组合Iris允许描述交换协议，以及可能不参与同一会话的各方之间的同步本文研究了Iris的类型检查问题。我们定义了一个类型检查算法Ch（Γ，P），它检查进程P在Γ中的类型假设下是否可类型化如果P在Γ下是可类型的，则返回P的最小结果，否则返回fail。虽然在过去的几年里，会话类型已经被广泛研究，但据我们所知，这是第一次证明具有会话类型的类型系统的类型检查的可判定性。我们目前正在研究的一个相关的开放问题是类型推断的可判定性，其中必须在存在诸如定义通道类型的对偶的方程的情况下考虑类型统一Iris允许我们表达在其源发送的信息和在预期目的地接收的信息之间的关系如果我们停留在一个可判定的片段中，比如线性算术，我们就可以捕获大量的通信和数据交换模式：在很大一部分数据传输的情况下，我们感兴趣的是在两端看到完全相同的数据，而许多其他情况涉及非常简单的线性算术变换。例如，ATM机经常被允许对交易收取手续费，那么客户输入的金额与银行收到的金额之间的关系将不相同，但将满足一个简单的线性算术方程。为了解决这个问题，我们正在考虑用算术扩展Iris如果我们允许不可判定的一般算术，我们可以期望定义一个合理的半判定过程：一个没有误报或漏报的算法如果算法说是，那么所有信息都可以追溯到其来源。如果算法说不是，算法将显示一条路径，表明数据不是来自预期的源。如果算法无法终止，那么我们就无法推断出任何信息。未来的工作还包括在HOL [15]中开发这种演算的形式理论，并使用开发来编码和推理安全和网络协议。18E. Bonelli等人/理论计算机科学电子笔记138（2005）3确认我们感谢史蒂文斯的LSS小组进行了有趣的讨论。我们也感谢GeorgiBabayan、Pablo Garralda、Healfdene Goguen和Ricardo Medel的意见和建议。引用[1] Bonelli，E.，A. Compagnoni和E. Gunter，并发通信中进程同步的对应断言，在：A。Brogi，J.- M. Jacquet和E. Pimentel，editors，FOCLASA 2003.第二届协调语言和软件体系结构基础国际研讨会，理论计算机科学电子笔记97（2003），pp。175比195[2] Bonelli，E.，A. Compagnoni和E.陈文辉，同步通信中的同步问题，北京大学计算机科学研究所硕士论文，2003。[3] Bonelli，E.，A. Compagnoni和E.林志荣，同步化系统的安全性分析，硕士论文，国立台湾科技大学计算机科学系，2004。[4] Bonelli ， E. ， A. Compagnoni 和 E. Gunter ， Correspondence Assertions for ProcessSynchronization in Concurrent Communications ， Journal of Functional Programming ，Special issue on Practice Based Security15（2005）.[5] 切尔韦萨托岛和F. Pfenning，线性逻辑框架，信息与计算179（2002），pp. 十九比七十五[6] Chaki ， S. ， S. Rajamani 和 J. J. J. J. ， Types as models ： Model checking message-passingprograms，2002年，第29届ACM SIGPLAN-SIGACT Symposium on Principles of ProgrammingLanguages45比57[7] 盖伊，S.，一个多进π演算的排序推理算法，在：Proc. of the 20th ACM SIGACT/SIGPLANSymposium on Principles of Programming Languages（1993），pp. 429- 438[8] 盖伊，S。和M. Hole，Types and Subtypes for client-server interactions，in：Proceedingsof the European Symposium on Programming Languages and Systems，number 1576 inLNCS（1999），pp.74比90[9] 盖伊，S.，V.Vasconcelos和A. Ravara，Session types for inter-process communication，Technical Report TR-2003-133 ，Department of Computing Science ，University of Glasgow（2003）。[10] Girard，J.-是的，Linear Logic，Theoretical Computer Science（1987），pp.1-102[11] 戈 登 A. 和 A. Je Escherey ， Authenticity by typing for security protocols ， 14th IEEEComputer Security Foundations Workshop（2001），pp. 145-159[12] 戈登A.和A.Je Escherey，Typing correspondence assertions for communication protocols，in ： Seventeenth Conference on the Mathematical Foundations of Programming Semantics（MFPS 2001），number 45 in ENTCS（2001）.[13] 戈登A.和A. Je Escherey，Authenticity by typing for security protocols，Jou
我的内容管理
展开
