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

Research output: Research - peer-reviewArticle in proceedings

  • Andrej Bauer
    Andrej Bauer
  • Jason Gross
    Jason Gross
  • Peter LeFanu Lumsdaine
    Peter LeFanu Lumsdaine
  • Michael Shulman
    Michael Shulman
  • Matthieu Sozeau
    Matthieu Sozeau
  • Bas Spitters
Original languageEnglish
Title of host publicationProceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs : CPP 2017
Number of pages9
Place of publicationNew York, NY, USA
PublisherAssociation for Computing Machinery
Publication year16 Jan 2017
Pages164-172
ISBN (print)978-1-4503-4705-1
DOIs
StatePublished - 16 Jan 2017
EventThe 6th ACM SIGPLAN Conference on Certified Programs and Proofs - Paris, France
Duration: 16 Jan 201717 Jan 2017
Conference number: 6
http://cpp2017.mpi-sws.org/

Conference

ConferenceThe 6th ACM SIGPLAN Conference on Certified Programs and Proofs
Nummer6
LandFrance
ByParis
Periode16/01/201717/01/2017
Internetadresse
SeriesCPP 2017

See relations at Aarhus University Citationformats

ID: 119288921