[HoTT] Call for Contributions: ICMS 2020 Session on "Univalent Mathematics: Theory and Implementation"

[HoTT] Call for Contributions: ICMS 2020 Session on "Univalent Mathematics: Theory and Implementation"

[Anders Mortberg]

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.