HoTT and Dependent Types Lab

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

这个项目是在 2012 年偶然开始的,当时 JetBrains 的一个团队正在开发一个基于操作转换(OT)的协作式实时编辑器。在 Coq 校对助手的帮助下,开发和验证了合适的 OT 算法,但由于对应用于现实世界任务的自动证明检查和形式化验证感兴趣,于是成立了一个单独的研究小组。 2015 年,该小组转向开发实验性的 HoTT 语言。

官方网站

小组成员

Sergey Sinchuk
研究员
Valery Isaev
研究员
Alexander Kuklev
研究员
Fedor Part
研究员
Marat Khabibullin
软件开发者