Grupo de pesquisa
HoTT e Grupo de Tipos Dependentes
O grupo está atualmente trabalhando na criação de uma linguagem com tipo dependente baseada na teoria do tipo de homotopia (HoTT). O objetivo final do projeto é criar um assistente de prova colaborativa online baseado em uma teoria de tipo moderno para permitir a formalização de certos ramos da matemática.
O projeto começou incidentalmente em 2012, quando uma das equipes da JetBrains estava desenvolvendo um editor colaborativo em tempo real baseado em transformação operacional (OT). Com a ajuda do assistente de prova Coq, um algoritmo de OT adequado foi desenvolvido e validado, mas o interesse em verificação automatizada de provas e verificação formal aplicadas a tarefas do mundo real levou à criação de um grupo de pesquisa separado. Em 2015, o grupo passou para o desenvolvimento da linguagem experimental HoTT.
Artigos sobre o Arend (em russo):
https://habr.com/ru/company/JetBrains-education/blog/469569/
https://habr.com/ru/company/JetBrains-education/blog/470632/
Membros do Grupo

Sergey Sinchuk
Pesquisador

Valery Isaev
Pesquisador

Fedor Part
Pesquisador

Alexander Kuklev
Pesquisador

Marat Khabibullin
Desenvolvedor de Software