Stefan Ciobaca, Dorel Lucanu, Vlad Rusu, Grigore Rosu

Two programs or fragments of program are mutually equivalent iff either theyboth diverge or they end up in similar states.Mutual equivalence is desirable in many contexts, ranging from capturingprogram equivalence or correctness of program transformations withinthe same language, to capturing correctness of compilersfrom one language to another.This paper introduces a language-independent proof system for mutualequivalence.The proof system is parametric in the operational semantics of the twolanguages and in a state similarity relation.

Full Document (PDF)

Bibtex

@TechReport{lipsmpe,
    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",
    institution = "``Al.I.Cuza'' University of Ia{c s}i, Faculty of Computer Science",
    year = "2013",
    number = "TR 13-03",
    url = "https://publications.info.uaic.ro/technical-reports/archive/tr13-03-2013-a-language-independent-proof-system-for-mutual-program-equivalence/"
}