A Language-Independent Proof System for Mutual Program Equivalence

Ciobaca, StefanLucanu, DorelRusu, VladRosu, Grigore
ICFEM’14

Abstract. 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 different languages (an imperative one and a functional one), that both compute the Collatz sequence.