Functional Specification of Algorithms 2016

This course offers a perspective on algorithm specification, in terms of purely functional programming. An algorithm is an effective method expressed as a list of instructions describing a computation for calculating a result. Algorithms have to be written in human readable form, either using pseudocode (natural language looking like executable code), a high level specification language like Dijkstra's Guarded Command Language, or an executable formal specification formalism such as Z.

The course will develop a purely functional perspective on algorithm specification, and demonstrate how this can be used for specifying (executable) algorithms, and for automated testing of Hoare correctness statements about these algorithms. The small extension of Haskell that we will present and discuss can be viewed as a domain specific language for algorithm specification and testing.

The course will focus on sat solving, model checking and reasoning with predicate logic, on graph algorithms, on algorithms for matching, decision making and fair division, and on algorithms for (probabilistic) epistemic model checking.


The main tool for this course will be the functional programming language Haskell.

We assume you all have managed to install a working Haskell system on your laptop. The easiest way to get a working system is by downloading Stack or the Haskell Platform from here.

Stack is a tool for Haskell project development that offers a functional approach to package management in Haskell. See here.


Important Note (added Thursday Sept 8)

Malvin has put together some instructions on

How to use Haskell on the MoL room computers.

See here


Prerequisites

Previous experience with functional programming is a pre, but is not absolutely necessary. The course will start with a lightning introduction in programming with Haskell. At the end of the course the participants will all be experienced Haskell programmers.

Teaching Staff

  1. Jan van Eijck (lectures, code review and feedback).

  2. Malvin Gattinger (code review and feedback).

Dates

Sep 5 -- Oct 28, 2016

For details of the schedule, consult datanose

Set-up

The course consists of three components:

  1. Lectures: every Monday, 9.00 -- 10.45 (Note: from week 38 onwards the lectures are on Tuesday, 9.00 -- 10.45.)

  2. Computer Lab (using your own laptop): every Monday, 11.00 -- 12.45.

  3. Code Review Sessions: every Friday, 11.00 --12.45

The computer lab sessions will be unsupervised, but they give you a great opportunity to discuss course work and learn from each other. You are expected to hand in course work every week, with a deadline (revised) of Monday evening at midnight. The code you submit will be reviewed on Fridays.

It is up to you whether you want to work on the lab exercises alone or in pairs. If you choose to work in pairs you should still make sure you acquire individual skills.

Final Project

Last two weeks of the course (week 42 and week 43).

Grading

Average of your computer lab grade and your final project grade.

Make sure you acquire individual skills, by spending time on the lab exercises on your own.

Course Goals

  1. Learn the basics of functional programming in Haskell.

  2. Learn how to use type-specification and abstraction to make programs more easily testable.

  3. Learn how the functional programming paradigm relates to imperative programming.

  4. Learn how to use functional programming for your own logic projects.


Resources

Reference


Week 1

  1. Sign up on github and send us an email with your github name, so we can invite you to the github repository for the course.

  2. Lecture: Informal Introduction to Haskell. Lecture notes week 1 The code is in FSA1.hs.

  3. Lab 1 Code in FSAlab1.hs.

  4. Read the first two chapters of The Haskell Road and carry out the implementation exercises if you still need this.

  5. Notes for First Friday Session. Code is in FridaySession1.hs.


Week 2

  1. Lecture: Functional programming and imperative programming. Lecture notes week 2 The code discussed in the lecture is in FSA2.hs.

  2. Lab 2. Code in FSAlab2.hs.

  3. Read chapters 3 and 4 of The Haskell Road and carry out the implementation exercises if you still need this.

  4. Notes from the Friday session.


Week 3

  1. Lecture: Fixpoint Operations, and Reasoning about Functions. Lecture notes week 3 The code discussed in the lecture is in FSA3.hs.

  2. Lab 3. Code in FSAlab3.hs. Topic: Sudoku solving and sudoku generation.

  3. Read chapters 5 and 6 of The Haskell Road.

  4. Notes from the Friday session.


Week 4

  1. Lecture: Action and Interaction. Lecture notes week 4 The code discussed in the lecture is in FSA4.hs. To get more familiar with monadic programming, you are invited to play with this code.

  2. Lab 4. Code in FSAlab4.hs. Topic: stable matching and school allocation.

  3. Notes from the Friday session.


Week 5

  1. Lecture: Fast Modular Arithmetic and Public Key Cryptography. Lecture notes week 5 The code discussed in the lecture is in FSA5.hs.

  2. Lab 5. Code in FSAlab5.hs. Topic: Fast Modular Arithmetic and Public Key Cryptography.

  3. Friday session: feedback on current lab work, plus discussion of exam paper choices. Notes from the Friday session. Code is in FridaySession5.hs.


Week 6

  1. We used the first hour of our Tuesday session to kickstart the term paper writing process.

  2. Second hour: a quick tour through first order theorem proving, using these slides. Code that goes with the slides is in FSA6.hs. Note: this would also make a fine term paper project, for those who like guided instruction. Your term paper could consist of carrying out all implemetation exercises in the slides, followed by a conclusion with your reflection on the learning process.

  3. There will be a Friday meeting, with opportunity to get hints and feedback for your term paper.


Term papers

Here is an open-ended list of possible research topics.

Note This list was updated on Sept 24.

The deadline for submitting your report (via github) is Friday October 28, at midnight.

Upon request of the director of the MoL programme, this deadline is strict.