Forschung
HoTT and Dependent Types Lab
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.
Publikationen
Gruppenmitglieder
Forscher
Forscher
Forscher