Formal Methods and Functional Programming

Announcements

• The final examination will take place on Monday, August 10, on the Hönggerberg campus. You are assigned to one of two rooms according to the first letter of your last name:
  • Students with last names A – K go to HIL F 41.
  • Students with last names L – Z and Ö go to HIL F 15.
    
• The slides and recording of the final Q&A session have been added to the protected page course material.
  
• If you want to solve your own problems with CYP on Code Expert, you can now edit the definitions file in the CYP demo. You may need to delete the project first if you have modified it. Some examples are external page here (cthy files).  

• The links to the video recordings of the second part of the lecture will be continuously added to the protected page course material.
• The results, discussion, and visualizations of the sixth round and the art gallery of the seventh round of the FP Competition are online.
• Two old FM midterm quizzes have been added to the protected page course material.
• The deadline for the last week of the FP Competition is on Tuesday, 31st March, 23:59 CEST.
• The results and discussion of the fifth round of the FP Competition are online.
  
• protected page Results of Quiz 1. Solutions: protected page variant A, protected page variant B.
  
• The second quiz is cancelled. We have added the first quiz to the protected page course material.
  
• The results and discussion of the fourth round of the FP Competition are online.
• All exercise lessons will be given remotely, too.
  
• The remaining lectures in the FP part will be prerecorded. We will organize remote Q&A sessions during the lecture hours, starting on March 12. Further details will be announced per mail. Please check your inbox frequently.
  
• The results and discussion of the third round of the FP Competition are online.
• The first quiz will take place on Tuesday, March 10. Please be ready in front of your assigned room by 10:05 am.
  
  • Students with last names A – E go to HG E 3.
  • Students with last names F – Q and Ö go to ETF E 1.
  • Students with last names R – Z and Ü go to ML D 28.
• The results and discussion of the second round of the FP Competition are online.
• We provide video recordings of the lecture starting from February 27.
  
• The results and discussion of the first round of the FP Competition are online.
  
• The FP Competition is online.
  
• Please enroll in the exercise class that you plan to attend.
• The first lecture is on Tuesday, February 18. There will be an exercise class in the first week.
  

Overview

Lecturers: Prof. Dr. Peter Müller and Dr. Dmitriy Traytel

Interactive Q&A: Tuesday 10–12 and Thursday 10–12

Credits: 7 ECTS (4V + 2U)

Requirements: none

Language (lecture): English

Exercise classes:

• Tuesday 13–15
   (FP), (FM) English
   (FP), (FM) German
  , German
   (FP),  (FM), English
  
• Wednesday 15–17
  , German
   (FP), (FM) German
   (FP), (FM), English
  , German
  
• Wednesday 16–18
   (FP), (FM) English

For questions/issues concerned with the first half (Functional Programming), please contact ; for the second half (Formal Methods), please contact .

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.

Homework is optional, but highly recommended.

A functional programming competition runs during the first seven weeks of the course and is reported on here.

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.