Rewriting Calculus with Fixpoints: Untyped and First-order Systems

Horatiu Cirstea 1 Luigi Liquori 2, 3 Benjamin Wack 1
1 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
3 MIRHO - Objects, types and prototypes : semantics and validation
CRISAM - Inria Sophia Antipolis - Méditerranée , UHP - Université Henri Poincaré - Nancy 1, Université Nancy 2, INPL - Institut National Polytechnique de Lorraine, CNRS - Centre National de la Recherche Scientifique : UMR7503
Abstract : The rewriting calculus, also called ρ-calculus, is a framework embedding λ-calculus and rewriting capabilities, by allowing abstraction not only on variables but also on patterns. The higher-order mechanisms of the λ-calculus and the pattern matching facilities of the rewriting are then both available at the same level. Many type systems for the λ-calculus can be generalized to the ρ-calculus: in this paper, we study extensively a first-order ρ-calculus à la Church, called ρstk→ . The type system of ρstk→ allows one to type (object oriented flavored) fixpoints, leading to an expressive and safe calculus. In particular, using pattern matching, one can encode and typecheck term rewriting systems in a natural and automatic way. Therefore, we can see our framework as a starting point for the theoretical basis of a powerful typed rewriting-based language.
Type de document :
Communication dans un congrès
Stefano Berardi and Mario Coppo and Ferruccio Damiani. Types for Proofs and Programs International Workshop, TYPES 2003, Torino, Italy, April 30 - May 4, 2003, Revised Selected Papers, Apr 2003, Turin, Italy. Springer Verlag, 3085, pp.147-161, 2003, Lecture Notes in Computer Science. 〈10.1007/978-3-540-24849-1_10〉
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00100113
Contributeur : Luigi Liquori <>
Soumis le : jeudi 7 mai 2015 - 14:07:18
Dernière modification le : samedi 27 janvier 2018 - 01:31:00
Document(s) archivé(s) le : mercredi 19 avril 2017 - 19:02:11

Fichier

2004-types-03.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Horatiu Cirstea, Luigi Liquori, Benjamin Wack. Rewriting Calculus with Fixpoints: Untyped and First-order Systems. Stefano Berardi and Mario Coppo and Ferruccio Damiani. Types for Proofs and Programs International Workshop, TYPES 2003, Torino, Italy, April 30 - May 4, 2003, Revised Selected Papers, Apr 2003, Turin, Italy. Springer Verlag, 3085, pp.147-161, 2003, Lecture Notes in Computer Science. 〈10.1007/978-3-540-24849-1_10〉. 〈inria-00100113〉

Partager

Métriques

Consultations de la notice

255

Téléchargements de fichiers

55