リサーチ
HoTT and Dependent Types Lab
現在、ホモトピー型理論 (HoTT) に基づいて、依存型言語の作成に取り組んでいます。プロジェクトの最終目標は、特定の数学文科の形式化を可能にする最新の型理論に基づいてオンラインの共同証明アシスタントを作成することです。
このプロジェクトは、JetBrainsのあるチームが運用変換 (OT) に基づくコラボレーション向けのリアルタイムエディターを開発していた2012年に開始されました。Coq 証明アシスタントの助けを借りて、適切な OT アルゴリズムが開発され、検証されましたが、自動化された証明チェックと実際のタスクに適用される正式な検証への関心から、別の研究グループが作られることになりました。2015年、グループは実験的な HoTT 言語の開発に切り替えました。
出版物
グループメンバー
Sergey Sinchuk
研究員
研究員
Valery Isaev
研究員
研究員
Fedor Part
研究員
研究員