Discussion of Homotopy Type Theory and Univalent Foundations
 help / color / mirror / Atom feed
* An online seminar about the Arend proof assistant
@ 2020-04-27 23:13 Andrej Bauer
  2020-04-28 15:30 ` Andrej Bauer
  0 siblings, 1 reply; 5+ messages in thread
From: Andrej Bauer @ 2020-04-27 23:13 UTC (permalink / raw)
  To: HomotopyT...@googlegroups.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

The seminar is the first one in a series of seminars about proof
assistants, see my blog post

With kind regards,


^ permalink raw reply	[flat|nested] 5+ messages in thread

end of thread, other threads:[~2020-05-01 13:42 UTC | newest]

Thread overview: 5+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2020-04-27 23:13 An online seminar about the Arend proof assistant Andrej Bauer
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

This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).