研究小组

HoTT 和依赖类型组

该小组目前正在致力于创建基于同论类型论 (HoTT) 的依赖性类型语言。这个项目的最终目标是创建一个基于现代类型理论的在线协作证明助手,以实现数学某些分支的正规化。

这个项目是在 2012 年偶然开始的,当时 JetBrains 的一个团队正在开发一个基于操作转换(OT)的协作式实时编辑器。在 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
研究员