Discussion of Homotopy Type Theory and Univalent Foundations
 help / color / 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
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

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

* Re: An online seminar about the Arend proof assistant
  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
  0 siblings, 1 reply; 5+ messages in thread
From: Andrej Bauer @ 2020-04-28 15:30 UTC (permalink / raw)
  To: HomotopyT...@googlegroups.com

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

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

* Re: [HoTT] Re: An online seminar about the Arend proof assistant
  2020-04-28 15:30 ` Andrej Bauer
@ 2020-05-01 13:41   ` Stefan Monnier
  2020-05-01 13:42     ` Anja Petković
  2020-05-01 13:42     ` Danel Ahman
  0 siblings, 2 replies; 5+ messages in thread
From: Stefan Monnier @ 2020-05-01 13:41 UTC (permalink / raw)
  To: Andrej Bauer; +Cc: HomotopyT...@googlegroups.com

> 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


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

* Re: [HoTT] Re: An online seminar about the Arend proof assistant
  2020-05-01 13:41   ` [HoTT] " Stefan Monnier
@ 2020-05-01 13:42     ` Anja Petković
  2020-05-01 13:42     ` Danel Ahman
  1 sibling, 0 replies; 5+ messages in thread
From: Anja Petković @ 2020-05-01 13:42 UTC (permalink / raw)
  To: Stefan Monnier; +Cc: Andrej Bauer, HomotopyT...@googlegroups.com


[-- Attachment #1: Type: text/plain, Size: 870 bytes --]

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

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

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

[-- Attachment #2: Type: text/html, Size: 1550 bytes --]

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

* Re: [HoTT] Re: An online seminar about the Arend proof assistant
  2020-05-01 13:41   ` [HoTT] " Stefan Monnier
  2020-05-01 13:42     ` Anja Petković
@ 2020-05-01 13:42     ` Danel Ahman
  1 sibling, 0 replies; 5+ messages in thread
From: Danel Ahman @ 2020-05-01 13:42 UTC (permalink / raw)
  To: Stefan Monnier; +Cc: HomotopyT...@googlegroups.com


[-- Attachment #1: Type: text/plain, Size: 881 bytes --]

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

Danel

> On 1 May 2020, at 15:41, Stefan Monnier <mon...@iro.umontreal.ca> wrote:
> 
>> 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
> 
> -- 
> 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 HomotopyT...@googlegroups.com.
> To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/jwv4kszydtr.fsf-monnier%2BInbox%40gnu.org.


[-- Attachment #2: Type: text/html, Size: 1845 bytes --]

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

end of thread, back to index

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

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