Homotopy type theory is a new branch of mathematics that combines aspects of several different fields in a surprising way. It is based on a recently discovered connection between homotopy the- ory and type theory. Homotopy theory is an outgrowth of algebraic topology and homological algebra, with relationships to higher category theory; while type theory is a branch of mathematical logic and theoretical computer science. Although the connections between the two are currently the focus of intense investigation, it is increasingly clear that they are just the beginning of a subject that will take more time and more hard work to fully understand. It touches on topics as seemingly distant as the homotopy groups of spheres, the algorithms for type checking, and the definition of weak ∞-groupoids.
Publié le : 2013-07-04
Classification:
ACM: F.: Theory of Computation/F.4: MATHEMATICAL LOGIC AND FORMAL LANGUAGES/F.4.1: Mathematical Logic,
ACM: D.: Software/D.3: PROGRAMMING LANGUAGES/D.3.1: Formal Definitions and Theory/D.3.1.0: Semantics,
[INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO],
[MATH.MATH-CT]Mathematics [math]/Category Theory [math.CT],
[MATH.MATH-LO]Mathematics [math]/Logic [math.LO]
@article{hal-00935057,
author = {Aczel, Peter and Ahrens, Benedikt and Altenkirch, Thorsten and Awodey, Steve and Barras, Bruno and Bauer, Andrej and Bertot, Yves and Bezem, Marc and Coquand, Thierry and Finster, Eric and Grayson, Daniel and Herbelin, Hugo and Joyal, Andr\'e and Licata, Dan and Lumsdaine, Peter and Mahboubi, Assia and Martin-L\"of, Per and Melikhov, Sergey and Pelayo, Alvaro and Polonsky, Andrew and Shulman, Michael and Sozeau, Matthieu and Spitters, Bas and Van Den Berg, Benno and Voevodsky, Vladimir and Warren, Michael and Angiuli, Carlo and Bordg, Anthony and Brunerie, Guillaume and Kapulkin, Chris and Rijke, Egbert and Sojakova, Kristina and Avigad, Jeremy and Cohen, Cyril and Constable, Robert and Curien, Pierre-Louis and Dybjer, Peter and Escard\'o, Mart\'\i n and Hou, Kuen-Bang and Gambino, Nicola and Garner, Richard and Gonthier, Georges and Hales, Thomas and Harper, Robert and Hofmann, Martin and Hofstra, Pieter and Koch, Joachim and Kraus, Nicolai and Li, Nuo and Luo, Zhaohui and Nahas, Michael and Palmgren, Erik and Riehl, Emily and Scott, Dana and Scott, Philip and Soloviev, Sergei},
title = {Homotopy Type Theory: Univalent Foundations of Mathematics},
journal = {HAL},
volume = {2013},
number = {0},
year = {2013},
language = {en},
url = {http://dml.mathdoc.fr/item/hal-00935057}
}