Each module contains 3 ECTS. You choose a total of 10 modules/30 ECTS in the following module categories:
- 12-15 ECTS in technical scientific modules (TSM)
TSM modules teach profile-specific specialist skills and supplement the decentralised specialisation modules. - 9-12 ECTS in fundamental theoretical principles modules (FTP)
FTP modules deal with theoretical fundamentals such as higher mathematics, physics, information theory, chemistry, etc. They will teach more detailed, abstract scientific knowledge and help you to bridge the gap between abstraction and application that is so important for innovation. - 6-9 ECTS in context modules (CM)
CM modules will impart additional skills in areas such as technology management, business administration, communication, project management, patent law, contract law, etc.
In the module description (download pdf) you find the entire language information per module divided into the following categories:
- instruction
- documentation
- examination
Although widespread, the currently mainstream imperative, object-oriented programming paradigm, with testing as its main method of quality assurance, has its limitations. Even though it allows novices to write programs relatively quickly and without much formal training, such programs tend to become complicated as soon as they need to do something non-trivial. This makes them increasingly hard to write and reason about, making assurance methods that give better guarantees than software testing intractable. Similarly, even though it is possible to write software tests relatively quickly and without much formal training, such tests are only able to show the presence of faults, but never their absence.
Few are aware that there exist a number of alternatives to imperative, object-oriented programming and testing. This course will start with a broad overview of these alternatives, and then focus on one of them, functional programming, and the use of formal methods to specify and prove the correctness of functional programs.
Functional programming is an approach to programming where simplicity, clarity, and elegance are the key goals. It is the application of formal mathematical and programming-language-based techniques for the construction and verification of computer programs. Although it has a long history, it has recently received attention due to its potential for writing elegant, correct and efficient programs that are easier to write, compose, and maintain, once one is familiar with its underlying concepts. Its simplicity also allows reasoning about the correctness of functional programs using techniques taught in high-school mathematics. These techniques can not only be used to state and prove functional correctness of smaller programs on paper, but also large systems using automated proof assistants. Such automated proof assistants (e.g. Agda, Isabelle/HOL, Idris, Lean and Coq) are themselves applications and further developments of functional programming.
In the final segment of the course, we broaden our focus to explore sophisticated type systems in imperative, object-oriented and functional programming languages. These advanced type systems serve as effective tools for program verification, and have proven effective for identifying and eliminating critical bugs.
Prerequisites
All participants should be able to program in the functional and object-oriented styles to the degree that can be expected after attending an introductory-level undergraduate course on these topics.
Participants without prior experience in functional programming are required to work through the chapters 1 through 8 in the book "Programming in Haskell" (second edition) by Graham Hutton before starting the course.
Learning Objectives
All participants are able to explain and apply formal programming-language-based techniques for the construction and verification of computer programs. Special emphasis will be made on techniques that surpass some of the limitations of mainstream programming in the imperative object-oriented programming style, and on alternatives to mainstream testing-based software assurance methods.
All participants should be able to:
- enumerate and explain a number of different programming paradigms.
- construct programs in the functional style.
- verify the correctness of functional programs using formal proof.
- apply advanced type systems to make imperative, object-oriented and functional programs more secure.
Contents of Module
The following is a rough overview of the content of the course and is subject to change:
- Overview (1 week)
- A broad overview of different programming paradigms.
- Functional Programming (4 weeks)
- Fast paced revision of functional programming prerequisites and Haskell.
- Types for correctness, Input/Output in a pure language.
- Functional design patterns: Functor, Applicative and Monad with parsing as an example application.
- Application: Interpreters for a small imperative and functional programming language.
- Proving Programs Correct (5 weeks)
- Equational reasoning
- Structural induction
- Automated theorem proving
- Dependent types
- Advanced Type Systems (4 weeks)
- Subtyping with generic types (co- and contravariance)
- Subtyping lattices
- Ownership typing
- Effect systems
Teaching and Learning Methods
Interactive lectures explaining main concepts, interspersed with programming exercises and reading assignments.
Literature
You are required to have a copy of the following book during the course:
- Graham Hutton, Programming in Haskell, Second Edition, Cambridge, 2016.
Further material will be provided during the course as required.
Download full module description
Back