Discussion of Homotopy Type Theory and Univalent Foundations
 help / color / Atom feed
From: Andrej Bauer <andre...@andrej.com>
To: "HomotopyT...@googlegroups.com" <homotopyt...@googlegroups.com>
Subject: An online seminar about the Arend proof assistant
Date: Tue, 28 Apr 2020 01:13:07 +0200
Message-ID: <CAB0nkh2b5okvkYdtURm0pTGd_sMtz8fwCELj=RQV22xK3vh5ew@mail.gmail.com> (raw)

Dear all,

I would like to draw your attention to an online seminar about the
Arend proof assistant, which will be given by Valery Isaev.

Title: Arend proof assistant
Time: Thursday, April 30, 2020 from 19:00 to 20:00 (Central European Time)
Location: online at Zoom ID 965 4439 5816 (https://zoom.us/j/96544395816)
Speaker: Valery Isaev (JetBrains research)

Abstract: I will discuss Arend, a proof assistant developed at
JetBrains Research. The aim of Arend is to provide a powerful system
for formalization results in homotopy type theory and in ordinary
mathematics. To achieve the latter goal, we prove a flexible class
system with subtyping, universe polymorphism with a powerful level
inference mechanism, quotient sets with convenient pattern matching
principles for them. We also recently implemented a tactic framework
which can be used to automate routine proofs and implement various
EDSLs. Homotopic features of Arend include built-in universes of
finite homotopy level, higher inductive types, univalence, and path
types in the style of cubical type theories. I will talk about these
features and also about our plans to implement language extensions
that can be used to simplify reasoning about various higher
structures.

The seminar is the first one in a series of seminars about proof
assistants, see my blog post
http://math.andrej.com/2020/04/28/every-theorem-prover/

With kind regards,

Andrej

             reply index

Thread overview: 5+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2020-04-27 23:13 Andrej Bauer [this message]
2020-04-28 15:30 ` Andrej Bauer
2020-05-01 13:41   ` [HoTT] " Stefan Monnier
2020-05-01 13:42     ` Anja Petković
2020-05-01 13:42     ` Danel Ahman

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:
  https://en.wikipedia.org/wiki/Posting_style#Interleaved_style

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

  git send-email \
    --in-reply-to='CAB0nkh2b5okvkYdtURm0pTGd_sMtz8fwCELj=RQV22xK3vh5ew@mail.gmail.com' \
    --to="andre..."@andrej.com \
    --cc="homotopyt..."@googlegroups.com \
    /path/to/YOUR_REPLY

  https://kernel.org/pub/software/scm/git/docs/git-send-email.html

* 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:
	nntp://inbox.vuxu.org/vuxu.archive.hott


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