The Calculus of Algebraic Constructions

Abstract : This paper is concerned with the foundations of the Calculus of Algebraic Constructions (CAC), an extension of the Calculus of Constructions by inductive data types. CAC generalizes inductive types equipped with higher-order primitive recursion, by providing definitions of functions by pattern-matching which capture recursor definitions for arbitrary non-dependent and non-polymorphic inductive types satisfying a strictly positivity condition. CAC also generalizes the first-order framework of abstract data types by providing dependent types and higher-order rewrite rules.
Type de document :
Communication dans un congrès
Rewriting Techniques and Applications, 10th International Conference, RTA-99, Jul 1999, Trento, Italy. 1631, 1999, LNCS
Liste complète des métadonnées

https://hal.inria.fr/inria-00105545
Contributeur : Frédéric Blanqui <>
Soumis le : lundi 26 mai 2008 - 14:54:04
Dernière modification le : mardi 24 avril 2018 - 13:38:59
Document(s) archivé(s) le : mardi 21 septembre 2010 - 16:37:40

Fichiers

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

Identifiants

  • HAL Id : inria-00105545, version 2
  • ARXIV : cs/0610063

Collections

Citation

Frédéric Blanqui, Jean-Pierre Jouannaud, Mitsuhiro Okada. The Calculus of Algebraic Constructions. Rewriting Techniques and Applications, 10th International Conference, RTA-99, Jul 1999, Trento, Italy. 1631, 1999, LNCS. 〈inria-00105545v2〉

Partager

Métriques

Consultations de la notice

156

Téléchargements de fichiers

74