This course aims to build a greater knowledge in several aspects of rewriting by practicing the theoretical content of the main lecture in many exercises.

This course deals with the formal modeling of concurrent systems such as parallel or multi-threaded programs, distributed hardware and software systems, mobile systems, and the like.

This course presents the major methods for defining the meaning of languages (operational semantics, denotational semantics, axiomatic semantics) and programs and discusses their relationship.


The course starts with a proof theoretic approach to propositional and predicate logic and their completeness, followed by basic recursion theory and it's formalization within formal arithmetic. From this point we can move from arithmetic to  Gödel’s Incompleteness Theorem  and Gentzen's proof of the consistency of arithmetic. At this point we will delve into basic type theory, Curry-Howard correspondence and it's connection to system T which provides an alternative consistency proof of arithmetic.  Both of this Highlight the existence of functions beyond arithmetic of which we provide a few examples . We then  discuss Second-order arithmetic, Strong type systems in correspondence with Second-order arithmetic (System F), and the relationship between subsystems of second-order arithmetic and mathematical analysis (Reverse Mathematics). 

This course explores advanced object oriented techniques using the Java language. The accent is on encapsulation, exemplified with algorithms and data structures, and on a frame of software tools used in real-world applications.

In dieser Lehrveranstaltung behandeln wir (als Fortsetzung der LVA "Programmierung 1") objektorientierte Programmierung in C++.

In this seminar, we explore current research and systems for specifying and verifying computer programs (specification languages, program verifiers, model checkers, ...).