Taking part in the development of Arend plugin for IDEA Archived


Arend is a new theorem prover based on homotopy type theory (see https://arend-lang.github.io/ for more details) developed by Jetbrains Research. One of the key features of Arend is that it is meant to be used on top of Intellij IDEA, for which a dedicated Arend plugin has been developed.
Arend plugin for Intellij IDEA is already rather rich with features, however there is always something that could be added to it. The purpose of the internship is to take part in the development of Arend plugin and to add some new features to it. In course of the internship you will have an opportunity to have a detailed look into the internals of Intellij IDEA and Arend. The former might be very useful if you plan to work on IDEA-based products in the future.


Strong programming skills, knowledge of Intellij IDEA API.
Some degree of familiarity with dependent types and systems of formalized mathematics (Coq, Agda, Arend) will be a plus.


Sergey Sinchuk

Contact details



All locations


JetBrains Research