A Language-Independent Proof System for Full Program Equivalence

From FSL
Revision as of 18:45, 1 February 2016 by Grosu (Talk | contribs)

Jump to: navigation, search

J.FOAC

ICFEM'14

A Language-Independent Proof System for Mutual Program Equivalence
Stefan Ciobaca and Dorel Lucanu and Vlad Rusu and Grigore Rosu
ICFEM'14, LNCS 8829, pp 75-90. 2014
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.
PDF, Slides(PDF), Matching Logic, DOI, ICFEM'14, BIB


Personal tools
Namespaces

Variants
Actions
Navigation