Special Issue on Homotopy Type Theory and Univalent Foundations

Publications

• Volume 31 - Issue 1 - January 2021
• Volume 31 - Issue 4 - April 2021

Accepted papers

• Carlo Angiuli, Guillaume Brunerie, Thierry Coquand, Robert Harper, Kuen-Bang Hou (Favonia), and Daniel R. Licata: Syntax and models of Cartesian cubical type theory
  Link to the published version
• Auke B. Booij: Extensional constructive real analysis via locators
  Link to the published version
• Simon Boulier and Nicolas Tabareau: Model structure on the universe of all types in interval type theory
  Link to the published version
• Felix Cherubini and Egbert Rijke: Modal descent
  Link to the published version
• Martín Hötzel Escardó: Injective types in univalent mathematics
  Link to the published version
• Cesare Gallozzi: Homotopy type-theoretic interpretations of constructive set theories
  Link to the published version
• Valery Isaev: Indexed type theories
  Link to the published version
• Luis Scoccola: Nilpotent types and fracture squares in homotopy type theory
  Link to the published version

Background

Homotopy Type Theory is a young research area combining ideas from several established fields: the use of dependent type theory as a foundation for mathematics, inspired by ideas and tools from abstract homotopy theory and higher category theory. Univalent Foundations are foundations of mathematics based on the homotopical interpretation of type theory. These ideas have led to many interesting developments, from the study of syntax and semantics of type theories to practical formalizations in proof assistants based on univalent type theory.

The HoTT/UF workshops, co-located with FSCD since 2016, started out as a forum for formalization of mathematics in a univalent setting. From the 2017 edition and onwards, its scope has been broadened to encompass all aspects of Homotopy Type Theory and Univalent Foundations, in particular (but not exclusively):

• semantics of (univalent) type theory,
• computational content of the univalence axiom,
• syntax and semantics of higher inductive types,
• synthetic homotopy theory, and
• formalization of mathematics and computer science in Homotopy Type Theory and Univalent Foundations.

Special issue

Submission is open from now and submissions will be reviewed on a rolling basis, as soon as they are received. Accepted papers will be published on the MSCS website via 'FirstView' and will be citeable through a DOI shortly after acceptance - before the completion of the whole journal issue (expected end of 2019). Submission will be closed on December 31, 2018.

Guest editors

• Benedikt Ahrens (B.Ahrens@cs.bham.ac.uk)
• Simon Huber (simonhu@chalmers.se)
• Anders Mörtberg (andersmortberg@gmail.com)

Details

• Papers must be submitted in PDF format through the MSCS ScholarOne submission system. Please choose the special issue "Homotopy Type Theory and Univalent Foundations" from the drop down menu on the submissions page. Please also choose Pierre-Louis Curien as editor-in-chief for the submission.
• Detailed submission instructions and MSCS guidelines to which the final versions of accepted papers need to follow can be found here.
• The LaTeX template can be found here.
• Authors have the option to attach to their submission a zip or tgz file containing code (formalized proofs or programs). Publication of such code together with the article can be arranged if desired by the authors.
• Submission will be closed on December 31, 2018. (However, as mentioned above, submissions will be handled as soon as they are received.)
• We recommend submissions have no more than 40 pages. For longer articles we ask authors to provide a justification for exceeding this limit.
• If you have any questions or remarks, please send an email to the guest editors.

Links to the HoTT/UF Workshops

• HoTT/UF 2018, Oxford. Co-located with FSCD 2018 and part of FLoC 2018.
• HoTT/UF 2017, Oxford. Co-located with FSCD 2017.
• HoTT/UF 2016, Porto. Co-located with FSCD 2016.
• HoTT/UF 2015, Warsaw. Co-located with RDP/TRA/TLCA 2015.