Research group

HoTT and Dependent Types Group

The group is currently working on creating a dependently typed language based on homotopy type theory (HoTT). The project's ultimate goal is to create an online collaborative proof assistant based on a modern type theory to allow the formalization of certain branches of mathematics.

The project started incidentally in 2012 when one of the teams at JetBrains was developing a collaborative real-time editor based on operational transformation (OT). With the help of the Coq proof assistant, a suitable OT algorithm was developed and validated, but the interest in automated proof checking and formal verification applied to real-world tasks led to the creation of a separate research group. In 2015, the group switched over to the development of the experimental HoTT language.

Official website: https://arend-lang.github.io/

Articles about Arend (in Russian):

https://habr.com/ru/company/JetBrains-education/blog/469569/

https://habr.com/ru/company/JetBrains-education/blog/470632/

News

More posts

Publications