Special Issue on Homotopy Type Theory and Univalent Foundations

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


Two issues of MSCS are dedicated to the collection of papers resulting from this call for papers:

Accepted papers


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):

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


Links to the HoTT/UF Workshops