Automating the diagram method to prove correctness of program transformations

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 functiona
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.
…show moreshow less

Download full text files

Export metadata

  • Export Bibtex
  • Export RIS

Additional Services

    Share in Twitter Search Google Scholar
Metadaten
Author:David Sabel
URN:urn:nbn:de:hebis:30:3-513488
URL:https://easychair.org/publications/preprint/5xRB
DOI:http://dx.doi.org/10.29007/vrxp
Parent Title (German):EasyChair Preprint ; No. 415
Publisher:EasyChair
Document Type:Working Paper
Language:English
Year of Completion:2018
Date of first Publication:2018/08/09
Publishing Institution:Universitätsbibliothek Johann Christian Senckenberg
Release Date:2019/10/01
Tag:contextual equivalence; correctness; deduction; observational equivalence; program transformation; semantics; verification
Pagenumber:16
HeBIS PPN:455221960
Institutes:Informatik
Dewey Decimal Classification:004 Datenverarbeitung; Informatik
Sammlungen:Universitätspublikationen
Licence (German):License LogoCreative Commons - Namensnennung 4.0

$Rev: 11761 $