October 8-9 at Aarhus University
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 a 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 (spitters@cs.au.dk). 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.
08:30 - 09:00 Registration and coffee
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 Nobuko Yoshida, Imperial College London
10:15 - 10:45 coffee break
10:45 - 11:30 Linear Haskell: some hows and whys by 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 A general definition of dependent type theories by 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 18:30: Conference diner at No.16, Europaplads 16, 8000 Aarhus C
Morning: Types for security and probability
09:00 - 09:45 Jasmin: High-Assurance and High-Speed Cryptography by 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 Using Types in Composed Cryptographic Proofs by Konrad Kohbrok, Aalto University
12:00 - 14:00 Lunch
Afternoon: WG3/ WG4, Types for Verification/Types for Programming
14:00 - 14:45 Precise reasoning about resources in an affine separation logic by Aleš 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 Correct-by-construction interpretation of imperative state by Arjen Rouvoet, PhD student at TU Delft
17:00 - 17:30 Thorsten Altenkirch, professor at University of Nottingham
