Type Theory (Laurea Magistrale in Matematica)


This page provides some information about the course. Also refer to ESSE3 for the syllabus and other information.

What is Type Theory about?

Prospective students can read an informal introduction.

Course Material

COVID-19 emergency notice

Due to the COVID-19 emergency, we can not perform the written exam in the standard way, gathering in the same room. Following the directions of the University of Trento, the exam will be performed in the following alternative way:

The written test will be performed online, using the Zoom platform, at the scheduled date and time, as reported on ESSE3. When the exam starts, students will receive the exam questions online as a PDF file, and will answer those questions by using their own pen & paper, while streaming themselves using Zoom so that we can monitor their activities. At the end of the exam, they will submit their paper answers as a scan or photo. Please remember to have some form of ID (e.g., identity card, passport) with you on this day.

Students will need to be available online on the exam day, but they do not need to be in any specific location. Students must be alone in a quiet room during the exam, without any course-related material in sight.

As an additional anti-cheating procedure, in the days following the written exam, some students might be asked to perform a quick additional oral test to verify the authorship and understanding of their submitted answers. This check might be performed by randomly selecting a few students, or because some suspicious activity was observed during the written test. If you are selected, you will be contacted by email.

The presentation part of the exam will also be performed using Zoom. Students will present the chosen topic in front of the instructor and other students. This can be performed before or after the written test, at any date and time agreed with the instructor, who will try to organize multiple presentations on the same day. We will try to avoid having the presentations on too many separate days, so that students can attend them more esily.

For everything else (e.g., marking rules), the ESSE3 syllabus still applies.

UPDATE: how to prepare for the online exam:

Please check that your equipment (computer, phone, or other device) is working before the test, including video and audio. You will need to keep both camera & microphone open during the exam, so try to find a quiet place. Test your Zoom installation as well.

Please disable screensavers or other locking mechanisms on your device, so that you don't need to continuously unlock it during the exam to keep the questions visible.

Video can drain your battery quickly during the exam, so keep your device plugged into a socket.

If you disconnect, don't panic but reconnect as quickly as possible.

Have some ID with you (identity card, passport, ...), as well as enough pens and paper.

At the end of the exam you will need to submit your answer by email, after scanning / taking a photo of your sheets, so please ensure you can do that with your device.

(end of notice.)

Presentation topics

This list is not exhaustive. You can propose another topic for your presentation. If you do, I will evaluate whether it is appropriate for the course and in such case approve it. For instance, if you find a programming language which has interestingly advanced types and you simply want to experiment with that and show some examples you tried, you can propose it.

Some topics are more complex others, but in such cases I only require a comparable effort to the one that would be needed for a simpler topic. For instance, you could skip a part of a complex paper, limiting yourself to the fundamental notions and results. You could also skip the proofs, and only present some examples.


The exam comprises a presentation and a written test.

Students have to individually study a topic related to type theory, which was not covered in the course, and present it. For instance, a research paper or book chapter can be presented.

The written test comprises both theoretical questions and exercises.


Home - Teaching

Valid CSS Valid XHTML 1.1 Roberto Zunino, 2016