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 1: Hugo Herbelin: Introduction to lambda calculus & type theory
• Course 2: Jesper Cockx: Correct-by-construction programming in Agda
• Course 3 : Yves Bertot: Introductory course on Coq/Gallina
• Course 4 : Xavier Leroy: Proving the correctness of a compiler
• Course 5: Nicolai Kraus: Introduction to homotopy type theory

• Exercise classes and local support: Thorsten Altenkirch, Herman Geuvers and Marija Mihova

Organising Committee

• Herman Geuvers (Radboud University Nijmegen, Netherlands), chair of the action
• Thorsten Altenkirch (University of Nottingham), chair
• Marija Mihova (Ss Cyril and Methodious University, Macedonia), local organizer