The rho cube : some results, some problems

Horatiu Cirstea 1 Claude Kirchner 1 Luigi Liquori 2, 3 Benjamin Wack 1, 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 rewriting calculus embeds in a same setting the lambda calculus and the rewriting, by allowing abstraction not only on variables but also on patterns. The higher-order mechanisms of the lambda-calculus and the pattern matching facilities of the rewriting are then both available at the same level. It is worth noticing that the complexity of the calculu breaks the confluence property, so that we need to define appropiate strategies or restrictions, in order to recover it. We choose here to look at the rho-calculus as an extension of the lambda-calculus, and we study the typed aspects. Our study is based upon a generalization of Barendregt's lambda-cube, in which we unify both abstractors lambda and Pi into a single one. We need to deal with the original features of the rho-calculus too: matching power, non-determinism, confluence issues. With proper restrictions, we have proved most of the usual properties for typed calculi: substitution lemma, correctness of types, subject reduction, consistency. Uniqueness of typing is generally no longer valid but we can still prove it for one of the most restrictive systems, rho-> and rho2.
Type de document :
Communication dans un congrès
First International Workshop on Higher-Order Rewriting Copenhagen, Denmark, July 21st, 2002 Affiliated with RTA 2002, Jul 2002, Copenhague, Denmark. 2002
Liste complète des métadonnées

https://hal.inria.fr/inria-00099411
Contributeur : Publications Loria <>
Soumis le : mardi 26 septembre 2006 - 09:01:59
Dernière modification le : jeudi 11 janvier 2018 - 16:44:57
Document(s) archivé(s) le : vendredi 25 novembre 2016 - 11:56:55

Fichiers

Identifiants

  • HAL Id : inria-00099411, version 1

Collections

Citation

Horatiu Cirstea, Claude Kirchner, Luigi Liquori, Benjamin Wack. The rho cube : some results, some problems. First International Workshop on Higher-Order Rewriting Copenhagen, Denmark, July 21st, 2002 Affiliated with RTA 2002, Jul 2002, Copenhague, Denmark. 2002. 〈inria-00099411〉

Partager

Métriques

Consultations de la notice

239

Téléchargements de fichiers

38