Formal Methods and Functional Programming
Spring Semester 2022, Bachelor course (252-0058-00)
Overview
Lecturers: Prof. Dr. Peter Müller and Dr. Christoph Sprenger
Classes: Tuesdays 10-12 and Thursdays 10-12
Credits: 7 ECTS (4V + 2U)
Language (lecture): English
Exercise classes: Tuesdays 14-16, Wednesdays 10-12 or Wednesdays 16-18
For questions/issues concerned with the first half (Functional Programming), please contact ; for the second half (Formal Methods), please contact .
Student forum : Please use the Moodle forum as main plaftorm for asking questions!
General Information
Course material and announcements:
All the course material will be uploaded on Moodle. Announcements will also be made via Moodle.
For the first part of the course, we will also use CodeExpert for programming exercises.
Lectures:
Lectures will be live streamed and recorded.
You will find the live streaming here: https://video.ethz.ch/live/lectures/zentrum/hg/hg-e-7.html
Recordings will be uploaded (at the latest the day after the lecture) here: https://video.ethz.ch/lectures/d-infk/2022/spring/252-0058-00L.html
Exercise Sessions:
Please enroll in an exercise group via CodeExpert.
It is important you attend the same exercise group you are enrolled in Code Expert!
Tuesdays 14-16:
- CAB G 57 [German]
- CAB G 52 [English]
- NO D 11 [English]
- ZOOM [English]: zoom link on Moodle
Wednesdays 10-12:
- CAB G 52 [English]
- LFW C11 [German]
- LEE C114 [German]
- ETZ F91 [German]
Wednesdays 16-18:
- CAB G 52 [English]
- CHN D 42 [English]
- CHN F 46 [English]
- HG G 26.5 [English]
- ZOOM [English]: zoom link on Moodle
Exam and Quizzes:
There will be a 120 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.
There will also be two graded midterm quizzes. Each quiz will be 30 minutes and each may improve the final grade.
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)