Addressed term rewriting systems: application to a typed object calculus
Daniel J. Dougherty, Pierre Lescanne, Luigi Liquori · Mathematical Structures in Computer Science · 2006
We present a formalism called addressed term rewriting systems, which can be used to model implementations of theorem proving, symbolic computation and programming languages, especially aspects of sharing, recursive computations and cyclic data structures. Addressed Term Rewriting Systems are therefore well suited to describing object-based languages, and as an example we present a language called and prove a type soundness result.