Documentation

• For the installation instructions, see Getting Started.
• Language Reference contains a description of the Arend language.
• Tutorial contains a more gentle introduction to the Arend language.
• Libraries describes how to manage Arend libraries.
• Standard Extensions explains the language extensions implemented in the standard library.
• To learn how to write proofs with IntelliJ Arend IDE, see Interactive Theorem Proving with IntelliJ Arend.

Papers

• Theorem prover Arend by Fedor Part, Valery Isaev, and Sergey Sinchuk is a self-contained exposition of the prover: the type theory it is based on, the features of the language, the IntelliJ Arend plugin and the command-line interface, and the contents of arend-lib.
• (Co)condition hits the Path by Tesla Zhang and Valery Isaev introduces conditions and coconditions, extensions of inductive types and records that generalize the cubical syntax of higher inductive types and the cubical path type respectively.
• A Constructive Approach to Complete Spaces by Valery Isaev introduces cover spaces, a constructive generalization of metric and uniform spaces, and studies their reflective subcategory of complete spaces and its relation to locales.

Forums

• Google Groups
• Telegram
• Gitter
• Zulip

We welcome questions about the Arend language, the IntelliJ Arend plugin, the libraries, and this website there.

Videos

• Introductory talk about the Arend language, which covers basic language and IDE features.