Skip to main content

Workshop on Homotopy Type Theory

Posted in
Organiser(s): 
Michael Batanin, Christian Blohmann, Ralph Kaufmann, Martin Markl
Date: 
Wed, 2016-02-10 08:00 - Sun, 2016-02-14 22:00
Location: 
MPIM Lecture Hall

 

 

The workshop will give the participants the chance to discuss of current problems in areas of active research in homotopy type theory. Each day will start with a lecture series by Vladimir Voevodsky on "Dependent Type Theory", followed by open seminars in which workshop participants can give short presentations on their research.

The lecture series by Vladimir Voevodsky was recorded and can be found here .

Workshop co-ordinator:

Richard Garner (Macquarie University)

Preliminary list of participants

Ahrens, Benedikt (Institute for Advanced Study )
Awodey, Steve (Carnegie Mellon University )
Bakovic, Igor (Croatia)
Bauer, Andej (University of Ljubljana)
Berger, Clemens (Université de Nice - Sophia Antipolis)
Blanc, David (University of Haifa )
Bordg, Anthony (Charles University Prague)
Breen, Lawrence (Université Paris Nord 13 )
Brunerie, Guillaume (École normale supérieure Paris)
Buchholtz, Ulrik (Carnegie Mellon University )
Cartier, Pierre (IHES)
Chapoton, Frederic (Université de Strasbourg)
Coquand, Thierry (Department of Computer Science and Engineering)
Curien, Pierre-Louis (Université Paris Diderot )
David, Sabonis (TU Munich)
Dotsenko, Vladimir (Trinity College Cambridge )
Doubek, Martin (Charles University Prague )
Durov, Nicolai (V. A. Steklov Institute of Mathematics )
Escardo, Martin (University of Birmingham)
Finster, Eric (LIX, École Polytechnique)
Fiore, Marcelo (University of Cambridge )
Fresse, Benoit (Université de Lille 1 )
Galvez Carrillo, Maria Immaculada (Universitat Politècnica de Catalunya)
Garner, Richard (Macquarie University )
Grayson, Dan (University of Illinois at Urbana-Champaign)
Haselwarter, Philipp (U.F.R. Mathématiques)
Hinich, Vladimir (University of Haifa )
Hofstra, Pieter Jan  (University of Ottawa )
Huber, Simon (Chalmers University of Technology)
Jaun, Lukas (Institute of Computer Science)
Joyal, André (Université du Quebec à Montréal )
Jurco, Branislav (Charles University )
Kapulkin, Chris (The University of Western Ontario )
Kassel, Christian (Université de Strasbourg et CNRS)
Kock, Joachim (Universitat Autònoma de Barcelona )
Le Grignou, Brice (Université de Nice - Sophia Antipolis)
Livernet, Muriel (Université Paris Diderot)
Lumsdaine, Peter (Stockholm University)
Makkai, Michael (McGill University)
Maltsiniots, Georges (Université Paris Diderot)
Martin-Löf, Per (Stockholm University)
Moerdijk, Ieke (Utrecht University )
Neeman, Amnon (The Australian National University )
Newstead, Clive (Carnegie Mellon University)
North, Paige (University of Cambridge)
Palmgren, Erik (Stockholm University)
Rijke, Egbert (Carnegie Mellon University)
Robayo Mesa, Jaime Andrés (Universidad Nacional de Colombia)
Ronco, Maria Ofelia (Universidad de Talca )
Salvatore, Paolo (Universit a di Roma Tor Vergata )
Sattler, Christian (University of Leeds )
Schreiber, Urs (Czech Academy of Sciences )
Shin, Heayong (Department of Mathematics)
Sinha, Dev Parakash (University of Oregon )
Sojakova, Kristina (Carnegie Mellon University)
Spitters, Bas (Aarhus University)
Streicher, Thomas (Technische Universität Darmstadt )
Szawiel, Stanisław (University of Warsaw)
Tonks, Andrew (University of Leicester)
Trlifaj, Jan (Charles University)
Vallette, Bruno (Université Paris Nord 13 )
van den Berg, Benno (University of Amsterdam )
Verchinine, Vladimir (Université Montpellier II )
Voevodsky, Vladimir (Institute for Advanced Study )
von Glehn, Tamara (University of Cambridge)
Weber, Mark (Macquarie University )
Wellen, Felix (Karlsruhe Institute of Technology)
Zawadowski, Marek (University of Warsaw)
 

Schedule

WednesdayThursdayFridaySaturdaySunday
Workshop on Homotopy Type Theory February 10 - 14, 2016

10:00-11:00
Voevodsky

10:00-11:00
Voevodsky

10:00-11:00
Voevodsky

10:00-11:00
Voevodsky

10:00-11:00
Voevodsky

Lunch break

Lunch break

Lunch break

Lunch break

Lunch break

14:30-16:00
Chris Kapulkin
13:30-15:00
Benno van den Berg
13:30-15:00
Bas Spitters
14:30-16:00
Egbert Rijke
13:30-14:15
Dan Grayson

 

  

 

14:15-15:00
Simon Hubert
 
15:00-16:00
Clemens Berger
15:00-15:30
Tea
 
15:00-15:30
Tea
16:00-16:30
Tea
16:00-16:30
Tea
15:30-17:00
Ulrik Buchholtz
16:00-16:30
Tea
15:30-16:15
Bas Spitters
16:30-18:00
Eric Finster
16:30-18:00
Peter Lumsdaine
 
16:30-18:00
Thomas Streicher
16:15-17:00
Andrej Bauer
    
17:00-17:45
Peter Lumsdaine
 

Lectures by Vladimir Voevodsky: "Dependent Type Theories"

Abstract: Modern dependent type theories exist mostly in the form of computer programs. As such they are objects of the physical reality more than they are objects of the mathematical one. For three decades the world of type theories was relatively calm - innovation was largely occurring in the layers of programming above the type theories leading to proof assistants with more and more sophisticated systems for notation, implicit arguments and tactics.

The discovery of the univalent models led to the addition of new features to the existing type theories as well as to the development of entirely new ones such as cubicaltt. Eventually, these new type theories will become the cores of proof assistants with much more convenient than before environments for formal verification of mathematical arguments.

It is clear that the only way to ensure that these new proof assistants are reliable - that any proof of “false” in such a proof assistant can be mechanically transformed into a proof of “false” in one of the “consistency standards”, is to have a system where a new proof assistant has to be formally certified using an already certified proof assistant against an already certified formal system before it can become accepted as a reliable tool in pure mathematics.

The strongest consistency standard available in pure mathematics is ZFC. This means that as a prerequisite  for such a certification system we need to have a mathematical theory of dependent type theories that can be formalized in ZFC. At the moment only fragments of this future theory exist. I will give an introduction to my vision of the theory by describing these fragments and pointing out the gaps.

Organizing committee

Michael Batanin (Macquarie University)
Christian Blohmann (MPIM Bonn)
Ralph Kaufmann (Purdue University)
Martin Markl (Czech Academy of Sciences)

Registration

To register please use this registration webform. There is no registration fee. For any further inquiries please send an email to htt2016@mpim-bonn.mpg.de.

Hotel reservations

If you would like us to make a hotel reservation for you, please state this on the registration webform. We can only honor requests for hotel reservations made by January 31,  2016. If you would like to make a hotel reservation by yourself you will find a list of hotels here.

 

AttachmentSize
File htt2016_MPIM_A3.pdf3.67 MB
© MPI f. Mathematik, Bonn Impressum
-A A +A