iRho: An Imperative Rewriting-calculus

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 big-step call-by-value operational semantics of iRho. 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-types, which can be assigned to terms-like structures (i.e., records). 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 of a pattern-matching imperative language, where a (monomorphic) typed store can be safely manipulated and where fixed-points are built-in into the language itself. Properties such as 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 :
Article dans une revue
Mathematical Structures in Computer Science, Cambridge University Press (CUP), 2008, 18 (03), pp.467-500. 〈Cambridge University Press〉. 〈10.1017/S0960129508006750 〉
Liste complète des métadonnées

Littérature citée [46 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01147678
Contributeur : Luigi Liquori <>
Soumis le : jeudi 30 avril 2015 - 19:14:34
Dernière modification le : vendredi 12 janvier 2018 - 11:03:46
Document(s) archivé(s) le : mercredi 19 avril 2017 - 12:22:21

Fichier

2008-mscs-08.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Luigi Liquori, Bernard Serpette. iRho: An Imperative Rewriting-calculus. Mathematical Structures in Computer Science, Cambridge University Press (CUP), 2008, 18 (03), pp.467-500. 〈Cambridge University Press〉. 〈10.1017/S0960129508006750 〉. 〈hal-01147678〉

Partager

Métriques

Consultations de la notice

163

Téléchargements de fichiers

109