Rewriting Calculus with(out) Types

Horatiu Cirstea 1 Claude Kirchner 1 Luigi Liquori 2, 3
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 last few years have seen the development of a new calculus which can be considered as the outcome of the last decade of various researches on (higher order) term rewriting systems, and lambda calculi. In the Rewriting Calculus (or Rho Calculus), algebraic rules are considered as sophisticated forms of "lambda terms with patterns'', and rule applications as lambda applications with pattern matching facilities. The calculus can be "customized'' to work modulo sophisticated algebraic theories, like commutativity, associativity, associativity-commutativity, etc. This allows us to encode complex structures such as list, sets, and more generally objects. The calculus can be either be presented "a la Curry'' or "a la Church'' without sacrificing readability and without complicating too much the metatheory. Many static type systems can be easily plugged-in on the top of the calculus in the spirit of the rich "type-oriented'' literature. The Rewriting Calculus could represent a lingua franca to encode many paradigms of computations together with a formal basis used to build powerful theorem provers based on lambda calculus and efficient rewriting, and a step towards new proof engines based on the Curry-Howard isomorphism.
Type de document :
Communication dans un congrès
WRLA 2002, 4th International Workshop on Rewriting Logic and Its Applications, Pisa, Italy 19–21 September 2002, Sep 2002, Pisa, Italy. Elsevier, Electronic Notes in Theoretical Computer Science, 71, pp.3-19, 2002, 〈10.1016/S1571-0661(05)82526-5〉
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00100858
Contributeur : Luigi Liquori <>
Soumis le : mardi 12 mai 2015 - 14:47:14
Dernière modification le : jeudi 11 janvier 2018 - 16:30:51
Document(s) archivé(s) le : mercredi 19 avril 2017 - 22:17:33

Fichier

2002-wrla-02.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Horatiu Cirstea, Claude Kirchner, Luigi Liquori. Rewriting Calculus with(out) Types. WRLA 2002, 4th International Workshop on Rewriting Logic and Its Applications, Pisa, Italy 19–21 September 2002, Sep 2002, Pisa, Italy. Elsevier, Electronic Notes in Theoretical Computer Science, 71, pp.3-19, 2002, 〈10.1016/S1571-0661(05)82526-5〉. 〈inria-00100858〉

Partager

Métriques

Consultations de la notice

269

Téléchargements de fichiers

40