Grupo de investigación

Grupo HoTT y Tipos Dependientes

Actualmente, el grupo trabaja en la creación de un lenguaje tipado dependiente basado en la teoría de tipos de homotopía (HoTT). El objetivo final del proyecto es crear un asistente de prueba colaborativa 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). Con la ayuda del 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