Combining Higher-Order and First-Order Computation Using Rho Calculus: Towards a Semantics of ELAN

Horatiu Cirstea 1 Claude Kirchner 1
1 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : The recently introduced rewriting calculus permits to express in a uniform and simple way first-order rewriting, lambda-calculus and non-deterministic computations as well as their combination. In this work, we recall the main properties of the rewriting calculus and we give a full first-order presentation of this rewriting calculus using an explicit substitution setting that generalizes the lambda-sigma-calculus. Its basic properties in the untyped as well as typed cases are presented. We then detail how to use the rewriting calculus to give an operational semantics to the rewrite based language ELAN.
Type de document :
Communication dans un congrès
FroCoS'98, 1998, Amsterdam, The Netherlands, 25 p, 1998
Liste complète des métadonnées

https://hal.inria.fr/inria-00098808
Contributeur : Publications Loria <>
Soumis le : mardi 26 septembre 2006 - 08:38:46
Dernière modification le : jeudi 11 janvier 2018 - 06:19:58

Identifiants

  • HAL Id : inria-00098808, version 1

Collections

Citation

Horatiu Cirstea, Claude Kirchner. Combining Higher-Order and First-Order Computation Using Rho Calculus: Towards a Semantics of ELAN. FroCoS'98, 1998, Amsterdam, The Netherlands, 25 p, 1998. 〈inria-00098808〉

Partager

Métriques

Consultations de la notice

85