Master Seminar: Functional Programming and Type Theory
Instructor: Luca Maio
Content
Functional programming has many advanced applications but most share one thing: they rely on a strong type system. This ensures a level of safety and correctness not easily achievable by imperative means. Further, dependent type theories can even be used to model mathematics as a whole and thus have computers check or even find proofs of real mathematical theorems. Interactive proof assistants such as Agda, Coq, Lean, and Matita are based on dependent type theory. After a short introduction to type theory, you will pick a topic in advanced functional programming or (dependent) type theory for your seminar paper and talk.
Prerequisites
- You need to either be familiar with the basics of functional programming, (e.g. already have some experience with a functional programming language, passed ProMo, etc.), or you need to be interested in learning about type theory from a more conceptual/mathematical point of view.
Organisation
There will be between 1 and 3 mandatory sessions (depending on previous knowledge of the attendees) at the beginning of the semester, where I will explain the organization of the course in detail, as well as present the basics of dependent type theory and maybe showcase some applications, after that we will fix your topics.
Topics can be chosen from the broad field of type theory, in that case I can provide pointers and give suggestions for topics depending on the specific interests, or they can be current topics of functional programming.
For the latter the following resources are available to choose a topic from among the proceedings of the following conferences:
After you had some time to familiarize yourself with the topic, there will be a mandatory session of short-talks (90 seconds) where you give a one-slide summary of your topic.
At the end of the semester we will take another 1 to 3 mandatory sessions for the seminar talks. In between there will be no scheduled meetings, but of course I will be available for questions on your topics either virtually via mail, Zulip etc. or in person.
Examination
The Examination consists of two parts:
- A written seminar paper on your chosen topic (60% of the grade), the length of which must be between 20.000 and 30.000 characters.
- A talk (40% of the grade) of 30 minutes plus 5-10 minutes discussion. The talk should cover some but possibly not all things written about in the seminar paper.
Submissions can be both in German and in English, the languages of the talk and the paper may even differ depending on your preference.
Schedule
TBD - First meeting should be ASAP, I will contact you about arranging a first slot and we will fix future dates there.
“Wn” stands for the n-th week of the year.
2023
====
--- start of winter semester
W42
W43
W44
W45
W46
W47
W48
W49
W50
W51
W52 holidays
2024
====
W01 holidays
W02
W03
W04
W05
W06
--- end of winter semester
W07
W08
W09
Artikelaktionen