Praktische Semantik von Programmiersprachen (SoSe 2020)

For the course description, see here.

Dozenten Tadeusz Litak
Termine und Ort Tue 12:15-13:45; Wed 16:15-17:45
Subscription StudOn registration
Updates and uploads StudOn page
Umfang 4 SWS – 7,5 ECTS
Zielgruppe those mentioned by UnivIS, let me know if you’re not covered

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:

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).