论文标题
带有联合和交点类型的逻辑框架的类型检查器
A Type Checker for a Logical Framework with Union and Intersection Types
论文作者
论文摘要
我们介绍了基于三角洲框架的原型定理谚语的语法，语义和打字规则，即用著作中的先前论文中所述，以联合和交叉点类型进行装饰的完全型的lambda-calculus。 Bull还为Barbanera-Dezani-De'liguoro的类型理论实现了亚型算法。 Bull具有一个命令行界面，用户可以在其中声明公理，术语和执行计算以及一些基本终端式功能，例如错误漂亮打印，子表达突出显示和文件加载。此外，它可以打开证明或对其进行归一化。这些术语可能是不完整的，因此，Typechecking算法使用统一来尝试构建缺失的子。 Bull使用Berardi纯型系统的语法来改善核的紧凑性和模块化。抽象和混凝土语法主要是对齐的，并且类似于Coq的混凝土语法。 Bull使用高阶统一算法进行术语，而Typechecking和部分类型的推断是通过双向改进算法完成的，类似于Matita和Beluga中的一种。细化可以分为两个部分：精髓的完善和打字精致。使用常用的de Bruijn指数实施了粘合剂。我们已经定义了一种具体的语言语法，该语言将允许用户编写Delta-Terms。我们已经定义了还原规则和评估者。我们已经从头开始实施了炼油厂，该炼油厂会进行部分打字和键入重建。我们已经为公牛提供了交叉和工会文献的经典示例，例如通过Pfenning和他在LF中的改进类型形式上的牛。我们希望这项研究静脉对于在证明理论环境中实验吉拉德参数替代品的形式可能是有用的。
We present the syntax, semantics, and typing rules of Bull, a prototype theorem prover based on the Delta-Framework, i.e. a fully-typed lambda-calculus decorated with union and intersection types, as described in previous papers by the authors. Bull also implements a subtyping algorithm for the Type Theory Xi of Barbanera-Dezani-de'Liguoro. Bull has a command-line interface where the user can declare axioms, terms, and perform computations and some basic terminal-style features like error pretty-printing, subexpressions highlighting, and file loading. Moreover, it can typecheck a proof or normalize it. These terms can be incomplete, therefore the typechecking algorithm uses unification to try to construct the missing subterms. Bull uses the syntax of Berardi's Pure Type Systems to improve the compactness and the modularity of the kernel. Abstract and concrete syntax are mostly aligned and similar to the concrete syntax of Coq. Bull uses a higher-order unification algorithm for terms, while typechecking and partial type inference are done by a bidirectional refinement algorithm, similar to the one found in Matita and Beluga. The refinement can be split into two parts: the essence refinement and the typing refinement. Binders are implemented using commonly-used de Bruijn indices. We have defined a concrete language syntax that will allow the user to write Delta-terms. We have defined the reduction rules and an evaluator. We have implemented from scratch a refiner which does partial typechecking and type reconstruction. We have experimented Bull with classical examples of the intersection and union literature, such as the ones formalized by Pfenning with his Refinement Types in LF. We hope that this research vein could be useful to experiment, in a proof theoretical setting, forms of polymorphism alternatives to Girard's parametric one.
