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.
Document type :
Conference papers
Liste complète des métadonnées

https://hal.inria.fr/inria-00098808
Contributor : Publications Loria <>
Submitted on : Tuesday, September 26, 2006 - 8:38:46 AM
Last modification on : Thursday, January 11, 2018 - 6:19:58 AM

Identifiers

  • 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. ⟨inria-00098808⟩

Share

Metrics

Record views

92