Formal Methods and Functional Programming
Spring Semester 2024, Bachelor course (252-0058-00)
Overview
Lecturers: Prof. Dr. Peter Müller and Prof. Dr. David Basin
Classes: Tuesdays 10-12 and Thursdays 10-12
Credits: 7 ECTS (4V + 2U)
Language: English (lectures), English and German (exercises)
Exercise classes: Tuesdays 14-16, Wednesdays 8-10 or Wednesdays 16-18
For questions/issues concerned with the first half (Functional Programming), please contact François Hublet; for the second half (Formal Methods), please contact Nicolas Klose.
Announcements
- [2023/04/12] The FP team is handing the course over to the FM team. Have fun!
- [2023/04/12] The protected pagemaster solution of the first midtermlock has been released.
- [2023/03/04] Our first midterm will take place on March 14 at 10:00 in the usual lecture halls!
- [2023/02/14] You can now enroll in an exercise group using CodeExpert. Note that enrollment in CodeExpert is obligatory to attend the exercises.
- [2023/01/25] The course webpage for this year's FMFP is up and running!
Course material
Week 9
- [2024/04/21] protected pageSlides: Operational Semanticslock
- [2024/04/21] protected pageExercise sheet 9lock
- [2024/04/21] protected pageExercise session 9lock - protected pageSolutionlock
Week 8
- [2024/04/11] protected pageSlides: Introductionlock
- [2024/04/11] protected pageSlides: IMPlock
Week 7
- [2023/04/08] protected pageSlides: monads and conclusionlock
- [2023/04/08] protected pageExercise (theory) sheet 7lock
Week 6
- [2023/04/12] NEW! protected pageMidterm with solutionslock
- [2023/04/08] protected pageExercise session slideslock
- [2023/03/26] protected pageSlides: case studieslock
- [2023/03/26] protected pageSlides: efficiencylock
- [2023/03/26] protected pageExercise (theory) sheet 6lock - protected pageSolutionslock
Week 5
- [2023/03/26] protected pageExercise session slideslock
- [2023/03/18] protected pageSlides: lazy evaluationlock
- [2023/03/18] protected pageExercise (theory) sheet 5lock - protected pageSolutionslock
Week 4
- [2023/03/18] protected pageExercise session slideslock
- [2023/03/11] protected pageSlides: algebraic data typeslock
- [2023/03/11] protected pageSlides: moduleslock
- [2023/03/11] protected pageExercise (theory) sheet 4lock - protected pageSolutionslock
Week 3
- [2023/03/13] protected pageExercise session slideslock
- [2023/03/04] protected pageSlides: higher-order programming and typeslock
- [2023/03/04] protected pageExercise (theory) sheet 3lock - protected pageSolutionslock
Week 2
- [2023/03/05] protected pageExercise session slideslock
- [2023/02/27] protected pageSlides: listslock
- [2023/02/26] protected pageSlides: correctnesslock
- [2023/02/26] protected pageExercise (theory) sheet 2lock - protected pageSolutionslock
Week 1
- [2023/02/22] protected pageExercise session slideslock
- [2023/02/22] protected pageSlides: natural deductionlock
- [2023/02/19] protected pageSlides: introductionlock
- [2023/02/19] protected pageExercise (theory) sheet 1lock - protected pageSolutionslock
General Information
Course material:
All the course material will be uploaded on this website.
For the first part of the course, we will also use CodeExpert for programming exercises.
Lectures:
The lecture will be held in HG E 7. If not all students fit into the room, there will be a live streaming of the lecture in HG E 3. Please come to HG E 7 first.
Attendance is strongly recommended. No recordings will be provided.
Exercise Sessions:
The enrollment link for the Code Expert groups will be posted on this website very soon!
Exam 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.
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)