Praktische Semantik von Programmiersprachen

Content

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!

FAQ

• 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
  • correctness of a C compiler up to the machine-instruction level.
  • implementation of Java Card technology with highest posssible industrial certification
  • relational specifications for low-level programs and the output of certified compilers at Microsoft Research Cambridge
  • … and much more, see here!

  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.

Material

• 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