Course at the International School on Rewriting ISR 2015

Rewriting Techniques for
Correctness of Program Transformations

August 12-14, Leipzig, Germany

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.
The lectures will be given by David Sabel and Manfred Schmidt-Schauß.
Lecture Notes
The lecture notes are available as PDF and printer-friendly PDF.
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:
Outputs of AProVE and CeTA

In the calculus LNAME

Transformation (case-app)

In the calculus LR

Transformation (llet) Transformation (cp)
(c) 2015 KIST, Impressum, Last modified: $Author: sabel $, $Date: 2015/08/14 07:13:40 $