Introduction to Type Theory [1 ECTS, SSD: Mat/01]

Type Theory is at the same time an alternative to set theory as a mathematical foundation and a programming language originally conceived by the Swedish philosopher and mathematician Per Martin-Löf. The course is an introduction to Type Theory which covers the following topics:

    λ-calculus and combinatory logic
    Propositions as types
    Classical vs intuitionistic reasoning
    Dependent types, Π- and Σ-types
    Reasoning in Type Theory, Equality
    Inductive and coinductive types
    Universes and paradoxes
    Homotopy Type Theory
    
The Agda system will be used for examples and exercises.

Timetable and venue: 

• Monday 27th: 16:30-18:30 - Aula G (2 hrs core lectures)
• Tuesday 28th:  08:30-10:30 - Aula T.04 (2 hrs core lectures) 
• Wednesday 29th:  08:30-11:30 - Aula T.04 (2 hrs core lectures + 1 h supplementary lecture)
• Friday 31st: 16:30-19:30 - Aula T.04 (3 hrs supplementary lectures)

All lectures will be held in Ca' Vignal 2 and 3, strada Le Grazie 15, Verona.