Formal Methods and Functional Programming

Bachelor Course 252-0058-00L, Spring Semester 2011

• 19/07 You can inspect your final exams on Wed, 03.8.2011, 13:30 - 14:30 and on Thu, 04.8.2011, 10:30 - 11:30 in CAB F 37. The course assistants will be present in case you have any questions.
• The results of the lecturer evaluation are available here for the first half of the course, and here for the second.

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

Classes: Tue 10-12 in HG F 3, Thu 10-12 in HG F 7

Exams:

• Midterm exam: April 6th, 15:30 - 17:30. Surnames A - L in Room HG F1, surnames M - Z in Room HG E7.
  
• Final exam: June 7th, 10:00 - 12:00. Surnames A - K in room HG F3, surnames L - Z in room HG F7.

Exercises (updated for second half of the course):

• Tue 16-18
  
  • IFW-B42 (Stefan Heule, german website)
  • IFW-C42 (Alex Summers, english)
    
• Wed 15-17
  • IFW-A34 (Pietro Ferrara, english)
  • IFW-A32.1 (Alex Summers, english)
  • IFW-C33 (Yannis Kassios, english)

Please attend the same session as in the first half of the course (the rooms and times are unchanged). If you want to switch session/group (for language reasons), please email Alex Summers

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 box outside room RZ F1. Solutions must be received by 9:15 on the Monday after the exercise is
published, in order to receive feedback.

Credits: 7

Homework is optional, but highly recommended. There will be a midterm and an end-of-semester final exam. The grade in the course will be determined by averaging the points from both exams.

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 modeling 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 analyze 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 modeled 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.

Literature for the first part:

• O'Sullivan, Stuart, Goerzen. Real World Haskell, O'Reilly, 2008 (full version online)
  
• Graham Hutton. Programming in Haskell. Cambridge University Press. 2007
  
• Simon Thompson. Haskell: The Craft of Functional Programming. Addison-Wesley, 1996

Literature for the second part:

• Hanne Riis Nielson and Flemming Nielson. Semantics with Applications: A Formal Introduction, John Wiley & Sons, 1992 (full version online)
  
• Christel Baier and Joost-Pieter Katoen. Principles of Model Checking. The MIT Press. 2008

Additional literature for interested students:

• Chris Okasaki. Purely Functional Data Structures. Cambridge University Press, 1998. (partially online)
  
• Harold Abelson and Gerald Jay Sussman with Julie Sussman. Structure and Interpretation of Computer Programs. MIT Press, 1996. (full version online)

Course Material: here