Stefan Ciobaca, Dorel Lucanu, Vlad Rusu, Grigore Rosu

Two programs are mutually equivalent if they both diverge or they end up in similar states. Mutual equivalence is an adequate notion of equivalence for programs written in deterministic languages. It is useful in many contexts, such as capturing the correctness of program transformations within the same language, or capturing the correctness of compilers between two different languages. 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. The proof system is sound: if it terminates then it establishes the mutual equivalence of the programs given to it as input. We illustrate it on two programs in two different languages (an imperative one and a functional one), that both compute the Collatz sequence.

Full Document (PDF)

Bibtex

@TechReport{lipsmper,
    author = "c{S}tefan Ciob^acu{a} and Dorel Lucanu and Vlad Rusu and Grigore Ro{c s}u",
    title = "{A Language-Independent Proof System for Mutual Program Equivalence (revisited)",
    institution = "``Al.I.Cuza'' University of Ia{c s}i, Faculty of Computer Science",
    year = "2014",
    number = "TR 14-01",
    url = "https://publications.info.uaic.ro/technical-reports/archive/tr14-01-2014-a-language-independent-proof-system-for-mutual-program-equivalence-revisited/"
}