연구
HoTT and Dependent Types Lab
본 그룹은 현재 동형 이론(HoTT)을 기반으로 종속 유형 언어를 만드는 작업을 하고 있습니다.이 프로젝트의 최종 목표는 최신 유형 이론을 기초로 온라인 협업 증명 지원 도구를 제작하여 특정 수학 지점을 공식화할 수 있도록 만드는 것입니다.
이 프로젝트는 2012년 JetBrains 팀 중 하나가 운영 혁신(OT)을 기반으로 협업 실시간 에디터를 개발하면서 우연히 시작되었습니다.Coq 증명 지원 도구의 도움으로 적합한 OT 알고리즘을 개발하고 검증한 후에도, 실제 작업에 적용된 자동 증명 검사 및 공식 검증에 대한 관심이 높아짐에 따라 별도의 연구 그룹이 형성되었습니다. 2015년, 이 그룹은 실험적인 HoTT 언어의 개발로 방향을 전환했습니다.
그룹 멤버
Sergey Sinchuk
연구원
연구원
Valery Isaev
연구원
연구원
Fedor Part
연구원
연구원