HoTT and Dependent Types Lab

Actualmente, el grupo trabaja en la creación de un lenguaje tipado dependiente basado en la teoría de tipos homotópica (HoTT). El objetivo final del proyecto es crear un asistente de prueba colaborativo en línea basado en una teoría de tipos moderna que permita la formalización de ciertas ramas de las matemáticas.

El proyecto comenzó de forma indirecta en 2012, cuando uno de los equipos de JetBrains estaba desarrollando un editor colaborativo en tiempo real basado en la transformación operativa (OT). Gracias al asistente de prueba de Coq, se desarrolló y validó un algoritmo OT adecuado, pero el interés en la comprobación automatizada de pruebas y la verificación formal aplicadas a las tareas del mundo real llevó a la creación de un grupo de investigación independiente. En 2015, el grupo cambió al desarrollo del lenguaje experimental HoTT.

Sitio web oficial

Miembros del grupo

Sergey Sinchuk
Investigador
Valery Isaev
Investigador
Alexander Kuklev
Investigador
Fedor Part
Investigador
Marat Khabibullin
Desarrollador de software