Automating the Diagram Method to Prove Correctness of Program Transformations

David Sabel
(Goethe-University Frankfurt am Main)

We report on the automation of a technique to prove the correctness of program transformations in higher-order program calculi which may permit recursive let-bindings as they occur in functional programming languages. A program transformation is correct if it preserves the observational semantics of programs. In our LRSX Tool 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.

In Joachim Niehren and David Sabel: Proceedings Fifth International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2018), Oxford, England, 8th July 2018, Electronic Proceedings in Theoretical Computer Science 289, pp. 17–33.
Published: 22nd February 2019.

ArXived at: http://dx.doi.org/10.4204/EPTCS.289.2 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org