Theoretische Informatik

Praktische Semantik von Programmiersprachen

Dozenten Tadeusz Litak (in SS 2017 with Christoph Rauch; in SS 2013 shared with Daniel Gorín)
Umfang 4 SWS – 7,5 ECTS
Zielgruppe WPF INF-BA-V-THI ab 4. Semester
WPF INF-MA ab 1. Semester

Editions so far


Coquette Coq session screenshot

We will study the foundations of the imperative and functional languages, including semantics and type systems. But there is a twist: we will be doing theory in a very practical and hands-on way: we will be proving programming all the results from first-principles.

Our weapon of choice: the Coq proof assistant.

Our motto: proofs are programs and programs are proofs!


  • I already know my Java/C++/..., why should I care about all this semantics stuff?
    Domain specific languages are becoming more and more frequent; just think of game scripting, shaders, complex build systems, mark-up and templating languages, etc. Sooner or later you will face the need to come up with your own DSL and you will really appreciate to have all the theory straight! (see also Greenspun's tenth law).

  • Is this Coq proof assistant thing just an academic toy?
    Not at all! Coq is an industrial-strength proof assistant used, e.g., to verify Coq is at the same time also a compiler for a total functional programming language, so it is quite fun to work with it.

  • Ok, I'm almost convinced! Where can I read more about the content of the course?
    We will follow the book Sofware Foundations, see below. The present plan is roughly to follow the blue arrow path on this diagram. This book has been used successfully as the basis for similar courses in universities throughout the world, the model one given at Penn in the US. We also had a very good experience teaching it here last year.


  • Software Foundations online book by Benjamin C. Pierce and coauthors will be our main resource.
  • Supplementary reading on the theory of programming: Types and Programming Languages, Benjamin C. Pierce, The MIT Press.
  • Supplementary reading on Coq: Interactive Theorem Proving and Program Development Coq'Art: The Calculus of Inductive Constructions. Series: Texts in Theoretical Computer Science. An EATCS Series Bertot, Yves, Casteran, Pierre

The lecture will be recorded again in 2019 and the old recording of the obsolete first edition is going to be deleted. The new recording will be only available to the participants of the course from the university network, protected by a password.