EUTypes Summer School

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: Silvia Ghilezan, Aleksy Schubert, Introduction to type theory: Untyped and simply typed lambda calculi, pure type systems
• Course 2: Robbert Krebbers, The Coq proof assistant for proving and programming
• Course 3: Conor McBride, Dependently typed programming, Agda
• Course 4: Andrei Paskevich, Program verification in Why3
• Course 5: Thorsten Altenkirch, Introduction to homotopy type theory

Organising Committee

• Herman Geuvers (Radboud University Nijmegen, Netherlands), chair of the action
• Marija Mihova (Ss Cyril and Methodious University, Macedonia), local organizer
• Tarmo Uustalu (Tallinn University of Technology, Estonia), vice-chair of the action