The HoTT Library: A Formalization of Homotopy Type Theory in Coq

Andrej Bauer, Jason Gross, Peter LeFanu Lumsdaine, Michael Shulman, Matthieu Sozeau, Bas Spitters

Publikation: Bidrag til bog/antologi/rapport/proceedingKonferencebidrag i proceedingsForskningpeer review

38 Citationer (Scopus)

Abstract

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.

OriginalsprogEngelsk
TitelCPP 2017 - Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, co-located with POPL 2017 : CPP 2017
RedaktørerYves Bertot, Viktor Vafeiadis
Antal sider9
UdgivelsesstedNew York, NY, USA
ForlagAssociation for Computing Machinery
Publikationsdato16 jan. 2017
Sider164-172
ISBN (Trykt)978-1-4503-4705-1
ISBN (Elektronisk)9781450347051
DOI
StatusUdgivet - 16 jan. 2017
BegivenhedThe 6th ACM SIGPLAN Conference on Certified Programs and Proofs - Paris, Frankrig
Varighed: 16 jan. 201717 jan. 2017
Konferencens nummer: 6
http://cpp2017.mpi-sws.org/

Konference

KonferenceThe 6th ACM SIGPLAN Conference on Certified Programs and Proofs
Nummer6
Land/OmrådeFrankrig
ByParis
Periode16/01/201717/01/2017
Internetadresse

Emneord

  • Coq, Higher inductive types, Homotopy type theory, Univalent foundations, Universe polymorphism

Fingeraftryk

Dyk ned i forskningsemnerne om 'The HoTT Library: A Formalization of Homotopy Type Theory in Coq'. Sammen danner de et unikt fingeraftryk.

Citationsformater