Formal Methods and Functional Programming
Spring Semester 2019, Bachelor course (252-0058-00)
Announcements
- The final exam on Saturday, August 17 will take place in two rooms. Please be ready in front of your assigned room shortly before 9:00 am.
Students with last names A-Ma go to HIL F 41.
Students with last names Me-Z go to HIL F 61. - The protected pagefirstlock and the protected pagesecondlock midterm quiz are available on the course webpage.
- Q&A session: Tuesday, July 30, at 10:00 in CAB G 52
- The protected pageresultslock of second midterm quiz are online. You can review your quiz on Thursday, June 6, between 8:30am and 10:00am in CAB J 71.6. There will be a second review toghether with the final exam after the examination session.
- The second midtern quiz on May 9 will take place in four different rooms. Please be ready in front of your assigned room by 10:05 am.
Students with last names A - J go to HG G 5.
Students with last names K - Lo go to CHN E 46.
Students with last names Lu - M go to CHN F 46.
Students with last names N - Z go to HG E 3. - All competition results, discussions, and the art gallery have been uploaded.
- The last competition task is online. Please note that the deadline is on Tuesday, 2nd April, 23:59 CEST.
- The game week has started! Please submit your strategy until the extended deadline on Tuesday, 2nd April, 23:59 CEST, and win a special prize.
- The results, discussion, and a pair of follow-up exercises for the third and fourth competition task are online.
- The protected pageresults of Quiz 1lock are online. You can review your quiz on Thursday, March 21, between 8:30 and 10:00 in CNB F 110. There will be a second review together with the final exam after the examination session.
- The second midterm quiz will take place on May 9 during the lecture.
- The results and discussion of the second competition task are online.
- The results and discussion of the first competition task are online.
- Please register for the exercise classes.
Overview
Lecturers: Prof. Dr. David Basin, Prof. Dr. Peter Müller, and Dr. Dmitriy Traytel
Classes: Tuesday 10–12 and Thursday 10–12, HG G 5
Credits: 7 ECTS (4V + 2U)
Requirements: none
Language: English
Exercise classes:
- Tuesday 13–15
CAB G 52, Martin Clochard (, English)
CHN D 46, Mauro Bringolf (, German)
NO D 11, Felix Wolf (, German)
NO E 11, Gaurav Parthasarathy (, English)
- Wednesday 15–17
CAB G 59, Jan Veen (, German)
CHN D 42, Sandra Dünki (, German)
IFW C 33, Arshavir Ter-Gabrielyan (, English)
- Feedback only
Jérôme Dohrau (, English/German)
For questions/issues concerned with the first half (Functional Programming), please e-mail Joshua Schneider (); for the second half (Formal Methods), please e-mail Jérôme Dohrau ().
Homeworks, Exams, and Quizzes
There will be a 180 minutes written examination. This examination covers both halves of the course. Note that the examination is only offered in the session after the course unit.
This year, there will also be two graded midterm quizzes. Each quiz will be 30 minutes and each may improve the final grade. The first one took place on March 12 at 10:15 (protected pageresultslock). The second quiz will take place on May 9 during the lecture.
Homework is optional, but highly recommended.
A functional programming competition runs during the first seven weeks of the course and is reported on here.
Course Material
The lecture slides, exercises, and other resources are available in our protected pagesecured arealock. To access the secured area, you must first login with your nethz account.
Description
In this course, participants will learn about new ways of specifying, reasoning about, and developing programs and computer systems. Our objective is to help students raise their level of abstraction in modelling and implementing systems.
The first part of the course will focus on designing and reasoning about functional programs. Functional programs are mathematical expressions that are evaluated and reasoned about much like ordinary mathematical functions. As a result, these expressions are simple to analyse and compose to implement large-scale programs. We will cover the mathematical foundations of functional programming, the lambda calculus, as well as higher-order programming, typing, and proofs of correctness.
The second part of the course will focus on deductive and algorithmic validation of programs modelled as transition systems. As an example of deductive verification, students will learn how to formalize the semantics of imperative programming languages and how to use a formal semantics to prove properties of languages and programs. As an example of algorithmic validation, the course will introduce model checking and apply it to programs and program designs.
Resources
Literature for the first part
- Miran Lipovača. external pageLearn you a Haskell for great good!call_made no starch press, 2011 (external pagefull version onlinecall_made)
- Simon Thompson. external pageHaskell: the Craft of Functional Programmingcall_made, Addison Wesley, 2011
- O'Sullivan, Stuart, Goerzen. external pageReal World Haskellcall_made, O'Reilly, 2008 (external pagefull version onlinecall_made)
- Graham Hutton. external pageProgramming in Haskellcall_made. Second edition, Cambridge University Press, 2016
- Mordechai Ben-Ari. external pageMathematical Logic for Computer Sciencecall_made. Springer, 2012
Haskell links
The external pageZurich Haskell user groupcall_made maintains a collection of external pageHaskell linkscall_made useful for both Haskell beginners and experts.
Proof checker
The proof checker CYP for induction proofs is external pageavailable on GitHubcall_made.
Literature for the second part
- Hanne Riis Nielson and Flemming Nielson. external pageSemantics with Applications: A Formal Introductioncall_made, John Wiley & Sons, 1992
- Christel Baier and Joost-Pieter Katoen. external pagePrinciples of Model Checkingcall_made. The MIT Press, 2008
Additional literature for interested students
- Chris Okasaki. Purely Functional Data Structures. Cambridge University Press, 1998.
- Harold Abelson and Gerald Jay Sussman with Julie Sussman. Structure and Interpretation of Computer Programs. MIT Press, 1996. (external pagefull version onlinecall_made)