Links und Funktionen
Sprachumschaltung

Navigationspfad
Sie sind hier: Startseite / Lehre / SS 2018 / Oberseminar / David Sabel: Correctness of Program Transformations: Automating Diagram-Based Proofs


Inhaltsbereich

David Sabel: Correctness of Program Transformations: Automating Diagram-Based Proofs

Oberseminar, Dienstag, 29. Mai 2018, 11 Uhr s.t.
Wann 11:00 12:30 29.05.2018
von bis
Wo Raum L109, Oettingenstr. 67
Termin übernehmen vCal
iCal
Speaker: David Sabel

Titel: Correctness of Program Transformations: Automating Diagram-Based Proofs

Abstract:
In this talk I report on techniques 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. The focused notion of correctness for program transformations is invariance with respect to the observational semantics of programs. The so-called diagram method computes overlaps between evaluation steps and transformations, joins the overlaps to form reduction diagrams and then uses the diagrams in an inductive proof to show correctness of the transformation. In the talk I explain how algorithms for unification, matching, reasoning on alpha-renamings in a higher-order meta-language. and automating induction proofs via an encoding into termination problems of term rewrite systems can be used to automate the diagram method.

Bio: David Sabel earned a doctorate in computer science at Göthe-University Frankfurt am Main, Germany in 2008 and completed his habilitation in 2013 on  correctness of programs and programming languages. His research interests lie broadly in (functional) programming languages, unification, and rewriting. Since 2016, he leads the DFG project  "Observational Correctness of Programming Language Translations”.

Artikelaktionen


Funktionsleiste