Arend

Arend is a theorem prover based on Homotopy Type Theory. It natively supports higher inductive types and a version of cubical syntax. IntelliJ Arend is a plugin for IntelliJ IDEA that turns it into a full-fledged IDE for the Arend language.

Arend Features IntelliJ Arend Features

Recent Posts

Arend 1.1.0 released

Arend now has proof irrelevant universe of proposition and the plugin can run the typechecker automatically in background. Language updates: \Prop is now...

Arend 1.0.0 released

The first version of Arend is released! It implements the following features: Path types based on the interval type. Higher inductive types, including ...