Programming languages are everywhere in computer science, but how can one formally describe, what a program written in a specific programming language actually means? This course answers this question by presenting the basics of programming language theory. First, we will see how one can formally give semantics for programming languages and then, second, we will see how one can use these formal semantics to reason about programs and verify their correctness. This course will combine lectures with hands-on sessions where students can reason about programs inside the Coq proof assistant.
Target group: Students interested in formal verification of programs and proof assistants.
Prerequisites: Experience with logical reasoning (e.g., proof by induction)
Experience with proof assistants (in particular, the Coq proof assistant) of advantage
Evaluation: None
Teaching format: None
ECTS: 3 Year: 2024
Track segment(s):
Elective
Teacher(s):
Michael Sammler
Teaching assistant(s):
- Teacher: Michael Sammler