PhD course - Type Theory Seminar

Course:

Type Theory Seminar

Organizer(s):

Rasmus Møgelberg

Course website: 

http://pls.itu.dk/Type_theory_seminar.html

Lecturer(s):

Rasmus Møgelberg and course participants.

Date(s) of the course:

March 20 – June 5

Time:

Wednesdays 10-12

Room preferences:

Already planned TBA.

Course description:

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.       

Reading list:

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.

Programme:

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.

Exam:

To pass, a student must present a paper, or part of a paper corresponding to 2x45 min of lecture.

Credits:

5 ECTS

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)