Equational Programming


Course Objective

The goal of the course is to obtain basic knowledge on the foundations
of 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
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 language
Haskell. We practice with the basics such as lists, recursion,
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
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 are
concerned 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

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.


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 exercise
classes, and programming assignments are available via the Canvas page
of the course.

Recommended background knowledge

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

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: