LFU:online

Students are able to formally specify the semantics of a simple functional or imperative programming language and instantiate and use verification tools such as the Hoare calculus or abstract interpretation for it. They can explain what the correctness of a compiler means formally.

Furthermore, they have acquired basic knowledge of the interactive theorem prover Isabelle/HOL and are able to formalise simple mathematical proofs by themselves.

Different kinds of formal semantics for programming languages: big-step, small-step, denotational; simple type systems; simple methods for program analysis and modification (initialisation analysis, constant folding, liveness); weakest precondition reasoning and the Hoare calculus; partial and total correctness; abstract interpretation

Basic Isabelle/HOL skills: non-recursive definitions, recursive definitions, inductive predicates; the structured proof language Isar; various schemes for induction and case distinction

Mostly slides, occasional blackboard use. Freely available textbook. Homework and in-class exercises.

written

Concrete Semantics, T. Nipkow und G. Klein, 2024.

ISBN: 978-3-319-10541-3

Freely available under: http://www.concrete-semantics.org

Good fundamental knowledge of logic (propositional logic, predicate logic), functional programming, and discrete mathematics as taught in e.g. the lectures "Introduction to Theoretical Computer Science", "Introduction to Functional Programming", "Discrete Structures", and "Logic".

Knowledge of Isabelle/HOL or program verification (e.g. Hoare calculus) is not necessary, but may be useful.

Allocation of places in courses with a limited number of participants (PS, SE, VU, PJ)

In courses with a limited number of participants, course places are allocated as follows:

1. Students for whom the study duration would be extended due to the postponement are to be given priority.

2. If the criteria in no. 1 do not suffice, first, students for whom this course is part of a compulsory module are to be given priority, and second, students for whom this course is part of an elective module.

3. If the criteria in no. 1 and 2 do not suffice, the available places are drawn by random.

Curriculum MA Computer Science 2021W