The International Congress on Mathematical Software 2020 (ICMS 2020) will be held in Braunschweig, Germany on July 13-16, 2020: http://www.iaa.tu-bs.de/AppliedAlgebra/ICMS2020/ICMS2020.html There will be a session on "Univalent Mathematics: Theory and Implementation" at this event: https://univalent-math.github.io/ Title and short abstract submission deadline: February 23, 2020. # Aim and scope of session Homotopy Type Theory/Univalent Foundations (HoTT/UF) is a new type-theoretic foundation for mathematics based on novel connections between dependent type theory and homotopy theory. Recently there has been much interest in the constructive meaning of the univalence axiom, which has led to multiple new cubical proof assistants natively supporting univalence and higher inductive types. These proof assistants allow for the convenient formalization of abstract mathematics, especially synthetic homotopy theory, and also provide several features previously missing from many type-theoretic proof assistants, such as function extensionality and quotients. The goal of this session is to gather experts on HoTT/UF and its implementation to present recent results and discuss future directions, including but not limited to: o Implementation of proof assistants for univalent mathematics o Cubical type theories and their metatheory o Formalization of univalent mathematics # Submissions Most talks at the session will be invited, but there is room for a few contributed talks. If you would like to speak at the session please send us an email with title and a short plain text abstract by February 23, 2020. If accepted, you will have the option to submit an extended abstract (4-8 pages) by March 16, 2020. The accepted extended abstracts will then be published in the Springer Lecture Notes in Computer Science (LNCS) series. # Deadlines * Title and short abstract deadline (strict): February 23, 2020. * Notification: February 24, 2020. * Extended abstract deadline (optional): March 16, 2020. * Notification: April 27, 2020. * Final version of accepted extended abstracts: May 9, 2020. # Session organizers * Carlo Angiuli (Carnegie Mellon University) - cangiuli@cs.cmu.edu * Anders Mörtberg (Stockholm University) - anders.mortberg@math.su.se -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAMWCpp%3DT%2Bixw60EvtrHuAqLweARJzdc9HjAQBrw0%2Bx-5kPeSaw%40mail.gmail.com.