Difference between revisions of "A Language-Independent Proof System for Full Program Equivalence"
From FSL
| Line 1: | Line 1: | ||
| − | <pubbib id='ciobaca-lucanu-rusu-rosu-2013-icalp-submission' template='PubDefaultWithAbstractAndTitle' /> | + | == J.FOAC == |
| + | <pubbib id='ciobaca-lucanu-rusu-rosu-2016-foac' template='PubDefaultWithAbstractAndTitle'/> | ||
| + | == ICFEM'14 == | ||
| + | <pubbib id='ciobaca-lucanu-rusu-rosu-2014-icfem' template='PubDefaultWithAbstractAndTitle'/> | ||
| + | <private>== Submitted to ICALP'13 == | ||
| + | <pubbib id='ciobaca-lucanu-rusu-rosu-2013-icalp-submission' template='PubDefaultWithAbstractAndTitle'/></private> | ||
Revision as of 18:45, 1 February 2016
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.
