TY  - UNPD
A1  - Sabel, David
T1  - Automating the diagram method to prove correctness of program transformations
T2  - EasyChair Preprint ; No. 415
N2  - 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 as they occur in functional programming languages. A program transformation is correct if it preserves the observational semantics of programs- In our tool the so-called diagram method is automated by combining unification, matching, and reasoning on alpha-renamings on the higher-order metalanguage, 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.
KW  - contextual equivalence
KW  - correctness
KW  - deduction
KW  - observational equivalence
KW  - program transformation
KW  - semantics
KW  - verification
Y1  - 2018
UR  - http://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/51348
UR  - https://nbn-resolving.org/urn:nbn:de:hebis:30:3-513488
UR  - https://easychair.org/publications/preprint/5xRB
PB  - EasyChair
ER  -