Skip to Main content Skip to Navigation
Conference papers

A Language-Independent Proof System for Mutual Program Equivalence

Ştefan Ciobâcǎ 1 Dorel Lucanu 2 Vlad Rusu 3 Grigore Rosu 4 
3 DREAMPAL - Dynamic Reconfigurable Massively Parallel Architectures and Languages
Université de Lille, Sciences et Technologies, Inria Lille - Nord Europe, CNRS - Centre National de la Recherche Scientifique
Abstract : 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.
Document type :
Conference papers
Complete list of metadata

Cited literature [17 references]  Display  Hide  Download
Contributor : Mister Dart Connect in order to contact the contributor
Submitted on : Tuesday, July 22, 2014 - 1:37:44 PM
Last modification on : Thursday, January 20, 2022 - 4:14:49 PM
Long-term archiving on: : Tuesday, November 25, 2014 - 11:05:14 AM


Files produced by the author(s)


  • HAL Id : hal-01030754, version 1



Ştefan Ciobâcǎ, Dorel Lucanu, Vlad Rusu, Grigore Rosu. A Language-Independent Proof System for Mutual Program Equivalence. ICFEM'14 - 16th International Conference on Formal Engineering Methods, Nov 2014, Luxembourg-Ville, Luxembourg. ⟨hal-01030754⟩



Record views


Files downloads