# Automating the Diagram Method to Prove Correctness of Program Transformations

## TL;DR

This paper presents an automated tool that uses the diagram method, combined with unification, matching, and induction, to verify the correctness of program transformations in higher-order functional languages.

## Contribution

It automates the diagram method for correctness proofs, integrating unification, matching, alpha-renaming, and termination analysis in a single tool.

## Key findings

- Successfully automates correctness proofs for program transformations.
- Demonstrates the tool's effectiveness through experiments.
- Integrates multiple techniques into a unified verification framework.

## Abstract

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.