The Implicit Calculus of Constructions as a Programming Language with Dependent Types

Bruno Barras 1, 2 Bruno Bernardo 1, 2
2 TYPICAL - Types, Logic and computing
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France, X - École polytechnique, CNRS - Centre National de la Recherche Scientifique : UMR
Abstract : In this paper, we show how Miquel's Implicit Calculus of Constructions (ICC) can be used as a programming language featuring dependent types. Since this system has an undecidable type-checking, we introduce a more verbose variant, called ICC* which fixes this issue. Datatypes and program specifications are enriched with logical assertions (such as preconditions, postconditions, invariants) and programs are decorated with proofs of those assertions. The point of using ICC* rather than the Calculus of Constructions (the core formalism of the Coq proof assistant) is that all of the static information (types and proof objects) is transparent, in the sense that it does not affect the computational behavior. This is concretized by a built-in extraction procedure that removes this static information. We also illustrate the main features of ICC* on classical examples of dependently typed programs.
Type de document :
Communication dans un congrès
FoSSaCS, Mar 2008, Budapest, Hungary. pp.365-379, 2008
Liste complète des métadonnées

Littérature citée [13 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00429543
Contributeur : Bruno Bernardo <>
Soumis le : mardi 3 novembre 2009 - 13:06:33
Dernière modification le : jeudi 10 mai 2018 - 02:06:34
Document(s) archivé(s) le : jeudi 17 juin 2010 - 19:11:39

Fichier

icc_barras_bernardo.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00429543, version 1

Collections

Citation

Bruno Barras, Bruno Bernardo. The Implicit Calculus of Constructions as a Programming Language with Dependent Types. FoSSaCS, Mar 2008, Budapest, Hungary. pp.365-379, 2008. 〈inria-00429543〉

Partager

Métriques

Consultations de la notice

226

Téléchargements de fichiers

216