{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,1]],"date-time":"2025-07-01T07:03:51Z","timestamp":1751353431385,"version":"3.41.0"},"reference-count":28,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2015,1,28]],"date-time":"2015-01-28T00:00:00Z","timestamp":1422403200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM SIGLOG News"],"published-print":{"date-parts":[[2015,1,28]]},"abstract":"<jats:p>\n            Homotopy type theory is a recently-developed unification of previously disparate frameworks, which can serve to advance the project of formalizing and mechanizing mathematics. One framework is based on a computational conception of the type of a construction, the other is based on a homotopical conception of the homotopy type of a space. The computational notion of type has its origins in Brouwer's program of intuitionism, and Church's \u03bb-calculus, both of which sought to ground mathematics in computation (one would say \"algorithm\" these days). The homotopical notion comes from Grothendieck's late conception of homotopy types of spaces as represented by \u221e-groupoids [Grothendieck 1983]. The computational perspective was developed most fully by Per Martin-L\u00f6f, leading in particular to his Intuitionistic Theory of Types [Martin-L\u00f6f and Sambin 1984], on which the formal system of homotopy type theory is based. The connection to homotopy theory was first hinted at in the groupoid interpretation of Hofmann and Streicher [Hofmann and Streicher 1994; 1995]. It was then made explicit by several researchers, roughly simultaneously. The connection was clinched by Voevodsky's introduction of the\n            <jats:italic>univalence axiom<\/jats:italic>\n            , which is motivated by the homotopical interpretation, and which relates type equality to homotopy equivalence [Kapulkin et al. 2012; Awodey et al. 2013].\n          <\/jats:p>","DOI":"10.1145\/2728816.2728825","type":"journal-article","created":{"date-parts":[[2020,4,4]],"date-time":"2020-04-04T05:05:40Z","timestamp":1585976740000},"page":"37-44","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["Homotopy type theory"],"prefix":"10.1145","volume":"2","author":[{"given":"Steve","family":"Awodey","sequence":"first","affiliation":[{"name":"Carnegie Mellon University"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Robert","family":"Harper","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2015,1,28]]},"reference":[{"key":"e_1_2_1_1_1","unstructured":"The Agda Proof and Programming System. http:\/\/wiki.portal.chalmers.se\/agda\/pmwiki.php  The Agda Proof and Programming System. http:\/\/wiki.portal.chalmers.se\/agda\/pmwiki.php"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628158"},{"key":"e_1_2_1_3_1","unstructured":"The Automath Archive. http:\/\/www.win.tue.nl\/automath.  The Automath Archive. http:\/\/www.win.tue.nl\/automath."},{"key":"e_1_2_1_4_1","doi-asserted-by":"crossref","unstructured":"S. Awodey A. Pelayo and M. A. Warren. 2013. Voevodsky's univalence uxiom in homotopy type theory. Notices of the Amer. Mathem. Soc. 60(08) (2013) 1164--1167.  S. Awodey A. Pelayo and M. A. Warren. 2013. Voevodsky's univalence uxiom in homotopy type theory. Notices of the Amer. Mathem. Soc. 60(08) (2013) 1164--1167.","DOI":"10.1090\/noti1043"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0305004108001783"},{"key":"e_1_2_1_6_1","volume-title":"A model of type theory in cubical sets. (March","author":"Bezem Marc","year":"2014","unstructured":"Marc Bezem , Thierry Coquand , and Simon Huber . 2014. A model of type theory in cubical sets. (March 2014 ). ( Unpublished Manuscript) . Marc Bezem, Thierry Coquand, and Simon Huber. 2014. A model of type theory in cubical sets. (March 2014). (Unpublished Manuscript)."},{"key":"e_1_2_1_7_1","volume-title":"Constructive Analysis. Number 279 in Grundlehren der mathematischen Wissenschaften: A Series of Comprehensive Studies in Mathematics","author":"Bishop Errett","year":"1967","unstructured":"Errett Bishop and Douglas Bridges . 1985. Constructive Analysis. Number 279 in Grundlehren der mathematischen Wissenschaften: A Series of Comprehensive Studies in Mathematics . Springer . (Revision of first edition by Bishop published in 1967 .). Errett Bishop and Douglas Bridges. 1985. Constructive Analysis. Number 279 in Grundlehren der mathematischen Wissenschaften: A Series of Comprehensive Studies in Mathematics. Springer. (Revision of first edition by Bishop published in 1967.)."},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.2307\/2266170"},{"key":"e_1_2_1_9_1","unstructured":"Robert L. Constable etal 1985. Implementing Mathematics with the NuPRL Proof Development System. Prentice Hall.   Robert L. Constable et al. 1985. Implementing Mathematics with the NuPRL Proof Development System. Prentice Hall."},{"key":"e_1_2_1_10_1","unstructured":"The Coq Proof Assistant. http:\/\/coq.inria.fr.  The Coq Proof Assistant. http:\/\/coq.inria.fr."},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2008.08.030"},{"key":"e_1_2_1_12_1","unstructured":"A. Grothendieck. 1983. Pursuing stacks. (1983). Unpublished manuscript.  A. Grothendieck. 1983. Pursuing stacks. (1983). Unpublished manuscript."},{"key":"e_1_2_1_13_1","unstructured":"Martin Hofmann and Thomas Streicher. 1994. The Groupoid Model Refutes Uniqueness of Identity Proofs. In LICS. 208--212.  Martin Hofmann and Thomas Streicher. 1994. The Groupoid Model Refutes Uniqueness of Identity Proofs. In LICS. 208--212."},{"key":"e_1_2_1_14_1","unstructured":"M. Hofmann and T. Streicher. 1995. The groupoid model of type theory. In Twenty-five years of constructive type theory G. Sambin and J. Smith (Eds.). Oxford University Press.  M. Hofmann and T. Streicher. 1995. The groupoid model of type theory. In Twenty-five years of constructive type theory G. Sambin and J. Smith (Eds.). Oxford University Press."},{"key":"e_1_2_1_15_1","unstructured":"The HOL System. http:\/\/www.cl.cam.ac.uk\/research\/hvg\/HOL.  The HOL System. http:\/\/www.cl.cam.ac.uk\/research\/hvg\/HOL."},{"key":"e_1_2_1_16_1","unstructured":"The HOL Light Theorem Prover. http:\/\/www.cl.cam.ac.uk\/~jrh13\/hol-light\/index.html.  The HOL Light Theorem Prover. http:\/\/www.cl.cam.ac.uk\/~jrh13\/hol-light\/index.html."},{"volume-title":"To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism","author":"Howard W. A.","key":"e_1_2_1_17_1","unstructured":"W. A. Howard . 1980. The formulae-as-types notion of construction . In To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism . Academic Press , 479--491. W. A. Howard. 1980. The formulae-as-types notion of construction. In To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism. Academic Press, 479--491."},{"key":"e_1_2_1_18_1","unstructured":"C. Kapulkin P. LeFanu Lumsdaine and V. Voevodsky. 2012. Univalence in Simplicial Sets. arXiv 1203.2553 (2012).  C. Kapulkin P. LeFanu Lumsdaine and V. Voevodsky. 2012. Univalence in Simplicial Sets. arXiv 1203.2553 (2012)."},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-03545-1_1"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2603088.2603153"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2013.28"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02273-9_14"},{"volume-title":"Intuitionistic type theory","author":"Martin-L\u00f6f Per","key":"e_1_2_1_23_1","unstructured":"Per Martin-L\u00f6f and Giovanni Sambin . 1984. Intuitionistic type theory . Vol. 17 . Bibliopolis Naples . Per Martin-L\u00f6f and Giovanni Sambin. 1984. Intuitionistic type theory. Vol. 17. Bibliopolis Naples."},{"key":"e_1_2_1_24_1","unstructured":"The NuPRL Proof Development System. http:\/\/nuprl.org.  The NuPRL Proof Development System. http:\/\/nuprl.org."},{"key":"e_1_2_1_25_1","unstructured":"T. Streicher. 2006. Identity types vs. weak omega-groupoids: some ideas some problems. (2006). Talk given in Uppsala at the meeting on \"Identity Types: Topological and Categorical Structure\".  T. Streicher. 2006. Identity types vs. weak omega-groupoids: some ideas some problems. (2006). Talk given in Uppsala at the meeting on \"Identity Types: Topological and Categorical Structure\"."},{"key":"e_1_2_1_26_1","unstructured":"The Univalent Foundations Program. 2013. Homotopy Type Theory: Univalent Foundations of Mathematics. http:\/\/homotopytypetheory.org\/book Institute for Advanced Study.  The Univalent Foundations Program. 2013. Homotopy Type Theory: Univalent Foundations of Mathematics. http:\/\/homotopytypetheory.org\/book Institute for Advanced Study."},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1112\/plms\/pdq026"},{"key":"e_1_2_1_28_1","unstructured":"V. Voevodsky. 2006. A very short note on the homotopy \u03bb-calculus. (2006). Unpublished note.  V. Voevodsky. 2006. A very short note on the homotopy \u03bb-calculus. (2006). Unpublished note."}],"container-title":["ACM SIGLOG News"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2728816.2728825","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2728816.2728825","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T06:16:33Z","timestamp":1750227393000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2728816.2728825"}},"subtitle":["unified foundations of mathematics and computation"],"short-title":[],"issued":{"date-parts":[[2015,1,28]]},"references-count":28,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2015,1,28]]}},"alternative-id":["10.1145\/2728816.2728825"],"URL":"https:\/\/doi.org\/10.1145\/2728816.2728825","relation":{},"ISSN":["2372-3491"],"issn-type":[{"type":"electronic","value":"2372-3491"}],"subject":[],"published":{"date-parts":[[2015,1,28]]},"assertion":[{"value":"2015-01-28","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}