Investigación
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.
Publicaciones
Miembros del grupo
Investigador
Investigador
Investigador