iRho: an imperative rewriting calculus
Luigi Liquori, Bernard Serpette · Mathematical Structures in Computer Science · 2008
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 both a static and big-stepcall-by-valueoperational semantics of iRho. The operational semantics is deterministic, and immediately suggests how an interpreter for the calculus may be built. The static semantics is given using a first-order type system based on a form of product types, which can be assigned to term-like structures (that is, records). The calculus isà laChurch, that is, pattern abstractions are decorated with the types of the free variables of the pattern. iRho is a good candidate for the core of a pattern-matching imperative language, where a (monomorphic) typed store can be safely manipulated and where fixed points are built into the language itself. Properties such as determinism of the interpreter and subject-reduction have been completely checked using a machine-assisted approach with theCoqproof assistant. Progress and decidability of type checking are proved using pen and paper.