Under consideration for publication in Math. Struct. in Comp. Science iRho: An Imperative Rewriting-calculus

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