October 8-9 at Aarhus University

EUTYPES 2018 at Aarhus University. Aarhus Institute of Advanced Studies (AIAS) Høegh-Guldbergs Gade 6B, 8000 Aarhus

The EUTypes working meetings are open to all members of the EUTypes COST network, as well as to all other researchers interested in topics such as Homotopy type theory, types and security as well as concurrent seperation logic. EUTypes is sponsored by COST Action EUTypes CA15123.

The meeting will consists of a number of more general introductory talks and a number of shorter talks for each working group.  We encourage discussions about ongoing work, problem statements, progress reports, as well as presentation of latest results. Most talks will be by invitation, but if you would like to participate, please send an e-mail to Bas Spitters ( In case you propose a talk, please include a title and a short description of the topic. Deadline for proposing talks: September 9.

Participation in EUTypes costs €70 which covers two lunches, coffee, cake and dinner on October 8.


Event organizers

Lars Birkedal

ProfessorDepartment of Computer Science
H bldg. 5341, 225/227
P +4523838546
P +4523838546

Bas Spitters

Associate professorDepartment of Computer Science


Sofia Rasmussen

Research Group CoordinatorDepartment of Computer Science

Program (subject to change!)

Monday, October 8

Morning: general talks (Chair: )

        08:30 - 09:00 Registration

Types in industry

        09:00 - 09:45 Nick Benton, Software engineer, Facebook research

        09:45 - 10:15 Behavioural Type-based Static Verification Framework for Go by Nobuku Yoshida, Professor at Imperial College London

        10:15 - 10:45 break

        10:45 - 11:30  Arnaud Spiwack, Senior Software Architect, tweag I/O

        11:30 - 12:00 Using reflection to eliminate reflection by Théo Winterhalter, Inria France

        12:00 - 14:00 Lunch

Afternoon: WG1 Theoretical foundations

        14:00 - 14:45 Peter Lumsdaine, Assistant professor at Stockholm university

        14:45 - 15:15 Universes in a Type Theory for Synthetic Infinity-Category Theory by Jonathan Weinberger, PhD student at Department of Mathematics, Technische Universität Darmstadt

        15:15 - 15:45 break

        15:45 - 16:30  Higher inductive types in cubical type theories by Anders Mörtberg, Postdoc at the School of Computer Science at Carnegie Mellon University

        16:30 - 17:00 Bicategories in Homotopy Type Theory by Niels van der Weide, Radboud University, Nijmegen

        17:00 - 17:30 A mode theory for a type theory of cubical and simplicial types by Ulrik Buchholtz, Department of Mathematics, Technische Universität Darmstadt

Evening 19:00: Conference diner at No.16, Europaplads 16, 8000 Aarhus C


Tuesday, October 9

Morning: Types for security and probability

        09:00 - 09:45 Pierre-Yves Strub, Maître de conférences at École Polytechnique

        09:45 - 10:15 Invertible Transformations of Types and Their Applications to, by Security by Sergei Soloviev, Institut de Recherche en Informatique de Toulouse (IRIT)

        10:15 - 10:45 break

        10:45 - 11:30 Mathematics in Lean, by Johannes Hölzl, Postdoc at Vrije Universiteit Amsterdam

        11:30 - 12:00 TBA

        12:00 - 14:00 Lunch

Afternoon: WG3/ WG4, Types for Verification/Types for Programming

        14:00 - 14:45  Ales Bizjak, Postdoc at Department of computer science, Aarhus University

        14:45 - 15:15 Bisimulation as path type for guarded recursive types by Niccolò Veltri, Postdoc at IT University of Copenhagen

        15:30 - 15:45 break

        15:45 - 16:30  #MoSeL: A General, Extensible Modal Framework for Interactive Proofs in Separation Logic by Robbert Krebbers, Assistant professor at Delft University of technology

        16:30 - 17:00 TBA

        17:00 - 17:30 Thorsten Altenkirch, professor at University of Nottingham