On type-based termination and dependent pattern matching in the calculus of inductive constructions. (Terminaison basée sur les types et filtrage dépendant pour le calcul des constructions inductives)
On type-based termination and dependent pattern matching in the calculus of inductive constructions. (Terminaison basée sur les types et filtrage dépendant pour le calcul des constructions inductives)
复制标题
关于归纳结构演算中基于类型的终止和依赖模式匹配。
DOI：
--
复制
发表时间：
2011
期刊：
影响因子：
--
通讯作者：
J. Sacchini
中科院分区：
文献类型：
--
作者：
J. Sacchini
基于依赖类型理论的证明助手作为开发认证程序的工具正在获得采用。一个成功的例子是Coq proof assistant，它是一个依赖类型理论的实现，称为归纳构造演算（Calculus of Inductive Construction，CIC）。Coq是一种函数式编程语言，具有表达类型系统，允许在高阶谓词逻辑中指定和证明程序的属性。基于Coq的成功和提高其可用性的愿望，本文研究了Coq及其基础理论CIC当前实现的一些局限性。我们提出了两个扩展的CIC，部分克服了这些限制，并作为未来实现Coq的理论基础。首先，我们研究递归函数的终止性问题。在Coq中，所有递归函数都必须终止，以确保底层逻辑的一致性。目前的终止性检查技术都是基于语法标准的，它们的局限性在实践中经常出现。我们提出了使用基于类型的机制来确保递归函数终止的CIC扩展。我们的主要贡献是证明了强规范化和逻辑一致性的扩展。其次，我们研究了CIC中的模式匹配定义。使用依赖类型，可以通过模式匹配编写比传统函数式编程语言（如Haskell和ML）更精确和更安全的定义。基于依赖类型编程语言如Epigram和Agda的成功，我们开发了具有类似功能的CIC扩展。
Proof assistants based on dependent type theory are gaining adoption as a tool to develop certified programs. A successful example is the Coq proof assistant, an implementation of a dependent type theory called the Calculus of Inductive Constructions (CIC). Coq is a functional programming language with an expressive type system that allows to specify and prove properties of programs in a higher-order predicate logic. Motivated by the success of Coq and the desire of improving its usability, in this thesis we study some limitations of current implementations of Coq and its underlying theory, CIC. We propose two extension of CIC that partially overcome these limitations and serve as a theoretical basis for future implementations of Coq. First, we study the problem of termination of recursive functions. In Coq, all recursive functions must be terminating, in order to ensure the consistency of the underlying logic. Current techniques for checking termination are based on syntactical criteria and their limitations appear often in practice. We propose an extension of CIC using a type-based mechanism for ensuring termination of recursive functions. Our main contribution is a proof of Strong Normalization and Logical Consistency for this extension. Second, we study pattern-matching definitions in CIC. With dependent types it is possible to write more precise and safer definitions by pattern matching than with traditional functional programming languages such as Haskell and ML. Based on the success of dependently-typed programming languages such as Epigram and Agda, we develop an extension of CIC with similar features.