연구 그룹

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
연구원