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

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
Sergey Sinchuk
Investigador
Valery Isaev
Valery Isaev
Investigador
Fedor Part
Fedor Part
Investigador
Alexander Kuklev
Alexander Kuklev
Investigador
Tesla Zhang
Tesla Zhang
Investigador