Semantics of Programming Languages
Prof. Tobias Nipkow, Wintersemester 2010/11
- Module: IN2055
- Lectures: Monday 8:30 - 10:00 in MI 00.07.011, Friday 10:15 - 11:45 in MI 00.07.011
- Exercises: Monday 10:15 - 11:45 in MI 01.11.018, Friday 12:00 - 13:30 in MI 00.09.055
- Consulting hours: Tuesday 14:00 - 15:00 in MI 02.09.012, Wednesday 14:00 - 15:00 in MI 02.09.012, by Armin Heller (ArminHeller
t-online.de) - Tutors: Sascha Böhme Alex Krauss
On this page: News Lecture and Exercises Homework Aims Important notice Literature Student feedback Evaluation talk
News
- Oral exams on 7/2/2011, starting at 8:30. Please enter your name into one slot on the list in the glass case close to Prof. Nipkow's office (from 17/1/2011).
- We now provide a repository for this site, to make synchronization easier. See below.
- The homework rules have been clarified and strengthened. See here.
Mercurial version control system, you can synchronize these files automatically:
[ view changelog ]
hg clone https://www4.in.tum.de/~krauss/hg/semantics_website[ view changelog ]
Homework
Homework is the heart and soul of this course.
-
Solved homeworks should be submitted via e-mail to one of the tutors:
boehmes
The latest submission date is given on each exercise sheet. Late submissions will not be graded! If you have a good excuse (such as being very sick), you should contact the tutors before the deadline.in.tum.de
or
kraussin.tum.de
- Each homework will get two, one or zero points, depending on the solution being correct, improvable or incorrect, respectively.
- Discussing ideas and problems with others is encouraged. When working on homework problems, however, you need to solve and write up the actual solutions alone. If you misuse the opportunity for collaboration, we will consider this as cheating. Cheating on one homework will result in zero points for that homework. If you cheat repeatedly, you will fail the course immediately. This applies for both parties, that is, the one who cheated and the one who provided his/her solution.
- Important: homeworks are graded and have a 40% share on the final grade.
Aims
The aim of this course will be to introduce the structural, operational approach to programming language semantics. It will show how this formalism is used to specify the meaning of some simple programming language constructs and to reason formally about semantic properties of programs and of tools like program analyzers and compilers. For the reasoning part the theorem prover Isabelle will be used.
At the end of the course students should- be familiar with rule-based presentations of the operational semantics of some simple imperative program constructs,
- be able to prove properties of an operational semantics using various forms of induction and
- be able to write precise formal proofs with the theorem prover Isabelle.
Important notice
- You must be familiar with the basics of some functional programming language like Haskell, Objective Caml, Standard ML or F# (as taught, for example, in Introduction to Informatics 2). For motivated students who do not have the necessary background yet: There are many introductions to functional programming available online, for example the first 6 chapters of Introduction to Objective Caml.
- You must haven taken some basic course in discrete mathematics where you learned about sets, relations and proof principles like induction (as taught, for example, in Discrete Structures).
- You need not be familiar with formal logic but you must be motivated to learn how to write precise and detailed mathematical proofs that are checked for correctness by a machine, the theorem prover Isabelle.
- At the end of the course there will be a written or oral examination, depending on the number of students. Throughout the course there will be homework assignments. They will involve the use of Isabelle and will be graded. The final grade will combine the grades from the examination (60%) and the homework (40%).
- All lectures are in English.
Literature
- Hanne Riis Nielson, Flemming Nielson: Semantics with Applications: A Formal Introduction.
- Glynn Winskel: The Formal Semantics of Programming Languages. MIT Press.
- Tobias Nipkow, Lawrence Paulson, Markus Wenzel: Isabelle/HOL. A Proof Assistant for Higher-Order Logic.
Anonymous student feedback
-
Dear Prof. Nipkow,
In my opinion the course is among the most interesting ones I've heard so far. Generally you present the topic very well, your explanations are easy enough to follow (of cause one has to think and stay tuned) and I like your style of presentation. Live-demos are good.
Learning to use a theorem prover and using it in the tutorials works well and is exciting.
The slides work very nicely in class, however as a reference for later they are a bit sparse with information. Here a more thorough script would the optimal (although I know this is quite a lot to ask). Recording the lecture could be a very nice bonus. At the moment I find it very hard to catch up on a missed lecture.
Thanks for offering this great course!
Best regards, a happy student -
Die Vorlesung deckt ein vergleichsweise breites Spektrum der theoretischen Informatik ab und zeigt gleichzeitig Tiefe durch eine komplette Implementierung und Beweisführung zu allen Aspekten, ohne zu überfordern!
Die Übungen und Hausaufgaben vertiefen dies und wecken Spaß am Beweisen. Sie sind aber auch nicht zu einfach, weshalb sie - meiner Meinung nach zu recht - in die Prüfungsleistung eingehen. - Interaktive Gestaltung (durch gemeinsames Erarbeiten an der Tafel etc.) trägt sehr zum besseren Verständnis bei.
-
In general really good but very demanding course.
But in many situations Prof. Nipkow (and also teaching assistants) have to be aware, that the proof/logic/concept is not as trivial for the students as it is for them.
Getting introduced to a topic within 15 minutes of the lecture in a very high speed is ok, getting presented proofs concerning the concept directly after the introduction, is okay too. But understanding the proof as fast as it is presented without having fully internalized the concept, is often impossible.
Prof. Nipkow should take into account, that the students do not work and think in this domain for years.
Nevertheless, very good and interesting course. - Good course. Homework sometimes (due to missing experience with Isabelle and many "confusing" mistakes) too time-consuming.
- I think this course has a very good structure, the lectures, exercises, homeworks match perfect to each other. The people are really nice and really try to get students to understand something. I will certainly recommend this course to other students. The thing is that when I asked my friends why they didn't take this course, they said "are you familiar with all that stuff in the course prerequisites?". Maybe it would be better to make "important notice" more simple since the material is very good arranged and if somebody knows nothing at the beginning, he can gradually get to some extent familiar with that (I'm saying that from my personal experience :-)). On the other hand with the current important notice one can get a small group of for the most part motivated students. So it depends on the goals. Anyway it is really difficult to find something bad about this course :-)