iRho: An Imperative Rewriting Calculus [Extended Abstract]

Luigi Liquori 1, 2 Bernard Serpette 3
1 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
3 OASIS - Active objects, semantics, Internet and security
CRISAM - Inria Sophia Antipolis - Méditerranée , COMRED - COMmunications, Réseaux, systèmes Embarqués et Distribués
Abstract : We propose an imperative version of the Rewriting-calculus, a calculus based on pattern-matching, pattern-abstraction, and side-effects, which we call iRho. We formulate a static and a call-by-value dynamic semantics of iRho like that of Gilles Kahn's Natural Semantics. The operational semantics is deterministic, and immediately suggests how to build an interpreter for the calculus. The static semantics is given via a first-order type system based on a form of product-type, which can be assigned to iRho-terms like structures (i.e. pairs). The calculus is a la Church, i.e. pattern-abstractions are decorated with the types of the free variables of the pattern. iRho is a good candidate for a core or an intermediate language, because it can safely access and modify a (monomorphic) typed store, and because fixed-points can be defined. Properties like determinism of the interpreter, and subject reduction are completely checked by a machine assisted approach, using the Coq proof assistant. Progress and decidability of type-checking are proved by pen and paper.
Type de document :
Communication dans un congrès
Proceedings of the 6th ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming, Aug 2004, Verona, Italy. ACM, pp.167-178, 2004, <10.1145/1013963.1013983>
Liste complète des métadonnées

https://hal.inria.fr/hal-01149659
Contributeur : Luigi Liquori <>
Soumis le : jeudi 7 mai 2015 - 14:35:09
Dernière modification le : jeudi 16 mars 2017 - 01:08:32

Fichier

2004-ppdp-04.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Luigi Liquori, Bernard Serpette. iRho: An Imperative Rewriting Calculus [Extended Abstract]. Proceedings of the 6th ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming, Aug 2004, Verona, Italy. ACM, pp.167-178, 2004, <10.1145/1013963.1013983>. <hal-01149659>

Partager

Métriques

Consultations de
la notice

228

Téléchargements du document

41