| Autor: |
Cirstea, Horatiu, Kirchner, Claude, Liquori, Luigi |
| Přispěvatelé: |
Constraints, automatic deduction and software properties proofs (PROTHEO), INRIA Lorraine, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique de Lorraine (INPL)-Université Nancy 2-Université Henri Poincaré - Nancy 1 (UHP)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique de Lorraine (INPL)-Université Nancy 2-Université Henri Poincaré - Nancy 1 (UHP), Logical Networks: Self-organizing Overlay Networks and Programmable Overlay Computing Systems (LOGNET), Inria Sophia Antipolis - Méditerranée (CRISAM), Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Environment for cooperation (ECOO), Objects, types and prototypes : semantics and validation (MIRHO), Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université Henri Poincaré - Nancy 1 (UHP)-Université Nancy 2-Institut National Polytechnique de Lorraine (INPL)-Centre National de la Recherche Scientifique (CNRS), LORIA, UMR 7503, Université de Lorraine, CNRS, Vandoeuvre-lès-Nancy |
| Jazyk: |
angličtina |
| Rok vydání: |
2000 |
| Předmět: |
|
| Zdroj: |
[Intern report] A00-R-344 || cirstea00d, LORIA, UMR 7503, Université de Lorraine, CNRS, Vandoeuvre-lès-Nancy. 2000, 18 p |
| Popis: |
Aussi apparu en "Proc. of FOSSACS, Foundations of Software Science and Computation Structures Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2001, Genova, Italy, April 2-6, Lecture Notes in Computer Sciences, no 2. Rapport interne.; 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. |
| Databáze: |
OpenAIRE |
| Externí odkaz: |
|
