EUTYPES2018

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 (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.

The registration deadline for EUTypes 2018 has passed.

 

Event organizers

Lars Birkedal

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

Bas Spitters

Associate professorDepartment of Computer Science

Administration

Sofia Rasmussen

Research Group CoordinatorDepartment of Computer Science

Monday, 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

 

Tuesday, October 9

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