Abstract
Homotopy Type Theory is a new, homotopical interpretation of constructive type theory. It forms the basis of the recently proposed Univalent Foundations of Mathematics program. Combined with a computational proof assistant, and including a new foundational axiom – the Univalence Axiom – this program has the potential to shift the theoretical foundations of mathematics and computer science, and to affect the practice of working scientists. This talk will survey the field and report on some of the recent developments.
Partially supported by the U.S. Air Force Office of Sponsored Research.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Awodey, S. (2015). Homotopy Type Theory. In: Banerjee, M., Krishna, S.N. (eds) Logic and Its Applications. ICLA 2015. Lecture Notes in Computer Science, vol 8923. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-45824-2_1
Download citation
DOI: https://doi.org/10.1007/978-3-662-45824-2_1
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-45823-5
Online ISBN: 978-3-662-45824-2
eBook Packages: Computer ScienceComputer Science (R0)