The EMS Publishing House is now EMS Press and has its new home at

Please find all EMS Press journals and articles on the new platform.

Oberwolfach Reports

Full-Text PDF (300 KB) | Introduction as PDF | Metadata | Table of Contents | OWR summary
Online access to the full text of Oberwolfach Reports is restricted to the subscribers of the journal, who are encouraged to communicate their IP-address(es) to their agent or directly to the publisher at
Volume 8, Issue 1, 2011, pp. 609–638
DOI: 10.4171/OWR/2011/11

Published online: 2011-09-04

Mini-Workshop: The Homotopy Interpretation of Constructive Type Theory

Steve Awodey[1], Richard Garner[2], Per Martin-Löf[3] and Vladimir Voevodsky[4]

(1) Carnegie-Mellon University, Pittsburgh, USA
(2) Macquarie University, Sydney, Australia
(3) Stockholm University, Sweden
(4) Institute for Advanced Study, Princeton, USA

Over the past few years it has become apparent that there is a surprising and deep connection between constructive logic and higherdimensional structures in algebraic topology and category theory, in the form of an interpretation of the dependent type theory of Per Martin-Löf into classical homotopy theory. The interpretation results in a bridge between the worlds of constructive and classical mathematics which promises to shed new light on both. This mini-workshop brought together researchers in logic, topology, and cognate fields in order to explore both theoretical and practical ramifications of this discovery.

No keywords available for this article.

Awodey Steve, Garner Richard, Martin-Löf Per, Voevodsky Vladimir: Mini-Workshop: The Homotopy Interpretation of Constructive Type Theory. Oberwolfach Rep. 8 (2011), 609-638. doi: 10.4171/OWR/2011/11