### General Information

Course Code | X_401011 |
---|---|

Credits | 6 EC |

Period | P2 |

Course Level | 300 |

Language of Tuition | English |

Faculty | Faculty of Science |

Course Coordinator | dr. F. van Raamsdonk |

Examiner | dr. F. van Raamsdonk |

Teaching Staff |
dr. F. van Raamsdonk |

### Practical Information

You need to register for this course yourself

Last-minute registration is available for this course.

Teaching Methods | Seminar, Lecture, Practical |
---|

Target audiences

This course is also available as:

### Course Objective

The goal of the course is to obtain basic knowledge on the foundationsof functional programming via lambda calculus and equational reasoning,

and to acquire basic functional programming skills.

For the lambda calculus part:

At the end of the course, the student is familiar with the notions

reduction, fixed points, reduction strategy, confluence, normalization,

data type encoding, simple types and typability. The student is able to

give and analyze reduction sequences and reduction graphs, to encode

basic data types and recursive functions in the untyped lambda calculus,

to give typing derivations.

For the equational specifications part:

At the end of the course, the student is familiar with the notions

equational system, (syntactic) derivability, (semantical) consequence,

Birkhoff's theorem, initial model, isomorphisms, initially correct

specification. The student is able to define an equational

specification, to give a derivation, to analyze algebra's with respect

to being a model, containing junk or confusion, being an initial model,

to analyze homomorphisms and isomorphisms.

For the functional programming part:

At the end of the course, the student is familiar with the basics of the

functional programming language Haskell: pattern matching, recursive

functions,

algebraic data types, and with the basics of monads. The student is able

to write small Haskell programs with pattern matching, recursion, and is

able to deal with partial functions using monads.

### Course Content

In the practical work we use the functional programming languageHaskell. We practice with the basics such as lists, recursion,

data-types,

and a bit of monads.

The theoretical part is concerned with the foundations of functional

programming in the form of lambda calculus and equational reasoning.

We study in untyped lambda calculus reduction theory and expressive

power:

beta reduction, reduction strategies, confluence, encoding of

data-types, fixed point combinators and recursive functions.

In addition we study the lambda-calculus with simple types, its typing

system and a type inference algorithm, and possibly strong normalization

of simply typed lambda-calculus.

In equational specifications part we study the syntax and semantics of

equational systems, and we work towards the results that all initial

models are equal up to isomorphism, and that the term model is an

initial model.

### Teaching Methods

There are two lectures and two exercise classes per week which areconcerned with the theoretical part of the course. In addition, during

the first six weeks we have two programming afternoons for in total 6

hours per week.

### Method of Assessment

There is a written exam which contributes for 75% to the final grade,and there is a programming part consisting of three sets of Haskell

programming exercises which contribute for 25% to the final grade, with

the additional proviso that both the grade for the written exam and the

grade for the programming part must be at least 5.5 in order to obtain a

passing grade for the course.

The written exam is for approximately 10% concerned with Haskell, and

the remaining part is approximately equally divided between the subjects

lambda calculus and equational specifications.

There are non-obligatory homework exercises concerned with the

theoretical part which yield a bonus of at most 0.5 on the grade for the

written exam, provided that the grade for the written exam is at least

5.5.

The programming part consists of three sets of Haskell programming

exercises which are handed in via Canvas and contribute equally to the

grade for the programming part. It may be asked to explain the program

in an individual meeting.

### Literature

Course notes.### Target Audience

3CS, 3LI, 3IMM, 3W### Additional Information

This course is part of the minor Deep Programming.### Custom Course Registration

The registration procedure is the standard one.### Explanation Canvas

The schedule, slides for the lectures, material for the exerciseclasses, and programming assignments are available via the Canvas page

of the course.

### Recommended background knowledge

For the theoretical part familiarity with formal reasoning as forexample taught in the cours e Logic and Modelling is helpful.