Formal Methods and Functional Programming
Spring Semester 2015, Bachelor Course (252-0058-00)
Overview
Lecturers: Prof. Dr. David Basin 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)
Requirements: none
Language: English
Exercise Classes
- Tuesday 13-15
1. (German)
2. ETZ H 91 Malte Schwerhoff (German)
3. NO D 11 Alex Summers (English)
4. NO E 11 Milos Novacek (English) - Wednesday 15-17
5. NOE 11 Malte Schwerhoff (German)
Course Material
The lecture notes, exercises, slides, and other resources are available in our protected pagesecured arealock.
Homework is optional, but highly recommended. There will be a session examination.
Submission instructions
Haskell programs must be submitted electronically via external pagecodeboard.iocall_made. The relevant assignments mention the URL of the corresponding project on codeboard.io. Please follow the submission guidelines outlined in the first exercise sheet to ensure that we are able to identify your submission and provide feedback.
Other assignments can be submitted in two ways: you can either send them by e-mail to your tutor or submit them on paper in the appropriate cardboard box outside room CAB F53.1. Solutions must be received by 11:00am on the Monday after the exercise is published, in order to receive feedback.
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 a 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. Cambridge University Press. 2007
Haskell links
The external pageZurich Haskell user groupcall_made maintains a collection of external pageHaskell linkscall_made useful for both Haskell beginners and experts.
Literature for the second part:
- Hanne Riis Nielson and Flemming Nielson. external pageSemantics with Applications: A Formal Introductioncall_made, John Wiley & Sons, 1992 (external pagefull version onlinecall_made)
- 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)