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

Publications

August 2021
Tesla Zhang

A Simpler Encoding of Indexed Types

ICFP 21 Workshop on Type-Driven Development 2021

January 2020
Fedor Part and Iddo Tzameret

Resolution with Counting: Dag-Like Lower Bounds and Different Moduli

11th Innovations in Theoretical Computer Science Conference (ITCS) 2020

September 2018
Valery Isaev

Contextually indexed contextual categories

See all publications

Group Members

Sergey Sinchuk
Researcher
Valery Isaev
Researcher
Fedor Part
Researcher