Formal Methods and Functional Programming

 Announcements

• Exam viewings:
  • Friday, 21. September, 10:00–11:30, CNB F110
  • Tuesday, 25. September, 10:00–11:30, CNB F110
    
• The final exam will take place on August 6th from 14:30 to 17:30 in HIL F 61 (last names starting with A-L) and HIL G 61 (last names starting with M-Z).
  
• We have uploaded the protected page exam from 2017.
• The results of the sixth competition task are finally online. Grab some popcorn and watch the Download games.
• The results of the fifth competition task are finally online.
• The results of the fourth competition task are finally online.
• There will be two possibilities for students to view their results of Quiz 1:
  • on Tuesday, 20.03.2018 from 15:30 to 17:00 (after the exercise classes) in CNB F 110, and
  • together with the viewing of the final exam after the semester.
• The protected page results of Quiz 1 are online.
  
• The results of the third competition task are online.
• You can take a look at protected page Quiz 1 from last year. Note that lists are not part of the material for this year's quiz.
  
• The results of the second competition task are finally online.
• The results of the first competition task have been summarized here.
• The Wednesday exercise class in English (“Applicative Functors”) has been moved to NO C 6 and starts at 16:00 sharp.
  
• Please register for the exercise classes: login with your ETH credentials, select a class, enter some text and click “submit”.
  

Overview

Lecturers: Prof. Dr. David Basin and Prof. Dr. Peter Müller

Classes: Tuesday 10–12, HG G 5 and Thursday 10–12, HG G 5

Credits: 7 ECTS (4V + 2U)

Requirements: none

Language: English

Exercise Classes

• Tuesday 13–15
  CAB G 52 (German)
  CHN D 46 (German)
  NO D 11 (English)
  NO E 11 (German)
  
• Wednesday 15–17
  CHN D 42 (German)
• Wednesday 16:00 sharp–18
  NO C 6 (English)

For questions/issues concerned with the first half (Functional Programming), please e-mail Dr. Dmitriy Traytel (); for the second half (Formal Methods), please e-mail Dr. Caterina Urban ().

Homeworks, Exams, and Quizzes

There will be a 180 minutes written examination on August 6th from 14:30 to 17:30 in HIL F 61 (last names starting with A-L) and HIL G 61 (last names starting with M-Z). 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 will count 10% of the total grade. The first one took place on March 13 at 10:10 in HG G 5 and HG E 3. The second quiz took place on May 15th in HG G 5 and CHN C 14.

Homework is optional, but highly recommended.

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

Course Material

The lecture notes, slides, and other resources are available in our protected page secured area. To access the secured area, you must first login with your nethz account at the top right corner of the page.

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.