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.
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.
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.