Graduated in 2010 from the St. Petersburg State University, Mathematics and Mechanics Faculty, Algebra Department. Defended his Ph.D. thesis in 2013. Joined the HoTT Group project in spring 2012. Apart from JetBrains, also works at Chebyshev Laboratory at SPbU.
Sergey's research interests include algebraic groups, K-theory, and type theory.
Developing and verifying an operational transformation algorithm with C1-property for tree-like structure by Anton Milenin. Defended at the Department of Informatics, SPbU in 2014.
HoTT and Dependent Types Group Senior researcher
- Dependently-typed languages
- Verified algorithms and theorem proving with dependent types