Inductive-data-type Systems

Abstract : In a previous work (''Abstract Data Type Systems'', TCS 173(2), 1997), the last two authors presented a combined language made of a (strongly normalizing) algebraic rewrite system and a typed lambda-calculus enriched by pattern-matching definitions following a certain format, called the ''General Schema'', which generalizes the usual recursor definitions for natural numbers and similar ''basic inductive types''. This combined language was shown to be strongly normalizing. The purpose of this paper is to reformulate and extend the General Schema in order to make it easily extensible, to capture a more general class of inductive types, called ''strictly positive'', and to ease the strong normalization proof of the resulting system. This result provides a computation model for the combination of an algebraic specification language based on abstract data types and of a strongly typed functional language with strictly positive inductive types.
Type de document :
Article dans une revue
Theoretical Computer Science, Elsevier, 2002, 〈10.1016/S0304-3975(00)00347-9〉
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00105578
Contributeur : Frédéric Blanqui <>
Soumis le : vendredi 13 septembre 2013 - 12:32:14
Dernière modification le : jeudi 11 janvier 2018 - 06:20:11
Document(s) archivé(s) le : jeudi 6 avril 2017 - 19:25:19

Fichiers

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

Identifiants

Collections

Citation

Frédéric Blanqui, Jean-Pierre Jouannaud, Mitsuhiro Okada. Inductive-data-type Systems. Theoretical Computer Science, Elsevier, 2002, 〈10.1016/S0304-3975(00)00347-9〉. 〈inria-00105578v2〉

Partager

Métriques

Consultations de la notice

140

Téléchargements de fichiers

86