Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
The HoTT Library: A formalization of homotopy type theory in Coq
Stockholm University, Faculty of Science, Department of Mathematics. (Logik)ORCID iD: 0000-0003-1390-2970
Show others and affiliations
2017 (English)In: Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs / [ed] Yves Bertot, Viktor Vafeiadis, New York, NY, USA: Association for Computing Machinery (ACM), 2017, 164-172 p.Conference paper, Published paper (Refereed)
Abstract [en]

We report on the development of the HoTT library, a formalization of homotopy type theory in the Coq proof assistant. It formalizes most of basic homotopy type theory, including univalence, higher inductive types, and significant amounts of synthetic homotopy theory, as well as category theory and modalities. The library has been used as a basis for several independent developments. We discuss the decisions that led to the design of the library, and we comment on the interaction of homotopy type theory with recently introduced features of Coq, such as universe polymorphism and private inductive types.

Place, publisher, year, edition, pages
New York, NY, USA: Association for Computing Machinery (ACM), 2017. 164-172 p.
National Category
Algebra and Logic
Research subject
Mathematical Logic
Identifiers
URN: urn:nbn:se:su:diva-140144DOI: 10.1145/3018610.3018615ISBN: 978-1-4503-4705-1 (electronic)OAI: oai:DiVA.org:su-140144DiVA: diva2:1077738
Conference
The 6th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP 2017), Paris, France, January 16 - 17, 2017
Available from: 2017-02-28 Created: 2017-02-28 Last updated: 2017-11-08Bibliographically approved

Open Access in DiVA

No full text

Other links

Publisher's full textFree full text

Search in DiVA

By author/editor
LeFanu Lumsdaine, Peter
By organisation
Department of Mathematics
Algebra and Logic

Search outside of DiVA

GoogleGoogle Scholar

doi
isbn
urn-nbn

Altmetric score

doi
isbn
urn-nbn
Total: 14 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf