Arend proof assistant?

[Henry Story]

Hi,

    The Arend proof assistant somehow came to my attention.

Their front page says the following:

[[

Arend

Arend implements a version of homotopy type theory with an interval type, which syntax is similar to cubical type theory. This implies several nice properties of path types and allows for a simple and clean definition of higher inductive types (including recursive ones). To learn more about homotopy features implemented in Arend, see Arend Features.

Arend has a powerful class system, which supports Haskell-style instance inference. Class inheritance can be used to define various hierarchies of (algebraic) structures. For a discussion of the class system, see Arend Features.

]]

https://arend-lang.github.io/about/

Anyone know more about this? Is it a competitor to Coq, Agda, or is it something different?

Henry

[Ben Sherman]

You might be interested in reading this thread on the HoTT mailing list, where it was announced and discussed:

https://groups.google.com/forum/?utm_medium=email&utm_source=footer#!msg/homotopytypetheory/rf6YJB5Omj0/eiKnPDLXFAAJ

--
You received this message because you are subscribed to the Google Groups "HoTT Cafe" group.
To unsubscribe from this group and stop receiving emails from it, send an email to hott-cafe+...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/hott-cafe/c590f540-e10c-4633-aa9c-c6a3e9045158%40googlegroups.com.

[Scott Morrison]

There's topic on Arend on the Lean discussion forum:
https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Arend.20.E2.80.94.20HoTT.20ITP

> To view this discussion on the web visit https://groups.google.com/d/msgid/hott-cafe/A121121E-E168-41D8-BE2C-6D2A23DC90E0%40csail.mit.edu.