Liquori and Serpette present a calculus called iRho. This calculus is a refinement of the Rho calculus introduced by Christea, Kirchner, and Liquori [1]. While Rho is a rewrite-based calculus, iRho is an “imperative rewriting calculus.” Concepts available in iRho are matching, rewriting, and functions (as in Rho), as well as references, memory allocation, and assignment.

After introducing the syntax of iRho (which includes types, contexts, patterns, and terms), the imperative operational semantics of iRho is described in some depth. This semantics is a call-by-value semantics, given by a set of 17 rules. The type system of iRho is then defined, in a more or less obvious way, by a set of type rules, including rules for terms and patterns.

The most interesting part of the paper is devoted to two examples. In the first example, the authors demonstrate how to compute negation normal forms in iRho. This is used to derive a decision procedure. The second example then explains how to define fixed-points in iRho. This example also shows that iRho is a calculus that might gain some practical relevance, since fixed-points are an essential mechanism for calculi describing real-life programming languages.