理论计算机科学电子笔记174（2007）95-108www.elsevier.com/locate/entcs机械化元理论的列表机基准（扩展摘要）Andrew W. Appel1普林斯顿大学计算机科学系，35 Olden Street，Princeton，NJ 08540，USA和INRIA Rocquencourt，B.P.105，78153 Le Chesnay，FranceXavier Leroy2INRIA Rocquencourt，B.P.105，78153 Le Chesnay，France摘要我们提出了一个基准比较定理证明系统的能力，表达编译器的正确性证明。与第一个POPL标记相反，我们强调证明与编译器实现的联系，并且我们指出，许多事情可以在没有绑定器或alpha转换的情况下完成。 我们提出了评估机械化元理论系统效用的具体标准;我们已经在Coq元理论和Coqf元理论中构建了解决方案，并且我们特别得出了关于这两个系统的结论关键词：定理证明，证明助手，程序证明，编译器验证，类型化机器语言，元理论，Coq，Coqf。1如何评价机械化的元理论POPLmark挑战赛[3]旨在比较几种自动化证明助手的可用性，这些自动化证明助手用于机械化可能由POPL论文作者完成的编程语言证明，基准问题正式化”。第一个POPLmark例子都在F理论中<：并强调粘合剂理论（例如，α转换）。关于真实编译器的机器检查证明的实践者有相似但不相同的兴趣我们希望正式地将机器检查的证明与行为实现联系起来，而不是将其与LATEX文档联系起来。 为了更好的生活，1电子邮件地址：appel@princeton.edu2电子邮件：Xavier. inria.fr1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2007.01.02096A.W. Appel，X.Leroy/Electronic Notes in Theoretical Computer Science 174（2007）95也许是“运动方面”的错误做法。. .很难正式化。”绑定器和αβ-转换当然是有用的，但它们对于证明关于真实编译器的真实事物并不是必不可少的，正如几个重要的编译器验证项目[9，10，13，6，7，8]所展示的那样。如果机器检查证明在提供真实系统的保证方面是有用的，让我们发挥它的优势，而不是它的弱点。因此，我们设计了一个实际的机器检查元理论示例它完全是一阶的，不需要绑定器或alpha转换。我们定义了一个简单的指针机器（cons，car，cdr，branch-if-nil）的结构化操作语义（SOS），并给出了一个简单的类型系统，其中包含了list-of-τ和nonempty- list-of-τ的构造函数。该基准明确地涵盖了类型系统的证明与可执行类型检查器的证明之间的关系。挑战在于表示类型系统，证明类型系统的可靠性，表示类型检查算法，并证明该算法正确地实现了类型系统。我们已经实现了在Coq和Biferf元理论的基准，我们得出结论，这两个系统的可用性。我们缺乏空间在这里介绍，但在全文中讨论[1]，• 实现者（可证明正确的编译器和可证明可靠的类型检查器）的需求如何• 整个问题的详细说明，如建议的谓词和推理规则的抽象• 了解我们的Coq和Coqf解决方案的详情;• 更多关于在Coq和Coqf中哪些子任务容易或困难的细节• 根据现有的文档，学习Coqf和Coq是多么容易除了基准测试之外，列表机也是学习Coq或Coqf的学生的有用练习;我们在Web上展示了我们解决方案的大纲（删除了证明）。2问题的具体化机器语法。 机器值A是cons cell和nil。a：A：：=零|cons（a1，a2）A.W. Appel，X.Leroy/Electronic Notes in Theoretical Computer Science 174（2007）9597机器的说明如下：I：I：：=jumpl（jump to labell）|branch-if -nil v l（如果v=nil，则转到l）|fetch-fieldv 0vJ（fetch the head ofv intovJ）|fetch-fieldv 1vJ（fetch the tail ofv intovJ）|consv0v1vJ（在vJ中创建一个cons单元格）| halt(stop executing)|i0;i1（顺序组合）在上面的语法中，元变量vi的范围是变量;变量本身vi由自然数枚举。类似地，元变量li的范围在程序标签Li上。程序是一系列指令块，每个指令块前面都有一个标签。p：P：：=L n：i; p| end操作语义学。机器状态是当前指令的（r，i）i和将值与变量相关联的存储r。我们写r（v）=a意味着a是r中变量v的值，而r[v：=a]=rJ意味着用绑定[v：=a]更新r会产生唯一的存储rJ。机器的语义定义如下：pJJ通过以下规则定义的最小步骤关系（r，i）›→（r， i），普吉J这是一个关系式，（r，i）→（r， i）。 p（r，（i1;i2）;i3）›→（r，i1;（i2;i3））r（v）= cons（a0，a1）r[vJ：=a0]=rJr（v）= cons（a0，a1）r[vJ：=a1] =rJjpjpJ（r，（fetch-fieldv0v;i））<$→（r，i）（r，（fetch-fieldv1v;i））<$→（r，i）r（v0）=a0 r（v1）=a1 r[vJ：= cons（a0，a1）]=rJJpJ（r，（consv0v1v;i））›→（r，i）r（v）= cons（a0，a1）pr（v）= nilp（l）=iJPJ（r，（branch-if-nilvl;i））›→（r，i）（r，（branch-if-nilvl;i））›→（r，i）p（l）=iJPJ（r，jumpl）›→（r，ι）一个程序p运行，也就是说，如果它从一个初始状态执行到一个最终状态，那么它就运行。如果变量v0 = nil并且当前指令是L0处的指令，则状态是初始状态。如果当前指令是halt，则状态是最终状态{}[v ：= nil]=r普吉0p（L0）=i （r，i）›→（r，halt）p对于机器验证证明的基准来说，包含显式抽象每个构造函数和规则的名称。 我们的具体说明[1]就是这样做的。类型系统。我们将在每个程序点为每个活动变量分配一个列表类型。为了保证98A.W. Appel，X.Leroy/Electronic Notes in Theoretical Computer Science 174（2007）95某些操作的安全性，我们为非空列表和空列表提供了列表类型的精化特别地，fetch-field操作要求它们的列表参数具有非空列表类型，并且branch-if-nilA.W. Appel，X.Leroy/Electronic Notes in Theoretical Computer Science 174（2007）9599operation将其参数的类型细化为空或非空列表，这取决于分支是否被接受。τ：T：：=nil（包含nil的单例类型）| list τ(list whose elements have type τ)| listcons τ(non-nil list of τ)环境Γ是类型对一组变量的类型赋值我们使用一组常见的一阶语法规则，在列表类型的各种细化中定义明显的子类型ττJ，这些规则在大多数机械化的元理论我们将子类型化和依赖扩展到环境中。我们定义两个类型τ1和τ2的最小公共超型τ1Hτ2=τ3为最小的τ3，使得τ1<$τ3和τ1<$τ2。在操作语义学中，程序是一系列带标签的基本块。在我们的类型系统中，一个程序类型化，由一个变量类型化的环境关联到每个程序标签。我们写f（l）= r来表示r表示标记为l的块的条目上的变量的类型。指令类型。单个指令由判断指令I。直觉是，在程序类型化下，霍尔三元组Γ{i} ΓJ将前置条件Γ与后置条件ΓJ联系起来。Π►instr Γ{ι1} ΓJΠ ►instr ΓJ{ι2} ΓJJ计算器指令Γ{ι1;ι2}ΓJJr（v）= listτ （l）= r1r [v：= nil]= rJrjrr1instr r r{ branch-if -nilv l}（v：listconsτ， rJ）Γ（v）= listconsτ（l）= Γ1Γ[v：= nil]= ΓJΓJΓ1instr Γ{ branch-if -nilv l} ΓΓ（v）= nil（l）= Γ1ΓΓ1instrr Γ{ branch-if -nilv l} Γr（v）= listconsτ r [vJ：=τ]= rj{ fetch-fieldv 0vJ} rJΓ（v）= listconsτ Γ[vJ：= listτ]= Γj{ fetch-fieldv 1vJ} ΓJΓ（v0）=τ0 Γ（v1）=τ1 （listτ0）Hτ1= listτΓ[v：= listconsτ]=Γjinstr Γ{ consv0v1v} ΓJ阻止打字。块是一条不（静态地）继续另一条指令的指令，因为它以跳转结束块I2块11;块12n（l）= r1 rn r1块跳跃程序类型。我们写|如果对于p中的每个标记块l：i，块i具有在p中给出的前提条件l（l）= r，即，l; r =块i，则说程序p具有程序类型l。此外，我们要求：（L0）= v0：nil，{}，并且在中声明的每个标签l都在p中定义。类型系统与类型检查器。我们已经提出了一些由推导规则定义的关系和一些非正式定义的关系。这有点草率，尤其是在100A.W. Appel，X.Leroy/Electronic Notes in Theoretical Computer Science 174（2007）95推导规则指的是一种非正式定义的关系; 2任何对基准的解决方案我们将使用符号|=progp：表示程序p在（不一定是算法的）类型系统中具有类型，符号progp：表示p：是在某种算法类型检查器中导出的。全文[1]概述了两个这样的算法类型检查器。一个是写在伪代码，并且对应于以命令式或函数式风格实现的类型检查器另一种是对上面给出的推导规则进行细化，使它们完全语法导向，因此可以作为逻辑程序来实现。示例程序。下面的列表机程序有三个基本块。变量v0被初始化为nil，如操作语义所规定的。 Block 0将block1切换到列表cons（nil， cons（nil， nil））并跳转到block 1。 块1 是一个循环，当v1不为nil时，获取v1的尾部并继续。块1的最后一条指令实际上是死代码（从未到达）。块2是循环出口，并停止。p样本=L0： cons v0 v0 v1; cons v0 v1 v1; cons v0 v1 v1; jump L1;L1：branch-if -nil v1L2; fetch-field 1 v1 v1; branch-if -nil v0L1; jumpL2;L2：halt;端该程序是良好的类型与sample= L0：（v0：nil，{ }）， L1：（v0：nil， v1：list nil，{ }）， L2：{}，{}3机械化任务在机械化元理论（MM）中实现1.表示MM中的操作语义。2.推导出p样本为n的事实。 MM应该方便地模拟小示例的执行，这样用户就可以调试SOS并对其表现力有直观的感觉。类型系统的可靠性。3.表示MM中的类型系统（定义足够的符号来表示公式|= progp：n和可以证明类型可靠性的推理规则）。4.在MM中表示最小公共超型的算法，即计算τ1Hτ2=τ3从输入τ1和τ2产生τ3。5.使用类型系统，导出以下事实：|= progpsample：prog p sample。MM应该方便地模拟小示例的类型检查，这样用户就可以调试类型系统并感受它的表现力。6.表示最小公共超类型的定义属性的声明τ1Hτ2= τ3<$τ1 <$τ3。7.证明H算法具有这些性质。A.W. Appel，X.Leroy/Electronic Notes in Theoretical Computer Science 174（2007）951018. 表示类型系统的可靠性定理的陈述。可靠性的非正式表述是：“一个类型良好的程序不会卡住。”如果程序步进或停止，则程序状态不会被卡住：|=p: Πinitial(p, r,ι)普吉JprogJJJJJJpJJJJ（r，i）›→（r， i）J健全性（r ， i。 （r，i）›→（r，i）） 停9.证明可靠性定理。全文[1]概述了这个证明的主要引理，这是类型保持和进步的标准论点。有效的类型检查算法。10.在MM中给出了一个渐近有效的类型检查算法-11.使用类型检查算法，计算campprogpsample：campsample。MM应模拟在小输入上执行算法。12.证明类型检查算法在任何程序上终止。13.在大规模示例上演示类型检查器，并具有良好的性能。通常，这将通过自动转换为Prolog或ML来完成，然后由优化编译器编译。14.证明：progp：意味着|= progp：也就是说，类型检查器可靠地实现了类型系统。写论文。15.我们可以通过一个简单的方法来生成一个LATEX，用于SOS规则、类型规则以及最小公共超型引理和可靠性定理的陈述（而不是证明）。Klein和Nipkow [6]证明这在Java子集编译器的Isabelle/HOL形式化中非常好4一个关于BMF元理论的BLOMF系统[12]是爱丁堡逻辑框架（LF）的一个实现。可以将逻辑的操作符表示为LF中的类型构造器，并将该逻辑中的证明表示为LF中的项，并且可以通过对项进行类型检查（将它们视为派生）来进行证明检查在逻辑推理中，人们可以证明定理（逻辑中的证明）或元定理（关于逻辑的证明）。这两种方法都可以用于我们的基准。我们的解决方案使用的是BMPF中常用的方法，这是元理论。在这种情况下，所讨论的逻辑是我们的操作语义和我们的类型系统，要证明的元定理是类型可靠性：也就是说，如果可以组合类型系统的推理规则来产生类型检查的派生，那么必须可以组合SOS的推理规则来产生（仅）执行的非卡住派生。这种方法是积极的句法。而不是说p是一个映射从标签到指令，我们给出的句法结构（我们声称）代表这样的映射。这种 风格的一个后果是，|= progp：不只是一个102A.W. Appel，X.Leroy/Electronic Notes in Theoretical Computer Science 174（2007）95语义关系，但句法推导一个表示为霍恩子句。通过仔细构造定义我们的关系的Horn子句，以便我们可以识别这种输入-输出组织可以通过%模式声明指定和机械检查。然后我们的类型系统可以直接在BMPF中执行在BLOOIF中的每个子句都被命名。当Prolog函数通过Prolog风格的回溯追踪成功应用子句的结果的一个或多个派生时，它也为每个派生构建一个派生树在LF中，我们也可以在导出树本身上进行计算。 假设我们编写另一个Prolog程序（子句集），它将派生树作为输入进行类型检查，并将派生树作为输出进行安全（非卡住）执行。如果这个程序是完全的（也就是说，在任何输入上成功终止），那么我们已经建设性地证明了任何类型良好的程序都是安全的。为了推理这个元程序，我们使用（机器检查的）%mode声明来解释什么是派生Transformer的输入和输出。我们还使用（机器检查的）%total声明来确保我们的元程序已经覆盖了可能出现的所有情况，并且我们的元程序不会在无限循环中。我们在第6节第6项和第7项中给出了这样一个证明的例子Beself有一个惊人的功能经济人们不必学习模块系统--因为根本就没有模块系统--只需对所有标识符使用命名约定人们不必学习如何使用大型的词元和策略库，因为没有词元和策略库：但这样的库不会那么有用，因为BMF几乎没有抽象特征，也没有多态性。所有的证明都是用证明元程序的整体性的简单机制来完成的这里有我们的Biferf证明从归纳定义自然数、标签、变量、类型结构和术语结构上的等式和不等式的概念开始。我们给出了良构环境的句法特征（即，不映射同一个变量两次）。有时候，对一个语义属性进行恰当的归纳句法定义是很棘手的。例如，考虑环境子类型，语义上为Γ1<$env Γ2 <$$> v. v∈ dom Γ2<$ $>（v∈dom Γ1<$ Γ1（v）<$Γ2（v））。一个的1Γ⊂{}Γ1（v）=τJ τJ <$τΓ1<$env Γ2 一个2r1=v：τ，r2在《易经》中，《易经》是一部经典，《易经》是一部经典。然而，这个定义对于有用的性质（传递性，反射性）来说并不是充分归纳的，至少我们不能证明它们。A.W. Appel，X.Leroy/Electronic Notes in Theoretical Computer Science 174（2007）95103问题似乎是，在规则a2中，Γ1不减小。下面的定义是正确归纳的--我们在规则b2的前提中使用ΓJ而不是Γ1。从这个定义证明传递性和自反性是容易的;困难的是避免浪费时间在上面的伪归纳定义上。.JJJJB1关于我们r1 =（v：τ，r）ττrenvr2Γ1谢琴夫v：τ，Γ2b25Coq中的一个证明Coq系统[5，4]是一个基于归纳构造演算的辅助证明系统.这种逻辑是类型论的一种变体，遵循从用户的角度来看，Coq提供了一种丰富的规范语言来定义问题这种语言包括：（1）具有所有常用连接词和量化器的构造性逻辑;（2）通过推理规则和公理进行归纳定义对于列表机器基准测试，我们使用了所有三种规范风格的组合，遵循类型系统研究论文中的常见做法操作语义和类型系统的推理规则被直接转录为归纳定义。对存储、环境和程序类型的操作，以及最小公共超类型和类型检查算法作为函数给出。最后，通过命题公式J J J Jv，与沃尔夫的元理论不同，Coq的逻辑提供了丰富的多态形式。这使我们能够通过重用有限映射的高效多态实现来分解存储、环境和程序类型的处理，作为Leroy早期开发的基数2搜索树，作为Compcert项目的一部分[8]。104A.W. Appel，X.Leroy/Electronic Notes in Theoretical Computer Science 174（2007）956机械化打样任务布拉夫Coq1.操作语义2.导出p1261988线3.类型系统|= progp：1671304.H算法**5.导出|= progpsample：prog p sample1没有6.H的态性质12137.证明H114218.状态可靠性定理29159.证明...的可靠性|= progp：Pi206031510.效率算法2214511.派生程序示例：程序示例1112.证明已终止运行程序p：18013.可缩放类型检查器是的是的14.证明P2P程序p：Pi的可靠性347141十五岁GnerateLATEX没有没有我们已经实现了那些可以在BMPF（元理论）和Coq系统中实现的任务。所需的代码行数汇总在上表中。解析和校对的总时间3，对于Cqref是0.558秒，对于Coq是2.622秒。1. 操作语义学。 Coq和Cof都使得表示SOS中的那种归纳定义变得容易和自然。在Coq中，还可以选择表示操作而不是映射（例如，在存储中查找和更新），或者作为关系（由归纳谓词定义），或者作为函数（由递归和模式匹配定义）。2. 导出p。Beself使得将归纳定义解释为逻辑程序变得非常容易。因此，这项任务在纳夫是微不足道的Coq不提供一种执行归纳定义的通用机制。然而，操作语义的规则足够简单，（经过一些实验）我们可以使用Coq的证明搜索工具（eauto策略）作为穷人的逻辑程序解释器。在Coq中执行归纳定义的一个更通用的方法，我们也实现了，是定义一个执行函数（61行），证明它相对于归纳定义的正确性（35行），然后执行函数。（函数程序的评估由Coq原生支持。3. 表示类型系统。在BMF和Coq中都是简单和自然的（和以前一样，Coq选择使用操作的函数表示而不是映射）。4. 最小上界算法因为在BNF中表示的“类型系统”是最直接地作为构造性算法来完成的，所以这已经在我们的BNF表示中作为任务3的一部分完成了。在Coq中，虽然类型系统本身不是算法的，但我们选择将最小上界操作指定为从类型对到类型的函数。因此，计算最小-3 Dell Precision 360，Linux，2.8 GHz Pentium 4，1 GB RAM，512 kB高速缓存。A.W. Appel，X.Leroy/Electronic Notes in Theoretical Computer Science 174（2007）95105在Coq开发中，上界也已经作为任务3的一部分完成5. 给出一个类型检查的例子。通过将类型系统作为逻辑程序来运行，这在BMPF中是微不足道的。在Coq中不直接可能，因为类型系统的指定不是算法的：它使用所有变量的通用量化来指定环境子类型。6. 最小上界的状态性质。在Coq中非常简单。 例如，下面是这些属性的Coq语句：引理lub_t2：对于所有t1 t2，lub t2 t1=lub t1t2。引理lub_subtype_left：对于所有t1 t2，子类型t1（lub t1 t2）。引理lub_subtype_right：对于所有t1 t2，子类型t2（lub t1 t2）。引理lub_least：for all t1 t3，subtype t1 t3->对于所有t2，子类型t2 t3->子类型（lub t1 t2）t3。与这些性质的数学陈述的对应是明显的。在BLF中，陈述最小上界的性质必须以一种起初似乎是人为的方式进行，但一旦学会就相当自然了。外稃τ1Hτ2=τ3τ1⊂ τ3lub-subtype-left被表示为逻辑编程谓词，lub-subtype-left：lub T1 T2 T3-> subtype T1 T3-> type。其将lubT1 T2 T3的派生转换为子类型T1 T3的派生。“证明”将由这个谓词上的逻辑编程子句组成。为了成为我们想要的属性的产品特性：%modelub-subtype-left+P1-P2。逻辑程序的模式指定哪些参数被认为是输入（+），哪些是输出（-）。一般来说，给定任何基项（即，不包含逻辑变量）P1，其类型为lubT1 T2 T3，我们的子句（如果它们终止）必须产生类型子类型T1 T3的输出P2，它们也是基础项。%总P1（lub-亚型-左侧P1和P2）。我们要求元定理检查我们的声明，即lub-subtype-left的执行不能在有限循环中执行：它必须失败或产生子类型T1T3的派生;我们检查执行永远不会失败的声明（所有情况都被覆盖）。在我们的%total声明中的两个地方使用P1（在某种意义上）是将要证明的东西与证明的一部分：我们指出归纳应该在lub-subtype-left的参数1上完成，而不是参数2。7. 证明最小上界的性质。 在BNF中，这是通过编写满足上述所有要求的逻辑编程子句来完成的。例如，以下9个条款将做到这一点：- ：lub-subtype-left lub-refl subtype-refl.106A.W. Appel，X.Leroy/Electronic Notes in Theoretical Computer Science 174（2007）95- ：lub-subtype-left lub-1 subtype-refl.- ：lub-子类型-左（lub-2 P1）（子类型列表P2）-lub-subtype-leftP1 P2。- ：lub-subtype-left（lub-2b P1）（subtype-listconsP3）<- lub-subtype-left P1 P3.- ：lub-子类型-左（lub-3 P1）（子类型列表P2）-lub-subtype-leftP1 P2。- ：lub-subtype-left lub-4 subtype-nil.- ：lub-subtype-left lub-5 subtype-nil.- ：lub-subtype-left lub-6（subtype-listcons subtype-refl）.- ：lub-subtype-left（lub-7 P1）（subtype-listmixedP2）<- lub-subtype-left P1 P2.这些不是类型检查器的子句，它们是关于类型检查器的子句，并且仅用于“证明”%mode和%total声明。在Coq中，证明是通过构造证明脚本来交互完成的。例如，lub_subtype_left的证明是：induction t1; destruct t2; destruct; auto; rewrite IHt1; auto.这相当于先对第一种类型t1的结构进行归纳，然后对第二种类型t2进行案例分析，再进行一些等式推理。Coq证明有6个独立的步骤，每个步骤只需要写两到三个令牌，每个步骤都需要用户思考。另一方面，BMF证明的9个子句中的每一个，大小从6到16个令牌不等，也需要一些思考。构建证明所需的时间或时间不一定与令牌计数成正比，但我们报告了我们采取的措施。8. 类型系统的状态可靠性定理。 在Coq中，这个陈述只是普通的数学。如上所述，在BMF中，这是通过编写一个逻辑谓词来完成的，该谓词将类型检查的派生与运行或停止的派生相关联，然后为BMF系统进行适当的%mode和%total声明以进行检查。9. 证明...的可靠性的类型系统用BMF编写这样一个逻辑程序需要2000多行;我们的全文[1]更详细地解释了这个证明。 Coq的可靠性证明大约短7倍（300行）。 那里 是Coq在这里优于Bisaf的几个原因。首先是Coq的打样自动化设备，它对许多中间打样非常有效：一旦我们手动指出归纳的结构，Coq的证明搜索策略通常能够从假设中自动得出结论。第二个原因是使用非算法规范，特别是对于环境子类型，这更容易推理。最后一个原因是能够重用映射上的基本属性，比如所谓的BASINF缺乏创建和重用抽象数据类型的能力，因此程序和证明的许多子句必须被复制和编辑。brief有一些证明自动化- % total声明计算结构归纳自动机-A.W. Appel，X.Leroy/Electronic Notes in Theoretical Computer Science 174（2007）95107并且（如果失败）打印一个报告，详细说明缺少的案例-但是它不能自动化案例分析。410. 渐近有效算法。在BASINF中，类型系统的最直接的表示，当作为算法运行时，需要二次时间。这是因为在全局环境中查找标签的规则需要搜索每个查找的标签长度。在任何允许有效动态断言新子句的Prolog系统中，可以在恒定时间内进行查找（Prolog系统内部使用散列）。BMF支持动态子句，因此我们可以编写一个很好的线性时间在Coq中，类型检查器被定义为从程序类型和程序到布尔值的函数。我们的解决方案使用中间函数来检查环境子类型以及类型检查指令和块。这些函数返回选项类型以通知键入错误，键入错误以一元样式传播为了避免n2算法，我们将环境和程序类型表示为由基数为2的搜索树实现的有限映射。因此，该算法的复杂度为O（nlogn）11.对新算法进行仿真。 这是一个微不足道的问题，无论是在巴夫和科克。同样，在BMPF中，我们在逻辑程序解释器中执行一行查询。在Coq中，我们简单地请求一个函数应用程序的求值（类型检查器对示例程序和程序类型的求值），这也是一行。12.证明类型检查器的终止。在逻辑程序（如类型检查器）的终止性证明中，归纳完全是结构性的，因此，Zerof有大量的自动化支持。这个任务在纳布卢斯很容易。在Coq中，这个任务甚至更容易：所有在Coq中可定义的函数都保证终止（特别是，所有递归必须是结构性的或由诺特归纳法建立的），所以这个任务没有什么需要证明的13. 工业强度的类型检查器。Coq有一个从Coq中表达的函数自动生成Caml程序的工具。从类型检查器的Coq函数规范中自动提取Caml代码，产生的代码接近于Caml程序员手工编写的代码，如果被限制到语言的纯函数子集。类似地，不使用高阶抽象语法的Prolog程序（例如我们的类型检查器）世界上有许多著名的Prolog编译器，其中有一个著名的Prolog编译器。14. 证明类型检查器的可靠性。在《古兰经》和《古兰经》中都是直截了当的（虽然有点繁琐）。同样，Coq4自动提供案例分析将是BMF元定理证明器的工作。 不幸的是，元定理证明器似乎不工作; BMF手册说， 人们怀疑最后两个词是否准确。108A.W. Appel，X.Leroy/Electronic Notes in Theoretical Computer Science 174（2007）9515. Genera teLATEX. 尽管Coq和Twel都 具 有 LATEX的功能，但它也有一个功能，即对于基准测试的实际应用来说，它是不可或缺的。7结论操作规范的语义属性的证明可以是积极的我们在本文中没有讨论这些方法，但是它们可以在Coq、Isabelle/HOL或嵌入在BMF中的对象逻辑中成功地机械化;然而，在BMF元理论中机械化语义证明似乎并不自然。或者证明可以是积极的Coq和Isabelle支持这种风格，而Besidf元理论只支持这种纯粹的证明理论风格。使用纯风格的好处是元理论本身可以更小更简单，使其更容易学习和推理。事实上，Bqf是一个比Coq更简单、更小的系统。在这两个极端之间，可以使用语义和句法推理的混合进行推理。那些认为自己是在用纯粹的赖特-费莱森风格写作的作者，经常会对环境和映射等事情进行语义推理。Coq系统相当好地支持混合风格（或两种极端风格中的任何一种）。因此，在Coq中表达的规格可能更接近于研究论文中所写的内容。 Coq证明可以大大短于Coqf证明，特别是当有经验的专家操纵战术语言时。因此，Coq可能是那些不想预先承诺纯证明理论风格的然而，我们的基准测试并没有运用BMPF系统的主要优势之一，高阶抽象语法和相关的证明机制。对于使用粘合剂和αβη-转换的句法理论，比较可能会有所不同。引用[1] Appel， A. W.和 X. Leroy ， A list-machine benchmark for mechanicalized metatheory ， Researchreport 5914，INRIA（2006）。[2] Appel，A.W.和X.Leroy，List-machine exercise （2006），http://www.cs.princeton.edu/搜索/listmachine/。[3] 艾德米尔湾E、A.Bohannon，N.福斯特湾Pierce，D.维提尼奥提斯，G. Washburn，S.Weirich，S.Zdancewic，M.Fairbairn和P.Sewell，The POPLmark Challenge（2005）http://fling-l.seas.upenn.edu/www.example.com[4] Bertot，Y. 和P. Cast'eran，“InteractiveTheoremPrvinganddPrgramDevelopmnt-Coq'Art：归纳构造的演算”，EATCSTextsinTheoreticalComputerScience，Springer-Verlag，2004。A.W. Appel，X.Leroy/Electronic Notes in Theoretical Computer Science 174（2007）95109[5] Coq证明助理 （1984http://coq.inria.fr/网站。[6] 克莱因，G.和T. Nipkow，A machine-checked model for a Java-like language，virtual machine andcompiler，ACM Transactions on Programming Languages and Systems28（2006），pp. 619-695[7] Leinenbach，D.，W. Paul和E. Petrova，Towards the formal verification of a C0 compiler，第三届软件工程与形式化方法国际会议（SEFM2005），2005年。2-11.[8] Leroy，X.，编译器后端的正式认证，或者：用证明助手编程编译器，在：POPL42比54[9] Moore，J.S.，一种机械验证的语言实现，自动推理杂志5（1989），pp. 461-492.[10] Moore，J.美国，[11] Pfenning，F.和C.Schuermann，《USAF用户http://www.cs.cmu.edu/www.example.comwww.example.com[12] Pfenning，F. 和DC。徐文，系统结构描述：面向推理系统的两种逻辑分析方法，载：CADE-16：第16届国际自动推理会议论文集，计算机科学讲义1632（1999），第110-202-206[13] Strecker，M.，Isabelle中Java编译器的正式验证，在：Proc. Conference on Automated Deduction（CADE），Lecture Notes in Computer Science2392（2002），pp. 63-77.[14] Wright，A.K. 和M.Felleisen，类型可靠性、信息和计算115（1994），pp. 38比94
我的内容管理
展开
