Forschungsgruppe

Gruppe für HoTT und abhängige Typen

Die Gruppe arbeitet derzeit an der Erstellung einer abhängig typisierten Sprache basierend auf der Homotopietypentheorie (HoTT). Das ultimative Ziel des Projekts ist es, einen kollaborativen Online-Beweisassistenten auf der Grundlage einer modernen Typentheorie zu erstellen, um die Formalisierung bestimmter Zweige der Mathematik zu ermöglichen.

Das Projekt begann zufällig im Jahr 2012, als eines der Teams von JetBrains einen kollaborativen Echtzeit-Editor auf Basis der operativen Transformation (OT) entwickelte. Mit Hilfe des Coq-Beweisassistenten wurde ein geeigneter OT-Algorithmus entwickelt und validiert, aber das Interesse an automatisierter Beweisprüfung und formaler Verifizierung, die auf reale Aufgaben angewendet wurde, führte zur Gründung einer separaten Forschungsgruppe. Im Jahr 2015 wechselte die Gruppe zur Entwicklung der experimentellen HoTT-Sprache.

Offizielle Website

Artikel über Arend (auf Russisch):

https://habr.com/ru/company/JetBrains-education/blog/469569/
https://habr.com/ru/company/JetBrains-education/blog/470632/

Gruppenmitglieder

Sergey Sinchuk
Sergey Sinchuk
Forscher*in
Valery Isaev
Valery Isaev
Forscher*in
Fedor Part
Fedor Part
Forscher*in
Alexander Kuklev
Alexander Kuklev
Forscher*in