Discussion of Homotopy Type Theory and Univalent Foundations
 help / color / Atom feed
From: Anders Mortberg <andersmortberg@gmail.com>
To: Homotopy Type Theory <homotopytypetheory@googlegroups.com>
Subject: [HoTT] Call for Contributions: ICMS 2020 Session on "Univalent Mathematics: Theory and Implementation"
Date: Wed, 12 Feb 2020 00:03:17 +0100
Message-ID: <CAMWCpp=T+ixw60EvtrHuAqLweARJzdc9HjAQBrw0+x-5kPeSaw@mail.gmail.com> (raw)

The International Congress on Mathematical Software 2020 (ICMS 2020)
will be held in Braunschweig, Germany on July 13-16, 2020:


There will be a session on "Univalent Mathematics: Theory and
Implementation" at this event:


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.

                 reply index

Thread overview: [no followups] expand[flat|nested]  mbox.gz  Atom feed

Reply instructions:

You may reply publicly to this message via plain-text email
using any one of the following methods:

* Save the following mbox file, import it into your mail client,
  and reply-to-all from there: mbox

  Avoid top-posting and favor interleaved quoting:

* Reply using the --to, --cc, and --in-reply-to
  switches of git-send-email(1):

  git send-email \
    --in-reply-to='CAMWCpp=T+ixw60EvtrHuAqLweARJzdc9HjAQBrw0+x-5kPeSaw@mail.gmail.com' \
    --to=andersmortberg@gmail.com \
    --cc=homotopytypetheory@googlegroups.com \


* If your mail client supports setting the In-Reply-To header
  via mailto: links, try the mailto: link

Discussion of Homotopy Type Theory and Univalent Foundations

Archives are clonable: git clone --mirror http://inbox.vuxu.org/hott

Example config snippet for mirrors

Newsgroup available over NNTP:

AGPL code for this site: git clone https://public-inbox.org/public-inbox.git