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

The HoTT Library: A Formalization of Homotopy Type Theory in Coq. Bauer, A., Gross, J., Lumsdaine, P. L., & others In Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs , of Cpp 2017, pages 164–172, New York, NY, USA, 2017. Association for Computing Machinery.

Paper doi bibtex

@inproceedings{HoTTCoq,
  title        = {{The HoTT Library: A Formalization of Homotopy Type Theory in Coq}},
  author       = {Bauer, Andrej and Gross, Jason and Lumsdaine, Peter LeFanu and others},
  year         = 2017,
  booktitle    = {
    Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and
    Proofs
  },
  location     = {Paris, France},
  publisher    = {Association for Computing Machinery},
  address      = {New York, NY, USA},
  series       = {Cpp 2017},
  pages        = {164–172},
  doi          = {10.1145/3018610.3018615},
  url          = {10.1145/3018610.3018615},
  numpages     = 9,
}

Downloads: 0

{"_id":"TqJmfPhdq4muvBsdP","bibbaseid":"bauer-gross-lumsdaine-others-thehottlibraryaformalizationofhomotopytypetheoryincoq-2017","author_short":["Bauer, A.","Gross, J.","Lumsdaine, P. L.","others"],"bibdata":{"bibtype":"inproceedings","type":"inproceedings","title":"The HoTT Library: A Formalization of Homotopy Type Theory in Coq","author":[{"propositions":[],"lastnames":["Bauer"],"firstnames":["Andrej"],"suffixes":[]},{"propositions":[],"lastnames":["Gross"],"firstnames":["Jason"],"suffixes":[]},{"propositions":[],"lastnames":["Lumsdaine"],"firstnames":["Peter","LeFanu"],"suffixes":[]},{"firstnames":[],"propositions":[],"lastnames":["others"],"suffixes":[]}],"year":"2017","booktitle":"Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs ","location":"Paris, France","publisher":"Association for Computing Machinery","address":"New York, NY, USA","series":"Cpp 2017","pages":"164–172","doi":"10.1145/3018610.3018615","url":"10.1145/3018610.3018615","numpages":"9","bibtex":"@inproceedings{HoTTCoq,\n title = {{The HoTT Library: A Formalization of Homotopy Type Theory in Coq}},\n author = {Bauer, Andrej and Gross, Jason and Lumsdaine, Peter LeFanu and others},\n year = 2017,\n booktitle = {\n Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and\n Proofs\n },\n location = {Paris, France},\n publisher = {Association for Computing Machinery},\n address = {New York, NY, USA},\n series = {Cpp 2017},\n pages = {164–172},\n doi = {10.1145/3018610.3018615},\n url = {10.1145/3018610.3018615},\n numpages = 9,\n}\n\n","author_short":["Bauer, A.","Gross, J.","Lumsdaine, P. L.","others"],"key":"HoTTCoq","id":"HoTTCoq","bibbaseid":"bauer-gross-lumsdaine-others-thehottlibraryaformalizationofhomotopytypetheoryincoq-2017","role":"author","urls":{"Paper":"https://bibbase.org/f/Gnwbc34Hkr4ELKWdc/10.1145/3018610.3018615"},"metadata":{"authorlinks":{}},"html":""},"bibtype":"inproceedings","biburl":"https://bibbase.org/f/Gnwbc34Hkr4ELKWdc/ref.bib","dataSources":["CC7dawDvD4eaYGJSr"],"keywords":[],"search_terms":["hott","library","formalization","homotopy","type","theory","coq","bauer","gross","lumsdaine","others"],"title":"The HoTT Library: A Formalization of Homotopy Type Theory in Coq","year":2017}