Rewriting Techniques for Correctness of Program Transformations @ ISR 2015

Course at the International School on Rewriting ISR 2015 Rewriting Techniques for Correctness of Program Transformations August 12-14, Leipzig, Germany
Summary Lecturers Lecture Notes Exercises Slides Proofs Links	Summary The course gives an introduction to program transformations, their correctness and rewriting techniques to reason about the correctness. The course focuses on small-step operational semantics of functional programming languages which can be seen as higher-order rewriting with a fixed strategy. On top of the operational semantics contextual equivalence is used as the main notion of program semantics and correctness of program transformations. The course also treats non-deterministic and concurrent extensions of functional programming languages and adaptions of the contextual semantics. Lecturers The lectures will be given by David Sabel David Sabel received his diploma in computer science from Goethe-University Frankfurt in 2003, his Dr. in 2008 from Goethe-University Frankfurt and in 2013 his habilitation in computer science. His research focuses on programming languages semantics, and he gave several lectures on functional and concurrent programming and the semantics of programming languages. He currently holds a post-doc position at Goethe-University Frankfurt. and Manfred Schmidt-Schauß Manfred Schmidt-Schauß received his diploma in Mathematics from the University of Mainz in 1979 and his Dr. from the University of Kaiserslautern in 1988 in Computer Science. Since 1992 he is full professor for Artificial Intelligence and Software Technology at the Department of Computer Science of the Goethe-University Frankfurt. Main research areas and publications are in automated deduction, unification, knowledge representation, functional programming, contextual semantics of functional programs and methods to show correctness, and algorithms on grammar-compressed compressed terms. . Lecture Notes The lecture notes are available as PDF and printer-friendly PDF. Exercises The exercises are included in the lecture notes. The solutions to the exercises are available as PDF. Presentation Slides The presentation slides used in the lectures will be available here: Part 1 (Wednesday): Screen (PDF)Printer-friendly (PDF) Part 2 (Thursday): Screen (PDF)Printer-friendly (PDF) Part 3 (Friday): Screen (PDF)Printer-friendly (PDF) Outputs of AProVE and CeTA In the calculus LNAME Transformation (case-app) Forking and commuting diagrams as TRS: case-app.trs Innermost-Termination-Proof: case-app.trs.proof.html CeTA-Output: case-app.trs.ceta.result In the calculus LR Transformation (llet) Forking diagrams as TRS (with free variables in right hand sides): llet_fork.trs Innermost-Termination-Proof: llet_fork.trs.proof.html CeTA-Output: llet_fork.trs.ceta.result Commuting diagrams as TRS (with free variables in right hand sides): llet_comm.trs Innermost-Termination-Proof: llet_comm.trs.proof.html CeTA-Output: llet_comm.trs.ceta.result Transformation (cp) Forking diagrams as TRS (with free variables in right hand sides): cp_fork.trs Innermost-Termination-Proof: cp_fork.trs.proof.html CeTA-Output: cp_fork.trs.ceta.result Commuting diagrams as TRS (with free variables in right hand sides): cp_comm.trs Innermost-Termination-Proof: cp_comm.trs.proof.html CeTA-Output: cp_comm.trs.ceta.result Links International School on Rewriting (ISR 2015) Termination-Prover AProVE: Website, Online Webinterface Certifier CeTA: Website DFG project: Automatic correctness proofs of program transformations
(c) 2015 KIST, Impressum, Last modified: $Author: sabel $, $Date: 2015/08/14 07:13:40 $