Type Theory, Homotopy Theory and Univalent Foundations

CRM (Barcelona), September 23-27, 2013.

Main page: http://www.crm.cat/2013/ctype

The present page serves only to make available latest news while the official page is frozen for August while the CRM is closed.

Objectives

Over the past few years, deep and surprising connections have emerged between type theory and homotopy theory. These links provide a previously unavailable topological intuition for working with type theories and are at the heart of Voevodsky's Univalent Foundations of Mathematics programme. This programme seeks to develop a new approach to the development of mathematics, on the basis of type theories that include axioms motivated by homotopy theory, such as the Univalence Axiom, with an associated formalisation within proof assistants based on type theory, such as Coq and Adga. Ongoing research in this area involves also the links between homotopy theory and higher-dimensional category theory that have been intensively developed in recent years. This conference aims at bringing together leading experts in type theory and homotopy theory, as well as interested researchers from related areas such as mathematical logic, theoretical computer science and category theory, to exchange the latest results and ideas, and to set out directions for further exploration of the subject. The conference is timed to serve also as a venue for presenting the advances made during the special year on Univalent Foundations at the Institute for Advanced Study.

Invited speakers

  • Richard Garner, Macquarie University, Sydney, Australia
  • André Joyal, UQAM, Montréal, Canada
  • Peter LeFanu Lumsdaine, IAS, Princeton, USA
  • Thomas Streicher, Technische Universität Darmstadt, Germany

Confirmed contributed talks

  • Steve Awodey
  • Bruno Barras
  • Guillaume Brunerie
  • Favonia
  • Dan Grayson
  • Hugo Herbelin
  • Krzysztof Kapulkin
  • Yves Lafont
  • Zhaohui Luo
  • Jack Morava
  • Paige North
  • Erik Palmgren
  • Emily Riehl
  • Egbert Rijke
  • Urs Schreiber
  • Kristina Sojakova
  • Bas Spitters

Programme outline

Tuesday afternoon is free.
Tuesday is the Mercè Festival, Barcelona's Festa Major, also called the "Festival of festivals".

Scientific committee

  • Steve Awodey (Carnegie Mellon University)
  • Thierry Coquand (Chalmers University)
  • Nicola Gambino (University of Palermo)
  • Joachim Kock (Universitat Autònoma de Barcelona)
  • Vladimir Voevodsky (Institute for Advanced Study)

Organising committee

  • Joachim Kock, Universitat Autònoma de Barcelona
  • Nicola Gambino, Università degli Studi di Palermo & University of Leeds

Registration

See the main page: http://www.crm.cat/2013/ctype

Deadline for registration and payment: September 1st, 2013

Registration fee: 220€

Junior registration fee (for PhD students and post-docs having read the thesis in the last three years): 110€

The registration fee and the junior registration fee cover: attendance to the lectures, documentation package, and coffee breaks.

Reduced registration fee (available to researchers affiliated to local universities and members of the Societat Catalana de Matemàtiques): 70€

The local fee covers: attendance to the lectures, documentation package, and coffee break.

Related events

In the week prior to the conference, Peter Lumsdaine will give four lectures on Homotopy Theory in Type Theory at the IMUB, downtown Barcelona. For more information see .

In the weekend 27-29 September the yearly Barcelona Topology Workshop will take place in Sant Fruitós de Bages, some 50km from Barcelona. (The lectures will start on Saturday 28. The only Friday activity will be the conference dinner Friday night.)

Last updated: 2013-08-27 by Joachim Kock.