HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Journal articles

Rewriting and Multisets in Rho-calculus and 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 is a new calculus that integrates in a uniform and simple setting first-order rewriting, lambda-calculus and non-deterministic computations. The main design concept of the is to make all the basic ingredients of rewriting explicit objects, in particular the notions of rule application and multisets of results. This paper describes the calculus from its syntax to its basic properties in the untyped case. The rewriting calculus embeds first-order conditional rewriting and lambda-calculus and it can be used in order to give an operational semantics to the rewrite based language . We show how the set-like data structures are easily represented in ELAN and how this can be used in order to specify the Needham-Schroeder public-key protocol.
Document type :
Journal articles
Complete list of metadata

Contributor : Publications Loria Connect in order to contact the contributor
Submitted on : Tuesday, September 26, 2006 - 2:48:41 PM
Last modification on : Friday, February 4, 2022 - 3:29:53 AM


  • HAL Id : inria-00100656, version 1



Horatiu Cirstea, Claude Kirchner. Rewriting and Multisets in Rho-calculus and ELAN. Romanian Journal of Information Science and Technology, Romanian Academy, 2001, 4 (1-2), pp.33--48. ⟨inria-00100656⟩



Record views