理论计算机中间语言F！的设计及其在编译安全中间语言开发中的应用

《理论计算机科学电子札记》58卷第1期（2001年）网址：http://www.elsevier.nl/locate/entcs/volume58.html18页代表F！在LFCarstenSchu大春玉2号;赵中倪3号耶鲁大学美国纽黑文摘要我们研究如何类型理论F！可以在Meta逻辑框架中充分表示[16]。这种开发特别强调术语、类型和种类的表示方式，因为它使用高阶抽象语法来建模变量绑定，使用依赖类型来建模类型约束。此外，我们的设计确保了只有良好类型的术语和良好类型的类型可以被构造。这项工作的一个可能的应用在于开发用于编译的安全中间语言。1引言现代编译器采用复杂的编译技术来保证生成的二进制文件的安全条件。一类重要的安全条件是由类型系统捕获的，编译器试图通过类型系统在整个编译过程中跨整个级联的中间语言维护类型信息。级联从源语言开始，通常以机器语言结束。已经提出了各种技术来表示安全条件，例如PCC [12]和TAL [11]。中间语言通常以这样一种方式设计，即各个语言之间的概念差异很小且易于管理，每个特定语言的属性是可证明的，并且不同中间语言之间的关系是可分析的。本文讨论了一种特殊的中间语言F！其特点是，它构成了FLINT [18]和TILT [8]的基础。1 电子邮件：carsten@ cs. yale。edu2 电子邮件地址：yu@cs.yale.edu3 电子邮件：nzz@cs.yale.edu4 这项工作得到了NSF Grants CCR-9901011和CCR-0081590的c 2001年由Elsevier Science B出版。诉 在CC BY-NC-ND许可下开放访问。2一般来说，从一种语言到另一种语言的编译是用判断和推理规则来表示的合理性的争论通常留给语言设计者，他们通常用铅笔和纸非正式地推理语言的属性考虑到这些中间语言的设计本身就是一项具有挑战性的工程任务，并且在安全性方面如此依赖于它，是否真正满足所需属性的问题至关重要。这些属性的示例包括静态和动态语义的正确性、主题归约、进度、终止属性、观察等价性以及编译的可靠性和完整性。非正式证明往往容易出错。 从工程的角度来看，在正式的开发过程中，维护一组有效的定理和证明是很困难的。出于这个原因，我们主张在本文中使用元逻辑框架来指定，实现和验证设计。元逻辑框架，如Coq [4]，Nuprl [1]和Isabelle/HOL [13]，例如精心制作和复杂的交互式证明搜索工具。为了使用这些工具，必须致力于一种特定的方式来表示所涉及的推理系统。特别是，类型关系和操作语义的表示，例如，通常具有非常优雅和表达性的高阶编码，在Coq，Nuprl或Isabelle/HOL中不直接支持，因为使用什么归纳原则的问题是有问题的[3，9]。然而，这些系统的真正高阶编码提供了巨大的优势，因为与替换和弱化相关的某些引理在本文中，我们使用BMF [16]作为规范、算法及其元理论的表示语言。从实现者的角度来看，每种中间语言和每种类型系统都需要不同的类型检查器实现。我们在这张纸上显示的是F！例如，如何静态键入可以成为表示的一部分。因此，LF类型检查器可以决定一个项是否为well-t ped。F的脏话！ 在我们的代表中是无法被简单地描述的。我们展示了这种设计的类型可靠性的实现证明本文的组织结构如下。 我们将在第2节中讨论BMF，引入F！ 在第3节中，讨论了第4节中关于替换问题，在第6节中展示类型可靠性之前，在第5节中给出了一个约简语义。第7节给出了如何使用我们的编码的示例第8节概述了今后的工作并评估了成果。2布拉夫[16]是一个元逻辑框架，也是编程语言和逻辑理论中的实验工具。它支持各种任务，如对象语言及其语义的规范，操作对象语言表达式3和演绎，以及对象语言的元理论的形式发展。BJMF实现了逻辑框架LF[7]，它采用了判断作为类型，派生作为对象的方法论进行规范。我们的LF公式是标准的。类型K：：=类型jx：A：K j A！KTy pesA：：=aj AMj x：A1：A2j A1！A2ObM：：=cjx jx：：e jM1M2签名：：= j ;c：K j ;a：A上下文：：= J;x：A我们使用a表示类型常量，c表示对象常量，x表示变量。as- signs类型到变量。下面使用签名按照标准实践[14]，我们假设替换是捕获避免的，并省略类型中所有的前导抽象前缀。- 可兑换性被认为是定义平等的基本概念[2]。 A！K和A1 ！一个2 作为x：A：K和x：A1：A2的缩写，如果x在K和A2中不存在。 有时候我们把A1写成A2！一台2.作为LF的类型判断，如果对象M在文本中具有类型A，则我们写`M：A， 并且如果M是well-t-ped并且另外是规范（-normal，-long）形式，则写` M：c A。相应的推理规则可以在[7]中找到。3F！F！是Girard在其论文[5]中提出的一种证明高阶逻辑性质的方法在类型定向编译中，F！的表达能力使其成为FLINT系统[18]和TILT [8]核心的吸引人的它通过多态性和类型构造函数扩展了简单类型演算。种* = o j（1）第2项类型：：=j）j12j：：j 8：：Termse：：=xjx：：e je1e2 j：：e je[]有不同的方式来enco odeF！ 在LF。例如，一种方法是将表达式、类型和种类表示为单独的句法类别，然后显式地编码相关的类型关系。然而，出于这项工作的目的，我们选择了一种“隐式”表示法，并按种类和按类型的术语选择索引类型（见下文）。41 2 121 2 121n1nn1nkd：o型：kd）：kd！kd！ KD我们写p q的（多态）表示函数，嵌入的syn战术类别的F！ 在LF。定理3.1（编码的一致性：类）如果是类，则pq ：c k d。并且，如果`M：c kd，则存在一种，使得pq= M。F！ 是强正规化的，这似乎使LF的简单类型演算成为表示F的好的候选者！你直接就可以了。然而，这样的编码将是不令人满意的，因为它与多态量化不兼容。 所以我们要去F！- LF中的ty pe作为由它们各自的种类索引的t y p e族。TP ：kd！ 类型）0 ：tp（o）o）o）@0 ：tp（K）K）！ tpK！tpK^0：（tpK！ tpK）！tp（K）K）80：（tpK！ tpo）！TPO我们用一个撇号标记这些新定义的常数，因为我们在下面的原子形式和规范形式的其他推理规则中重用了相同的名称。这种选择使得编码定理和证明的签名更具可读性。定理3.2（编码的一致性：类型）如果是一种自由类型变量：* *：那么，：pq; ：;：pq`pq ：tppq. 与此同时，：pq; ：;：pq`M ：tpp q则存在一种类型：，s.t.p q= M。p q是组成的，因为p[=]0q=（：pq：p0q）pq。F！ 所有的O-约化都是在T_y_e_v上进行的，从而在表示为“12：. 为了避免 符号混乱，我们抑制上下文和善良简单地写上12、这个判断然而，重要的是要注意，所有的定义推理规则都依赖于参与类型是良好的。1n11n51 2 12122111nn12111nn0tbeta（* *（1）第2项[2=]1teta（ 不免费）**0高大0tlam8： ：8：：**0 0塔尔1122Tapp0 0））1212tref122313为本评估1221齐姆F的典型水平！ 形成强正规化演算[5]。在没有进一步讨论和形式化的情况下，我们假设这个事实是给定的，并将关于这个同余关系的元级属性的公式化留给未来的工作。 F！同时也满足了几项创新原则，这两点对本工作有重要意义。引理3.3（可接受的推理规则）(i) 如果））00然后 0的情况。(ii) 如果8**8： ：和00 那么[0= ][0= ]。1 21 2 1122引理3.3的同余关系和两个部分在LF中由图1所示的签名表示。仅对判断的编码就迫使一个全等的左手边和右手边是同一类型的。定理3.4（编码的一致性：同余关系）如果R是1的导子2 其中f ree变量在1 ：1; ：;n ：n，则：pq; u：**：pq; u：`pRq ：pq pq。相反，如果：pq; u：**：pq; u：`M：pqpq 则re存在s. t的导数R。 pRq=M。此外，p q是合成的，但仅就的导子而言。然而，这种组合性的有限性质对于一般情况是不充分的。引理4.1的主要结果是，在定理3.4中，0的偶数导子可以代替任意的ui。在[17]中给出了这种同余关系的实现。 规则上面的“tref”也是一个可接受的推理规则，但是我们选择不这样编码，而是实现可接受性证明。12211nnn11nnn06引理3.5（恒等引理）对于所有类型它认为.其在BMF中的编码为具有一组定义常数decla的类型族71 2 121111121211221 212：tp K！ tp K！ 类型tbeta：（（^0 （a：tpK：Ta））@0 T）TTteta ：T^0 （a：tpK：T@0 a）、tarr：））T1T2！ T2T3！T1T3高：（a：tpK：aa！T1aT0 a）！80不80的t0tapp：TT0！不T0！不@0 不 的t0 @0的t0tlam：（a：tpK：aa！ T1tsymm：T1T2！T2T1aT0 a）！^0不^0的t0tinv：）@0 不@0 T）@0的t0 @0的t0 ！不的t01 21222时间：80T80T0 ！TT0 ！TTT0的t0Fig. 1. 编码引理3.3可以在[17]中找到。识别码： T：tp K：TT！ 类型F调！，每一个等价类的模同余都有唯一的代表。它们被称为标准型，它们是（tbeta）-正规（teta）-长形式[5]。规范形式是根据两个判断来定义的，一个是针对规范类型的，它的定义是面向类的，另一个是针对原子类型的，它是面向类型的。“j”规则只适用于类型o。;#`*o8`8： ：*o;#1`*2个- -`： ：*（1）第2项`#oJ**o第二`#）`）#o）o）o1212118`1#2）1`2*2@`12#1图2给出了LF中原子和正则项的表示j的声明中的类型归属（T：tp o）是必要的，因为否则，Jumif会将更一般的类型'tp K'推断为参数类型。定理3.6（编码的精确性： 规范形式和原子形式）如果C是类型的规范形式派生自由类型变量1 ：91 2 121nn111nn111nnn可以：tpK！ 类型：TPK！ 类型8：（a：tpK：ata！ can（Ta））！可（80 T）^：（a：tpK：ata！ can（Ta））！可以（^0 T）j：at（T：tp o）！不可能）：at）0@：在T！ 能T！在（T@0 T）图二. 规范和原子类型的编码。**：那么，：pq; u：在**：pq; u：在`pCq：的情况。可以pq。与此同时，：pq; u：在**：pq; u：在的则存在一个导子C，它是canonic al，s.t.pCq=M。对称性适用于原子形式。注意，在这种情况下，p q是合成的，但只是在原子推导可以取代原子假设的意义用正则导子代替原子假设的更一般的情况也成立，如引理4.2所正则形式和原子形式的引入带来了其他好处，例如额外的反演引理（我们在这里只展示引理3.7（反演）如果8**0 和`0 * 0然后0 = 8个：：00对于一些00。引理3.7与引理3.3的区别在于八点语法上是相同的，而且不仅可以转换。因此，这个引理直接由LF支持，1nn1n10不需要额外编码按照我们最初的提议，我们将良好类型性条件作为BMPF编码的一部分，因此避免了类型关系的显式编码。一旦在LF中构造了一个项，这种技术就使我们不必运行单独的类型检查和类型规范化阶段。良好类型性条件被构建到表示中。11212exp：can（T：tp o）！ 类型abs：（expC1！ expC2）！ exp（j（）@C1）@C2）app：exp（j（）@C1）@C2）！ 实验C1！实验C2Abs：（a：tp K： u：at a：a一个！exp（C au））！实验（8 ℃）应用程序：exp（8（C：a：tpK：ata！can（T1a）！T：tpK：C0 ：canT ：R：TTT：C00 ：canT：expC00图三. 术语编码（x）= var`e：00聪`x：;x：1`e：2ABS` x：1：e：一个！ 2`e：一比二！1 `e2：2app第一卷第二章第一;：`e：的： ：e：8**ABS`e：8*1`2 ：`e[2]：[2=]1App术语应该如何表示？引入类型族并按类型对其进行索引的明显解决方案是不充分的，因为类型不是唯一的。每个术语都有几种类型，模“cong”规则的应用，并且在类型级别上不存在任何期望的反演原理。另一种成功的解决方案是规定规则中的所有类型都必须是规范的。这个解决方案相当于从上面的规则列表中省略“cong”，并以满足这个新约束的方式重写“App”规则。[2=]1 D oes不一定产生标准形式的Ty pe，但已知它全等于1，即0。`e：8：：1`2：[2=] 1`e[2]：App如果所有类型的术语都是规范的，则术语形成规则可直接表示为LF中的类型族，由证明其类型的规范性的证明对象索引。图3中给出了相0012应的常量声明。我们想对这一表述提出两点意见。 首先，rst声明中的注释（T：tpo）将术语限制为13111n1111n一种类型。第二，到目前为止提出的所有规则的公式化，特别是这些规则，充分利用了BMPF强大的类型重构能力。例如，（j（）@C1）@C2）是`absE'canonici ty的一个prof。它几乎读起来像它的类型。由于与充分性相关的原因，Abs的类型在参数a是原子的证明中是参数的。 另一个假设aa通过参数的自反性扩展了类型上的可转换关系。定理3.8（编码的一致性：项）设e是C是一个推导， 是canonical。如果e包含自由类型变量1：1; ：m：m 和f re ee项变量x1：1; ：;xn：n，（和Ci p roofs他们的标准），然后：tppq; ：：tppq; x ：exppCq; ：; x：exppCnq`peq：exppCq。并且，如果：tppq; ： ：m：tppmq; x：exppCq; ：; x：exppCq`M：exppCq. 则re存在te：0，s. t。peq=M和0。LF中的术语及其表示之间的双射对于术语是合成的，但对于类型不是。因此，必须单独考虑类型级别4取代F的特殊编码！上一节中的系统策略类别带来了许多广告，但也有一些令人失望的广告。 只会说脏话！术语是可表示的，然而，每当使用多态应用时，必须提供类型和相应规范形式的等价性的显式证明。因此，即使我们使用高阶抽象语法来编码多态抽象“Abs”的规则，我们也不能使用LF应用程序来模仿替换。当实例化自由类型变量时，术语的表示不是组合的，因为自由类型变量被规范类型假设为原子的。相反，我们必须在一个假设的规范性证明中证明所有的自由假设，并通过替换引理将结果转换为规范形式证明。在这一节中，我们将讨论同余关系、标准形和项的适当替换引理。事实上，这些引理分别建立了定理3.4、定理3.6和定理3.8的广义复合性性质。对于本节的剩余部分，请记住，我们假设所有术语都是良好类型的，所有类型都是良好类型的。引理4.1（代入同余关系）设340的种类。如果，在假设它是类型为0的类型变量的情况下，12是一种，然后[3=]1[4=]2。这个证明推广了Pfenning用多态量子表示的代换引理它被编码为一个类型族1MMn141221 21221 21thm-sub-c：（a：tpK0： aa！（Ta：tpK）Ta）！T3T4！T1T3T2T4！字体：[17]中给出了证明的实现。类型批注（T1 a：tp，K）用信号通知T wel f的类型重构算法，K不能依赖于类型。替换引理不仅对同余关系成立，而且对类型也成立。引理4.2（替换成规范/原子形式）(i) 对于所有的证据， ;：`0 *和`*存在一个00，因此[ = ]000 #21040;的证明” 。(ii) 所有证据表明：`0 #和`*存在一个00，因此[ = ]000 要么证明00 *或'00#。同样，这个引理可以在LF中通过两个相互依赖的类型族形式化。这一证明的编码在[17]中给出。主要的困难是引理第二部分的析取：00要么是正则的，要么是原子的。把这个逻辑连接词推入LF暗示了一个辅助的中间类型族“can_at”.can_at：tp K！字体：iscan：can T！can_at T：isat：at T！can_at T：substc：（a：tp K：at a！可以（T0 （a））！不可能！（T0 T）T00！可以T00！类型substa：（a：tp K：at a！at（T0a））！不可能！（T0T）T00！can_at T00！类型15最后，我们在术语级别上定义了一个替换应用[]e。子式定义为=1=1; ：;n=n，且所有i都是正则形式. 像往常一样，我们假设这些替换是通过默契避免捕获1612 12211211333R00：：[0=]（8：00： ）000by关于E的诱导性论文1变量重命名。[ ]（x）=（x）[]（x：：e）=x：0：[ ; x=x]e其中[]（）0和0 canonical[]（e1e2）=（[]e1）（[]e2）[]（： ：e）=： ：[ ; =] numerous[ ]（e[ ]）=（[ ]e）[0]其中[ ]（）0 和0规范[ ]（ ）=的（）下一页[]（））[ ]（）=0，其中（[ ] ）（[]）0和0规范[ ]（： ：）=的：：0 ，其中[ ; = ]0 和0 典型的[ ]（8： ：）= 8：：0，其中[ ; = ]0和0是标准的与内部编码为-redices的项替换e=x的应用不同，类型替换application =的表示是外部的。术语变量和类型变量都是通过高阶抽象语法表示的，但是-归约模型只替换前者。对于后者，我们观察到，对于自由类型变量的任何实例化，用\exp”记录的规范性证明可能会改变。因此，这种形式的替代应用必须从外部定义。它的定义是相当复杂的，并实现了以下替代引理的证明引理4.3（代入项）对于所有证明， ;：0 E：和`0 *0 存在00，因此[0=]00 并证明00 *和`[0=]e：00.我的律师。 通过对E的归纳。 我们只考虑e=e1的情况。 所有其他情况都是类似的。C0 ：：0* 0假设D ：：;：0 [1]：假设E ：：;：0娥：8：上午10：通过DC ：：;：0 *00通过DR：：[1=]2byin在D上的反转2000 = 8个：00：01引理3.7C000 “八点零分。 *o通过对E的归纳得出结论1117111E00 ：：`[0=]e：8：00：0在E1上通过诱导Hy论文0 ：：[0=]0引理4.2关于C; C0了c0 *`0 *00通过C上的引理4.2;C01 111R118311 122 1 2111424R00：：[0=][=][0= ]0by引理3.3（2）关于R00;R01 21 3 1C00 ：00 `0 *由C000上的版本提供r10的：：[0=]0by引理4.2关于C00;C02 1 3410 ：：`*oy引理4.2onC00;C0我：：0Lemma 3.5 on0Q：：[0= ][ = ][0=]通过引理4.1在R上;IQ ：：[0= ][0= ][=] by tsymm on QQ：：[0=][0=]0byttraonQ;R00;R031 34 22Q：：`（[0=]e）[0]：byApponE00;C0;R01141 2问：`[0= ]（e[]）：通过定义替换2当用一个类型替换表达式中的一个类型变量时，引理4.3的证明包含了一个算法，该算法是关于如何重新建立结果对象的类型的规范性证明的事实上，该算法定义了如何应用替换，并且在BMF中形式化如下：subst：C：（ a：tp K：u：at a：can（T a））：（a：tp K： u：在a： e：aa：exp（C a u））！可以T0！（T T0）T00！C00 ：canT00：expC00 ！泰培图4中描述了一个讨论过的证明案例所有其他案例都可以在[17]中找到。在这种表示中，用类型替换类型变量不仅仅是一种作用于术语的算法。它同时强制执行所有表示不变量在执行期间得到满足。有了这个替换引理，就有可能为F定义一个操作语义。 并提供进展、终止和最终的健全性。5归约语义我们已经选择了一个约简语义作为F的操作语义！，which|保存类型。|preserves types. 只有类型良好的表达式才计算为相同类型的表达式。 我们写E7！e0级 对于judgme nt，表达式ee的值为e0一步一个脚印！e0级如果它是任意的，但有很多步骤。求值符号的左右两侧始终是正确键入的。EV β（x： ：e）v 7！[v=x]e0埃夫·普贝塔（：：e）[ ] 7！[ =]e0e17！e10电动汽车应用程序1e27！e2C019evapp20e7！e0埃夫帕普e1e27！e1e2e1e27！e1e2e[ ]7！e []201 1111 C（ttra（ttra（tsymmQ）（tinvallR00R0））R0）C01spapp：subst（a：tpK0：u：ata：Dau）（a：tpK0：u：ata：i：aa：app（E a u i）（T a）（C a u）（R a i）（D au））C0(AppE00 不了c0r10的1C0）1 2 261 2 2subst（a：tpK0：u：ata：8（a1：tpK：a2：ata1：C2aua1a2））（a：tpK0：u：ata：Eau）C0 R00 （80 C00）E00substcC1了c0 R00substcC00了c0 r10的了c0ID T0I1 2 2thm-sub-c（a：tpK0：i：aa：Rai）IQ图 四、引理4.3的表示，情况e=e1[1]。没有损失的generali ty，F！的归约语义要求a -redex的索引是一个值。只有- and -抽象才被认为是值。图5给出了规则的表示6类型健全性通过构造，F！ 就是保存。评估规则的快速检查显示，重复应用的个别减少步骤必须终止，因为在一个术语（术语和类型级别）的redices的数量减少与每个单独的步骤。定理6.1（终止）如果e：，则从e开始的所有求值步骤序列都是nite。我们可以假设e是良好类型的上下文为空，因为归约语义不计算under-binders。因此，类型可靠性的问题简化为确保评估永远不会卡住的进度问题。定理6.2（进步）如果e：则要么e是一个值，要么存在一个e0，s. t。e7！ e0。这个定理的证明是通过在e上的归纳法。遗憾的是，目前尚处于初步阶段，不能自动证明进展定理一份手写的校样1