Special Issue on Homotopy Type Theory and Univalent Foundations

Open call for papers
for a Special Issue of
Mathematical Structures in Computer Science
in association with the workshops on
Homotopy Type Theory and Univalent Foundations
HoTT/UF 2017-2018


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 a lot of 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 Workshop started out as a forum for formalization of mathematics in the univalent style. From the 2017 edition onwards, its scope has been broadened to encompass all aspects of (homotopy) type theory and univalent foundations, in particular (but not exclusively):

The 2017 edition of the workshop is colocated with FSCD'17, taking place in September 2017 in Oxford, UK. The 2018 edition is colocated with FSCD'18 and part of FLoC'18 in July 2018 in Oxford, UK.

Special issue

We are soliciting submissions for a Special Issue of the journal
Mathematical Structures in Computer Science
(Cambridge University Press)
edited in association with the 2017 and 2018 editions of the HoTT/UF workshop. Submission is open to everyone and not limited to workshop participants.

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