print · login   

WG meeting in Nijmegen

EUTypes meeting, Nijmegen, Netherlands, 22-24 January 2018

Radboud University, Mercator building

Travel and accommodation information you can find here.

Registration

The registration system is now open. After registration, you will receive a link to our payment system via email.
This link needs to be activated by our financial department, so it may take some time before you receive this mail.
During the Holidays from 23 December 2017 untill 2 January 2018 our university is closed.
Registration form

Registration costs: 60 euros.

The costs include:

  • Meeting room
  • Coffee breaks
  • Lunches
  • Conference dinner on Tuesday

Overview

The EUTypes working meetings are open to all members of the EUTypes COST network, as well as to all other researchers interested in the topic. We encourage discussion about ongoing work, problem statements, progress reports, as well as presentation of latest results. The meeting will consists of a number of more general introductory talks and a number of shorter talks for each working group. Most talks will be by invitation. If you would like to participate, please send an e-mail to Herman Geuvers (herman@cs.ru.nl). In case you propose a talk, please include a title and a short description of the topic.

Program

See the abstracts page

The schedule below is still preliminary

January 22

  • Morning: general talks (Chair: Herman Geuvers)
    • 08:30 - 09:00 Registration
    • 09:00 - 09:45 Conor McBride (Strathclyde, UK) - Cubical Adventures pic movie slides notes
    • 09:45 - 10:00 break
    • 10:00 - 10:45 Brigitte Pientka (McGill, Canada, UK) - POPLMark Reloaded: Mechanizing Logical Relations Proofs slides
    • 10:45 - 11:00 break
    • 11:00 - 11:45 Gabriel Scherer (Inria Saclay, France) - Proof theory for type systems slides
    • 11:45 - 12:00 break
    • 12:00 - 12:30 Danko Ilik (Trusted Labs, France) - Industrial use of proof assistants: Common Criteria evaluations
  • 12:30 - 14:00 Lunch
  • Afternoon: talks to commemorate the legacy of Vladimir Voevodsky (Chair: Marc Bezem)
    • 14:00 - 14:15 Andrej Bauer (Ljubljana, Slovenia) - Introduction
    • 14:15 - 15:00 Thierry Coquand (Chalmers Gothenburg, Sweden) - Some contributions of Vladimir Voevodsky to dependent type theory slides
    • 15:00 - 15:15 break
    • 15:15 - 16:00 Nicolas Tabareau (Inria Nantes, France) - Homotopy Types and Resizing Rules: a fresh look at the impredicate sort of CIC slides
    • 16:00 - 16:15 break
    • 16:15 - 17:15 Andrej Bauer (Ljubljana, Slovenia) - Derivations as computations

January 23

  • Morning: WG1, Theoretical Foundations (Chair: Andrej Bauer)
    • 09:00 - 09:30 Stefano Berardi (Torino, Italy) - A possible reformulation of polymorphism: the simply typed lambda calculus N slides
    • 09:30 - 10:00 Jan Bessai (Dortmund, Germany) - Combinatory Logic Beyond S and K slides
    • 10:00 - 10:15 break
    • 10:15 - 10:45 Pawel Urzyczyn (Warsaw, Poland) - First-order answer set programming as constructive proof search slides
    • 10:45 - 11:15 Bas Spitters (Aarhus, Denmark) - Internal Universes in Models of Homotopy Type Theory paper slides
    • 11:15 - 11:30 break
    • 11:30 - 12:00 Ambrus Kaposi (ELTE Budapest, Hungary) - Towards a syntax for higher inductive inductive types slides
    • 12:00 - 12:30 Niels van der Weide (Radboud Nijmegen, The Netherlands) - Finite sets in HoTT slides
  • 12:30 - 14:00 Lunch
  • Afternoon: WG4, Types for Verification (Chair: Keiko Nakata, Andreas Abel)
    • 14:00 - 14:30 Carsten Schürmann (ITU Copenhagen, Denmark) - Evidence
    • 14:30 - 15:00 Chantal Keller (LRI Paris France) - Mixing type-based proof techniques for the verification of the SQL compilation chain slides
    • 15:00 - 15:30 Wilmer Ricciotti (University of Edinburgh, UK) - Mechanising the Metatheory of SQL with Nulls
    • 15:30 - 15:45 break
    • 15:45 - 16:15 Kenji Maillard (ENS Paris, France) - F*, from practice to theory slides
    • 16:15 - 16:45 Danel Ahman (Inria Paris, France) - Leveraging monotonic state in F* slides
    • 16:45 - 17:00 break
    • 17:00 - 17:30 Cyril Cohen (Inria Sophia Antipolis, France) - Foundations of 3D geometry to model robot manipulators slides
    • 17:30 - 18:00 Milena Vujosevic Janicic (University of Belgrado, Serbia) - A calculus for a LLVM-based software verification tool LAV slides
  • Evening 19:00: Conference diner: in De Waagh, Grote Markt 26, 6511 KB Nijmegen (see the back side of your participants badge). Closest parking garage: Eiermarkt, Eiermarkt 20

6511 TP Nijmegen.

January 24

  • Morning: WG3, Types for Programming (Chair: Conor McBride)
    • 09:00 - 09:30 Ralf Hinze (Radboud Nijmegen, The Netherlands) - Combles
    • 09:30 - 10:00 Ralph Matthes (CNRS, IRIT, Toulouse, France) - Intensional and univalent aspects of rule-based programming
    • 10:00 - 10:15 break
    • 10:15 - 10:45 Ulrich Schöpp (Ludwig Maximilian Universitat, Munich, Germany) - Defunctionalisation as Modular Closure Conversion slides
    • 10:45 - 11:15 Andreas Nuyts (Leuven, Belgium) - Degrees of Relatedness slides
    • 11:15 - 11:30 break
    • 11:30 - 12:00 Wouter Swierstra (Utrecht, The Netherlands) - Calculating correct programs slides
    • 12:00 - 12:30 Andreas Abel (Gothenburg, Sweden) - Normalization by Evaluation for Sized Dependent Types slides
  • 12:30 - 14:00 Lunch
  • Afternoon: WG2, Type-theoretic Tools (Chair: Freek Wiedijk)
    • 14:00 - 14:30 Thibaut Benjamin (École polytechnique, France) - Type theory for weak ω-categories
    • 14:30 - 15:00 Sophie Bernard (Inria, France) - An extension of libraries for polynomials
    • 15:00 - 15:30 Łukasz Czajka (University of Copenhagen, Denmark) - CoqHammer: A General-Purpose Automated Reasoning Tool for Coq slides
    • 15:30 - 15:45 break
    • 15:45 - 16:15 Johannes Hölzl (VU Amsterdam, The Netherlands) - Mathlib: Lean's math library slides
    • 16:15 - 16:45 Pierre-Marie Pédrot (MPI Saarbrücken, Germany) - Proof assistants for free[*]!
    • 16:45 - 17:00 break
    • 17:00 - 17:20 Matthieu Sozeau (Université Paris Diderot, France) - - Nested, Well-Founded and Mutual recursion in Equations slides
    • 17:20 - 17:40 Philipp Haselwarter (University of Ljubljana, Slovenia) - Algorithmic inversion principles for Extensional Type Theory slides
    • 17:40 - 18:00 Dmitriy Traytel (ETH Zürich, Switzerland) - Foundational Nonuniform (Co)datatypes in Higher-Order Logic slides

Organisation

Herman Geuvers
Simone Meeuwsen