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 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.
Volltext Dateien herunterladen
Weitere Dienste
| Verfasserangaben: | David SabelORCiDGND |
|---|---|
| URN: | urn:nbn:de:hebis:30:3-513488 |
| URL: | https://easychair.org/publications/preprint/5xRB |
| DOI: | https://doi.org/10.29007/vrxp |
| Titel des übergeordneten Werkes (Deutsch): | EasyChair Preprint ; No. 415 |
| Verlag: | EasyChair |
| Dokumentart: | Arbeitspapier |
| Sprache: | Englisch |
| Jahr der Fertigstellung: | 2018 |
| Datum der Erstveröffentlichung: | 09.08.2018 |
| Veröffentlichende Institution: | Universitätsbibliothek Johann Christian Senckenberg |
| Datum der Freischaltung: | 01.10.2019 |
| Freies Schlagwort / Tag: | contextual equivalence; correctness; deduction; observational equivalence; program transformation; semantics; verification |
| Seitenzahl: | 16 |
| HeBIS-PPN: | 455221960 |
| Institute: | Informatik und Mathematik / Informatik |
| DDC-Klassifikation: | 0 Informatik, Informationswissenschaft, allgemeine Werke / 00 Informatik, Wissen, Systeme / 004 Datenverarbeitung; Informatik |
| Sammlungen: | Universitätspublikationen |
| Lizenz (Deutsch): |  Creative Commons - Namensnennung 4.0 |
