PhD course - Type Theory Seminar
Type Theory Seminar
Rasmus Møgelberg and course participants.
Date(s) of the course:
March 20 – June 5
Already planned TBA.
The goal of the type theory seminar is to keep up with current state of the art research in type theory and application of type theory. As such, the goal of attending the seminar is to discuss current trends in type theory, relate application and theory across wide ranging areas, apply state of the art techniques and identify application in new areas.
Abel et. Al, 2016: Interactive Programming in Agda – Objects and Graphical User Interfaces.
Abel and Pientka, 2016: Wellfounded Recursion with Copatterns and Sized Types.
Kavvos, 2019: Modalities, Cohesion and Information Flow
Shulman, 2015: Brouwer’s fixed-pint Theorem in Real-Cohesive Homotopy Type Theory
Riljke et Al, 2017: Modalities in Homotopy Type Theory
Brady, 2017: Type-Driven Development of Concurrent Communication System
More to be added as last part of course in planned by participants.
Type-driven Development of Concurrent Communcating Systems
Interactive Programming in Agda – Objects and Graphical User Interfaces.
Wellfounded Recursion with Copatterns and Sized Types
Modalites, Cohesion and Information Flow
Brouwer’s fixed-point theorem in real-cohesive homotopy type theory
Modalities in homotopy type theory
The rest of the programme is determined based on interest of participants.
To pass, a student must present a paper, or part of a paper corresponding to 2x45 min of lecture.
Amount of hours the student is expected to use on the course
Participation: 20 hours (Lectures and presentations)
Preparation: 115 hours (Reading articles and preparing presentation)