Discussion of Homotopy Type Theory and Univalent Foundations
 help / color / mirror / Atom feed
* [HoTT] New theorem prover Arend is released
@ 2019-08-06 22:16 Валерий Исаев
  2019-08-07 15:01 ` Andrej Bauer
                   ` (2 more replies)
  0 siblings, 3 replies; 20+ messages in thread
From: Валерий Исаев @ 2019-08-06 22:16 UTC (permalink / raw)
  To: Homotopy Type Theory

[-- Attachment #1.1: Type: text/plain, Size: 2913 bytes --]

Arend is a new theorem prover that have been developed at JetBrains 
<https://www.jetbrains.com/> for quite some time. We are proud to announce 
that the first version of the language was released! To learn more about 
Arend, visit our site <https://arend-lang.github.io/>.

Arend is based on a version of homotopy type theory that includes some of 
the cubical features. In particular, it has native higher inductive types, 
including higher inductive-inductive types. It also has other features 
which are necessary for a theorem prover such as universe polymorphism and 
class system. We believe that a theorem prover should be convenient to use. 
That is why we also developed a plugin for IntelliJ IDEA 
<https://www.jetbrains.com/idea/> that turns it into a full-fledged IDE for 
the Arend language. It implements many standard features such as syntax 
highlighting, completion, auto import, and auto formatting. It also has 
some language-specific features such as incremental typechecking and 
various refactoring tools.

To learn more about Arend, you can check out the documentation 
<https://arend-lang.github.io/documentation>. You can also learn a lot from 
studying the standard library <https://github.com/JetBrains/arend-lib>. It 
implements some basic algebra, including localization of rings, and 
homotopy theory, including joins, modalities, and localization of types.

Frequently asked questions (that nobody asked):

   - Why do we need another theorem prover? We believe that a theorem 
   prover should be convenient to use. This means that it should have an IDE 
   comparable to that of mainstream programming languages. That is why we 
   implemented IntelliJ Arend 
   <https://arend-lang.github.io/about/intellij-features>. This also means 
   that the underlying theory should be powerful and expressive. That is why 
   Arend is based on homotopy type theory and has features such as an 
   impredicative type of propositions and a powerful class system.
   - Does Arend have tactics? Not yet, but we are working on it.
   - Does Arend have the canonicity property, i.e. does it evaluate closed 
   expressions to their canonical forms? No, but it computes more terms than 
   ordinary homotopy type theory, which makes it more convenient in many 

If you want to know about language updates, you can follow us on twitter 
<https://twitter.com/ArendLang>. Questions, suggestions, and comments are 
welcome at google groups 

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 HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/9d23061c-4b7a-4d69-9c22-f28261ad3b33%40googlegroups.com.

[-- Attachment #1.2: Type: text/html, Size: 3367 bytes --]

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

end of thread, other threads:[~2019-08-12 17:33 UTC | newest]

Thread overview: 20+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2019-08-06 22:16 [HoTT] New theorem prover Arend is released Валерий Исаев
2019-08-07 15:01 ` Andrej Bauer
2019-08-07 22:13 ` Nicolai Kraus
2019-08-08  9:55   ` Valery Isaev
2019-08-10  9:47     ` Michael Shulman
2019-08-10 12:30       ` Valery Isaev
2019-08-10 12:37       ` Valery Isaev
2019-08-08 12:20 ` Jon Sterling
2019-08-08 12:29   ` Bas Spitters
2019-08-08 14:44     ` Valery Isaev
2019-08-08 15:11       ` Jon Sterling
2019-08-08 15:22         ` Valery Isaev
2019-08-10  9:42           ` Michael Shulman
2019-08-10 12:24             ` Valery Isaev
2019-08-10 23:37               ` Michael Shulman
2019-08-11 10:46                 ` Valery Isaev
2019-08-11 12:39                   ` Michael Shulman
2019-08-11 16:55                     ` Michael Shulman
2019-08-12 14:44                       ` Daniel R. Grayson
2019-08-12 17:32                         ` Michael Shulman

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).