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 either 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 Fr. 20.10. 14:00 L109 First Meeting and start of Type Theory Introduction
W43
W44 Fr. 03.11. 16:00 Room 151 (Oett. 67) Cont. TT-Intro
W45 We. 08.11. 16:00 L109 Cont. TT-Intro
W46
W47
W48 We. 29.11. 16:00 L109 Quick Talks - Send me slide via E-Mail until the date
W49
W50
W51
W52 holidays
2024
====
W01 holidays - Su. 07.01. 23:59 Deadline submission first draft (Modus TBD)
W02
W03 Th. 18.01. 23:59 Deadline subission reviews
W04 Seminar talks (Room TBD? L109 if you hear nothing):
Send me your slides via E-Mail before your talk!
Mo. 22.01. 09:00 - 13:00
<Schedule goes here (TBD)>
We. 24.01. 09:00 - 13:00
<Schedule goes here (TBD)>
Fr. 26.01. 13:00 - 19:00
<Schedule goes here (TBD)>
W05
W06
--- end of winter semester
W07
W08
W09 Su. 03.03. 23:59 Deadline for submission of seminar paper
Artikelaktionen