Equational Programming

Dit vak wordt in het Engels aangeboden. Omschrijvingen kunnen daardoor mogelijk alleen in het Engels worden weergegeven.

Doel vak

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.

Inhoud vak

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.


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.


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.


3CS, 3LI, 3IMM, 3W

Overige informatie

This course is part of the minor Deep Programming.

Afwijkende intekenprocedure

The registration procedure is the standard one.

Toelichting Canvas

The schedule, slides for the lectures, material for the exercise
classes, and programming assignments are available via the Canvas page
of the course.

Aanbevolen voorkennis

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

Algemene informatie

Vakcode X_401011
Studiepunten 6 EC
Periode P2
Vakniveau 300
Onderwijstaal Engels
Faculteit Faculteit der Bètawetenschappen
Vakcoördinator dr. F. van Raamsdonk
Examinator dr. F. van Raamsdonk
Docenten dr. F. van Raamsdonk

Praktische informatie

Voor dit vak moet je zelf intekenen.

Voor dit vak kun je last-minute intekenen.

Werkvormen Werkcollege, Hoorcollege, Practicum

Dit vak is ook toegankelijk als: