An online seminar about the Arend proof assistant

[Andrej Bauer]

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

[Andrej Bauer]

Dear all,

I apologize for messing up the time zones. The correct time is 18:00
as measured currently in Ljubljana, which is Central European Summer
Time (UCT+2).

Title: Arend proof assistant
Time: Thursday, April 30, 2020 from 18:00 to 19:00 (Central European
Summer Time, UTC+2)

Location: online at Zoom ID 965 4439 5816 (https://zoom.us/j/96544395816)
Speaker: Valery Isaev (JetBrains research)

If you forwarded the talk announcement anywhere, please kindly forward
the time clarification as well.

With kind regards,

Andrej

[Stefan Monnier]

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

I managed to miss it. Any chance it was recorded?


Stefan

[Anja Petković]

Indeed it was: https://vimeo.com/413726748

V pet., 1. maj 2020 15:41 je oseba Stefan Monnier <mon...@iro.umontreal.ca> napisala:

--
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 HomotopyTypeThe...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/jwv4kszydtr.fsf-monnier%2BInbox%40gnu.org.

[Danel Ahman]

Yes it was, see https://vimeo.com/413726748

Danel