Workload:
180 h
|
Module Number INF3186 |
Module Title Programming with Dependent Types |
Type of Module Elective Compulsory |
|---|---|---|
| ECTS | 6 | |
|
Work load - Contact time - Self study |
Workload:
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 | |
| Content | 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. |
|
| Objectives | 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
Status
SWS
Credits
Type of Exam
Exam duration
Evaluation
Calculation
of Module (%) |
|
| Prerequisite for participation | INFM1110 Practical Computer Science 1: Declarative Programming | |
| Lecturer / Other | Brachthäuser | |
| Literature | - |
|
| Last offered | unknown | |
| Planned for | Wintersemester 2023 | |
| Assigned Study Areas | BIOINFM2510, INFM2510, INFM3110, MDZINFM2510, MEINFM3210 | |