Organized by COST action CA15123 The European research network on types for programming and verification (EUTypes) .

Summary

Types are pervasive in programming and information technology. A type defines a formal interface between software components, allowing the automatic verification of their connections, and greatly enhancing the robustness and reliability of computations and communications. In rich dependent type theories, the full functional specification of a program can be expressed as a type. Type systems have rapidly evolved over the past years, becoming more sophisticated, capturing new aspects of the behaviour of programs and the dynamics of their execution.

The aim of this summer school is to provide advanced training, especially to PhD students and early-career researchers, in all aspects of the theory and practice of type theory and applications.

Lecturers and Topics

• Course 0: Matthieu Sozeau: Introduction to Dependent Type Theory
• Course 1: Fredrik Nordvall Forsberg: Introduction to HOTT
• Course 2: Enrico Tassi: The Coq proof assistant and the Mathematical Components library
• Course 3: Mariangiola Dezani-Ciancaglini: Session Types: an introduction
• Course 4: Danel Ahman: Program Verification with F*
• Exercise classes and local support: Marino Miculan and Marija Mihova

Organising Committee

• Herman Geuvers (Radboud University Nijmegen, Netherlands), chair of the action
• Marino Miculan (University of Udine , Italia), chair
• Marija Mihova (Ss Cyril and Methodious University, Macedonia), local organizer