[3] He is the author of the free online book Programs and Proofs: Mechanizing Mathematics with Dependent Types, Lecture notes with exercises, which introduce the basic concepts of mechanized reasoning and interactive theorem proving using Coq.
Sergey holds a joint appointment at Yale-NUS College[4] and is a lead language designer at Zilliqa.
[5] He received his MSc in 2008 at Saint Petersburg State University and his PhD in 2012 at KU Leuven.
Before joining NUS, he was a postdoctoral researcher at IMDEA Software Institute and on the faculty of University College London.
Prior to starting an academic career, he worked as a software developer at JetBrains.