Sergey Sinchuk
Biography
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 SPbSU.
Sergey's research interests include algebraic groups, Ktheory, and type theory.
Academic Advising
Developing and verifying an operational transformation algorithm with C1property for treelike structure by Anton Milenin. Defended at the Department of Informatics, SPbSU in 2014.
Publications
 Journal of Pure and Applied Algebra Volume 220, Issue 2, February 2016
 Interactive Theorem Proving (ITP), 2016

Injective stability for unitary K1, revisited, J. Ktheory, 11 (2013), 233242January 2013

Improved Stability for odddimensional orthogonal group, J. Math. Sci. 199, 3 (2013), 343349January 2013

HoTT and Dependent Types Group Senior researcher
 Dependentlytyped languages
 Verified algorithms and theorem proving with dependent types