Formal Methods and Functional Programming

Overview

Lecturers:
Dr. Andreas Lochbihler and Prof. Dr. Peter Müller

Classes:
Tuesday 10-12 HG E 5 and Thursday 10-12 HG E 5

Credits: 7 ECTS (4V + 2U)

Homework:
is optional, but highly recommended. There will be a session examination.

Announcements

• (17/07) Some typos were spotted in the solution of exercise sheet 10, question 3 (specifically, the case of the proof for the assignment rule). A typo was also fixed in Sheet 12 Assignment 4 (which referred to itself, instead of Assignment 3 in its proof). These have now been fixed in the online versions.
  
• (24/06) The questions and answers session will be held on Wednesday, August 13th, starting at 9.00, in CAB G61. We will first cover the FP part, then the FM part. Note that once no more questions remain, we will end the session! It will at most last until 12.00.

Exercise Classes (second part, please note changes):

• Tuesday 13-15 *
  ETZ )
  NO ) *
  NO ) *

* Any students who are able to move from a Tuesday class to a Wednesday class, please do so. Students who previously attended the class in CAB G 57, please choose to either attend the class in ETZ G 91 or one of the classes on Wednesday. Please do not attend the NO classes, which are full. Due to timetabling constraints, we are not able to have an extra class during the second half of the course.

• Wednesday 15-17
  IFW )
  IFW )

Solutions can be submitted in two ways: you can either send them by email to the assistant assigned to you or submit them on paper in the appropriate cardboard box opposite room CAB F 51.2 Solutions must be received by 11:00am on the Monday after the exercise is published, in order to receive feedback.

Requirements: none

Language: English

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.