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 [5] .
Richard Garner (Macquarie University)
Wednesday  Thursday  Friday  Saturday  Sunday 

10:0011:00  10:0011:00  10:0011:00  10:0011:00  10:0011:00 
Lunch break  Lunch break  Lunch break  Lunch break  Lunch break 
14:3016:00 Chris Kapulkin  13:3015:00 Benno van den Berg  13:3015:00 Bas Spitters  14:3016:00 Egbert Rijke  13:3014:15 Dan Grayson 

 14:1515:00 Simon Hubert  
15:0016:00 Clemens Berger  15:0015:30 Tea  15:0015:30 Tea  
16:0016:30 Tea  16:0016:30 Tea  15:3017:00 Ulrik Buchholtz  16:0016:30 Tea  15:3016:15 Bas Spitters 
16:3018:00 Eric Finster  16:3018:00 Peter Lumsdaine  16:3018:00 Thomas Streicher  16:1517:00 Andrej Bauer  
17:0017:45 Peter Lumsdaine 
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.
To register please use [6]this registration webform [6]. There is no registration fee. For any further inquiries please send an email to htt2016@mpimbonn.mpg.de [7].
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 [8].
Attachment  Size 

[9]htt2016_MPIM_A3.pdf [10]  3.67 MB 
Links:
[1] http://www.mpimbonn.mpg.de/taxonomy/term/164
[2] http://www.mpimbonn.mpg.de/node/3444
[3] http://www.mpimbonn.mpg.de/node/6459/program?page=last
[4] http://www.mpimbonn.mpg.de/node/6459/abstracts
[5] http://www.mpimbonn.mpg.de/6486
[6] https://www.mpimbonn.mpg.de/node/6460
[7] mailto:htt2016@mpimbonn.mpg.de
[8] http://www.mpimbonn.mpg.de/node/3079
[9] http://www.mpimbonn.mpg.de/webfm_send/343/1
[10] http://www.mpimbonn.mpg.de/webfm_send/343