Skip to Main content Skip to Navigation
Journal articles

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.
Complete list of metadatas

Cited literature [46 references]  Display  Hide  Download

https://hal.inria.fr/hal-01147678
Contributor : Luigi Liquori <>
Submitted on : Thursday, April 30, 2015 - 7:14:34 PM
Last modification on : Saturday, January 27, 2018 - 1:32:20 AM
Long-term archiving on: : Wednesday, April 19, 2017 - 12:22:21 PM

File

2008-mscs-08.pdf
Files produced by the author(s)

Identifiers

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. ⟨10.1017/S0960129508006750⟩. ⟨hal-01147678⟩

Share

Metrics

Record views

300

Files downloads

364