HoTT and Dependent Types Lab

No momento, o grupo está trabalhando na criação de uma linguagem tipada de forma dependente, com base na teoria dos tipos de homotopia (HoTT). O objetivo final do projeto é criar um assistente de prova colaborativa on-line baseado em uma teoria moderna de tipos, 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 do Coq, foi desenvolvido e validado um algoritmo de OT adequado, mas o interesse na verificação automatizada de provas e na 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 de HoTT.

Site oficial

Membros do Grupo

Sergey Sinchuk
Pesquisador
Valery Isaev
Pesquisador
Alexander Kuklev
Pesquisador
Fedor Part
Pesquisador
Marat Khabibullin
Desenvolvedor de Software