HoTT and Dependent Types Lab

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

Group Members

Sergey Sinchuk
Valery Isaev
Alexander Kuklev
Fedor Part
Marat Khabibullin
Software Developer