The simply typed rewriting calculus

Horatiu Cirstea 1 Claude Kirchner 1
1 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : The rewriting calculus is a rule construction and application framework. As such it embeds in a uniform way term rewriting and lambda-calculus. Since rule application is an explicit object of the calculus, it allows us also to handle the set of results explicitly. We present a simply typed version of the rewriting calculus. With a good choice of the type system, we show that the calculus is type preserving and terminating, i.e. verifies the subject reduction and strong normalization properties.
Type de document :
Communication dans un congrès
3rd International Workshop on Rewriting Logic & its Applications - WRLA2000, Sep 2000, none, 19 p, 2000
Liste complète des métadonnées

https://hal.inria.fr/inria-00099052
Contributeur : Publications Loria <>
Soumis le : mardi 26 septembre 2006 - 08:48:35
Dernière modification le : jeudi 11 janvier 2018 - 06:19:58
Document(s) archivé(s) le : mercredi 29 mars 2017 - 12:47:36

Fichiers

Identifiants

  • HAL Id : inria-00099052, version 1

Collections

Citation

Horatiu Cirstea, Claude Kirchner. The simply typed rewriting calculus. 3rd International Workshop on Rewriting Logic & its Applications - WRLA2000, Sep 2000, none, 19 p, 2000. 〈inria-00099052〉

Partager

Métriques

Consultations de la notice

81

Téléchargements de fichiers

36