On type-based termination and dependent pattern matching in the calculus of inductive constructions

Jorge Sacchini 1
1 MARELLE - Mathematical, Reasoning and Software
CRISAM - Inria Sophia Antipolis - Méditerranée
Abstract : 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.
Document type :
Theses
Liste complète des métadonnées

Cited literature [81 references]  Display  Hide  Download

https://pastel.archives-ouvertes.fr/pastel-00622429
Contributor : Bibliothèque Mines Paristech <>
Submitted on : Monday, September 12, 2011 - 2:15:00 PM
Last modification on : Thursday, January 11, 2018 - 4:20:55 PM
Document(s) archivé(s) le : Tuesday, November 13, 2012 - 10:21:37 AM

Identifiers

  • HAL Id : pastel-00622429, version 1

Collections

Citation

Jorge Sacchini. On type-based termination and dependent pattern matching in the calculus of inductive constructions. Performance [cs.PF]. École Nationale Supérieure des Mines de Paris, 2011. English. ⟨NNT : 2011ENMP0022⟩. ⟨pastel-00622429⟩

Share

Metrics

Record views

911

Files downloads

858