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.

Site oficial

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