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