Pesquisa
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.
Publicações
Membros do Grupo
Pesquisador
Pesquisador
Pesquisador