The Rho Cube

Horatiu Cirstea 1 Claude Kirchner 2, 1 Luigi Liquori 3, 4
1 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
4 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, or Rho Calculus, is a simple calculus that uniformly integrates abstraction on patterns and non-determinism. Therefore, it fully integrates rewriting and lambda-calculus. The original presentation of the calculus was untyped. In this paper we present a uniform way to decorate the terms of the calculus with types. This gives raise to a new presentation a la Church, together with nine (8+1) type systems which can be placed in a rho-cube that extends the lambda-cube of Barendregt. Due to the matching capabilities of the calculus, the type systems use only one abstraction mechanism and therefore gives an original answer to the identification of the standard ``lambda'' and ``Pi'' abstractors. As a consequence, this brings matching and rewriting as the first class concepts of the Rho-versions of the Logical Framework (LF) of Harper-Honsell-Plotkin, and of the Calculus of Constructions (CC) of Coquand-Huet.
Type de document :
Communication dans un congrès
4th International Conference on Foundations of Software Science and Computation Structures - FOSSACS 2001, Apr 2001, Genova, Italy. 15 p, 2001, 〈10.1007/3-540-45315-6_11 〉
Liste complète des métadonnées

https://hal.inria.fr/inria-00107877
Contributeur : Publications Loria <>
Soumis le : jeudi 19 octobre 2006 - 09:12:44
Dernière modification le : jeudi 11 janvier 2018 - 16:24:42
Document(s) archivé(s) le : mercredi 29 mars 2017 - 13:30:58

Identifiants

Collections

Relations

Citation

Horatiu Cirstea, Claude Kirchner, Luigi Liquori. The Rho Cube. 4th International Conference on Foundations of Software Science and Computation Structures - FOSSACS 2001, Apr 2001, Genova, Italy. 15 p, 2001, 〈10.1007/3-540-45315-6_11 〉. 〈inria-00107877〉

Partager

Métriques

Consultations de la notice

205

Téléchargements de fichiers

57