Module Number

Module Title

Programming with Dependent Types
Type of Module

Elective Compulsory
Work load
- Contact time
- Self study
180 h
Class time:
60 h / 4 SWS
Self study:
120 h
Duration 1 Semester
Frequency In the winter semester
Language of instruction German and English
Type of Exam

Grading of the course results

Lecture type(s) Practical Course

Type systems help programmers to ensure properties of programs across all executions of the program. The more expressive the type system, the more properties can be covered in this way. A particularly expressive class of type systems are those with dependent types. With these, the type of programs can depend on concrete runtime values. Programming in such programming languages requires theoretical knowledge and above all practical experience. Both are taught in this practical course.


Students know what constitutes a programming language with dependent types, what additional expressive power is available at the type level and can use it practically in concrete programs. They recognize which properties of the program can be ensured by dependent types and which sources of errors can be avoided. They also understand what additional effort is required to do this and can thus make an informed decision about using a programming language with dependent types.

Allocation of credits / grading
Type of Class
Type of Exam
Exam duration
of Module (%)
Prerequisite for participation INFM1110 Practical Computer Science 1: Declarative Programming
Lecturer / Other Brachthäuser


Last offered unknown
Planned for Wintersemester 2023
Assigned Study Areas BIOINFM2510, INFM2510, INFM3110, MDZINFM2510, MEINFM3210