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.
Artículos sobre Arend (en ruso):
https://habr.com/ru/company/JetBrains-education/blog/469569/
https://habr.com/ru/company/JetBrains-education/blog/470632/
Miembros del grupo

Sergey Sinchuk
Investigador

Valery Isaev
Investigador

Fedor Part
Investigador

Alexander Kuklev
Investigador

Marat Khabibullin
Desarrollador de software