Arend is a new theorem prover that have been developed at
JetBrains 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.
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 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. You can also learn a lot from studying the
standard library. 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. 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 aspects.
If you want to know about language updates, you can follow us on
twitter. Questions, suggestions, and comments are welcome at
google groups.