Workshop on Homotopy Type Theory

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

Workshop co-ordinator:

Richard Garner (Macquarie University)

Preliminary list of participants

Schedule

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

Registration

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

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 [8].

Attachment	Size
[9]htt2016_MPIM_A3.pdf [10]	3.67 MB