リサーチグループ

HoTTと依存型グループ

現在、ホモトピー型理論(HoTT)に基づいて、依存型言語の作成に取り組んでいます。プロジェクトの最終目標は、特定の数学文科の形式化を可能にする最新の型理論に基づいてオンラインの共同証明アシスタントを作成することです。

このプロジェクトは、JetBrainsのあるチームが運用変換(OT)に基づくコラボレーション向けのリアルタイムエディターを開発していた2012年に開始されました。Coq証明アシスタントの助けを借りて、適切なOTアルゴリズムが開発され、検証されましたが、自動化された証明チェックと実際のタスクに適用される正式な検証への関心から、別の研究グループが作られることになりました。2015年、グループは実験的なHoTT言語の開発に切り替えました。

公式サイト

Arendに関する記事(ロシア語):

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

グループメンバー

Sergey Sinchuk
Sergey Sinchuk
研究員
Valery Isaev
Valery Isaev
研究員
Fedor Part
Fedor Part
研究員
Alexander Kuklev
Alexander Kuklev
研究員
Tesla Zhang
Tesla Zhang
研究員