Praktische Semantik von Programmiersprachen (SoSe 2020)

For the course description, see here.

We’re scheduled for Mo 10:15 – 11:45, 01.255-128 and Do 18:15 – 19:45 00.131-128  Fortunately we do have a lot of online material, much more than an average lecture.

**The lecture was recorded in 2019 and I expect these recordings to be massively useful in 2020. Do expect, however, that there will be some changes now, as Coq and the lecture matter do evolve. ** Link to FSI 2019 videos together with the user name and the password is available via StudOn.

This means that I am likely to create new videos as well, presumably via StudOn interactive video feature.

More importantly, the whole lecture is based on electronic material. And the proof assistant is meant to act as your own personal tutor. Reach out and touch faith!

We have a lot of experience with using StudOn in previous years. This is of course only going to increase now.

I am going to do everything possible to avoid using Zoom. At the moment, our plan is to use MS Teams for meetings. Team’s name available via StudOn.

The tool we are going to use throughout the course is Coq. Ideally, go for the latest stable release (8.11 before the beginning of the semester) or the alpha/beta development version if you’re adventurous. You can install using either:

• the Coq webpage itself, but decide if you want it bundled with CoqIDE
• release pages of subsequent versions on GitHub (including newest dev alpha/beta version ”which might be risky”but also other recent versions). One advantage of native-code is that it is supposed to “run 4 to 10 times faster than bytecode”
• whichever port system you’re using on your OS
• your favourite package manager (opam, the OCaml package manager, recommended; another option is nix)

I will inform you later (e.g., in the first set of lecture slides and recordings) about the choice of possible IDEs.

Please register via the StudOn registration link. If you’re already a member, this is the regular StudOn page, which is going to be used to post proof scripts, homework and additional lecture materials as we progress. Hence, the role of this page ends (possible updates in future if lecture hours are going to change).