An online seminar about the Arend proof assistant

[Andrej Bauer <andre...@andrej.com>]

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