A Language-Independent Proof System for Mutual Program Equivalence
Stefan Ciobaca and Vlad Rusu and Grigore Rosu and Dorel Lucanu
Two programs are mutually equivalent if they both diverge or they both terminate with the same result. In this paper we introduce a language-independent proof system for mutual equivalence, which is parametric in the operational semantics of two languages and in a state-similarity relation. We illustrate it on two programs in two dierent languages (an imperative one and a functional one), that both compute the Collatz sequence.