Download PDFOpen PDF in browser

Automating the Diagram Method to Prove Correctness of Program Transformations

EasyChair Preprint no. 415

15 pagesPublished: August 9, 2018

Abstract

Our recently developed LRSX Tool implements a technique to automatically prove the correctness of program transformations in higher-order program calculi which may permit recursive let-bindings. The focused notion of correctness for program transformations is invariance with respect to the observational semantics of programs. The so-called diagram method is automated by combining unification, matching, and reasoning on alpha-renamings on the higher-order meta-language, and automating induction proofs via an encoding into termination problems of term rewrite systems. We explain the techniques, we illustrate the usage of the tool, and we report on experiments.

Keyphrases: contextual equivalence, correctness, deduction, observational equivalence, program transformation, semantics, verification

BibTeX entry
BibTeX does not have the right entry for preprints. This is a hack for producing the correct reference:
@Booklet{EasyChair:415,
  author = {David Sabel},
  title = {Automating the Diagram Method to Prove Correctness of Program Transformations},
  howpublished = {EasyChair Preprint no. 415},
  doi = {10.29007/vrxp},
  year = {EasyChair, 2018}}
Download PDFOpen PDF in browser