28 College Avenue West
#01-501, Singapore 138533
||#RC3-01-03E, Cendana College|
|Office Phone:||+65 6516 1903|
|Availability:||Calendar (it takes a while to load)|
I do research in programming language theory, including, but not limited to types, semantics, software verification, and program synthesis. Lately, I have been mostly focusing on developing sound and scalable methodologies for building provably correct concurrent and distributed systems (with applications to blockchains and smart contracts). I also designed and co-developed Scilla, a programming language for safe and secure smart contracts. For my work, I write a lot of mechanised proofs in Coq, as well as functional code in Scala, OCaml, and Haskell.
Since November 2018, I am a tenure-track Associate Professor at Yale-NUS College (Singapore), holding a joint appointment with NUS School of Computing. From November 2015 till October 2018, I was a faculty at the Department of Computer Science of University College London. Prior to joining UCL, from December 2012 to October 2015, I was a postdoc at IMDEA Software Institute. From November 2008 to November 2012, I was a research assistant in the CS Department of KU Leuven, where I obtained my PhD. During my doctoral studies I was a visiting PhD fellow in the Department of Computer Science of Aarhus University and a research intern in the PPT group at MSR Cambridge. I got my MSc degree in Mathematics and CS in 2008 from Dept. of Mathematics and Mechanics of Saint Petersburg State University. Before joining academia I worked as a software developer at JetBrains.
Curriculum Vitae: [PDF]
|Nov 28||A work-in-progress report on probabilistic verification of security properties of blockchain protocols will be presented by Kiran Gopinathan at CoqPL 2019.|
|Nov 12||Gave a talk entitled What We Talk about When We Talk about Formally Verified Systems at Blockchain and Cybersecurity Workshop 2018 hosted by National University of Singapore.|
|Nov 5||A paper on practical programming with distributed protocos (with Kristoffer Just Andersen), will appear at PADL 2019.|
|Oct 9||Two papers accepted at POPL 2019: on program synthesis via Separation Logic (with Nadia Polikarpova), and on proving no-false-positives for unsound static race detectors (with Nikos Gorogiannis and Peter O'Hearn).|
|Sep 8||Looking forward to visit Dominique Devriese at KU Leuven on September 19 and give a talk on program synthesis with Separation Logic.|
|Aug 29||On September 3-5, I will be visiting Éric Tanter and the research group of Cătălin Hriţcu at Inria Paris.|
|Aug 23||Our paper on Finding the Greedy, Prodigal, and Suicidal Contracts at Scale, with Ivica Nikolić, Aashish Kolluri, Prateek Saxena and Aquinas Hobor, got accepted to ACSAC 2018.|
|Aug 15||I am looking forward to visit Sukyoung Ryu and Hongseok Yang and their groups at KAIST in Daejeon on August 23-28.|
|Aug 14||On August 21, I will be giving a series of lectures on implementation and verification of distributed systems and their applications at SIGPL Summer School 2018 in Seoul (yes, that page is entirely in Korean, but, even if you are, just like me, not a Korean speaker, you can still try to identify the titles of my talks there).|
|Aug 6||Scilla, a strongly typed intermediate language for smart contracts developed by Zilliqa, is now open-sourced: here's the repository, and here's a new shiny web page with tutorials and documentation. Contributions are welcome!|
|Jul 20||Got promoted to an Associate Professor of Computer Science at UCL, effective 1st October 2018.|
|Jul 6||Our paper on RacerD, an industrial-scale compositional static race detector, developed at Facebook, with Sam Blackshear, Nikos Gorogiannis, and Peter O'Hearn, is conditionally accepted at OOPSLA 2018. Here's the preprint.|
|Jun 6||Amrit Kumar and I gave a long interview to Epicenter about Scilla and formal verification of smart contracts.|
|Jun 1||Next year, I will be serving on the Programme Committees of PLDI 2019 and OOPSLA 2019. Looking forward for reading lots of (your) exciting submissions on types, logics, compilers, verification, and program synthesis!|
I am a also a creator of the La Clojure plugin for IntelliJ IDEA. It is no longer maintained, but its sources are available on GitHub.
Check my GitHub profile for my other projects.
Over the years, I have been very lucky to work on joint research projects with some great people:
I am married to CG artist Lilia Anisimova.
I am on Twitter as @ilyasergey.
My Erdős number is here (you can view this MathSciNet page from your university network). Last time I checked it was 4.
The photo above is couresy of Elena Alhimovich. Here is my "official" photo,
suitable for appropriate occasions. Yet another picture of mine by Jorge Cham, for I have contributed to the
PHD Movie 2 on
While living in Madrid, I enjoyed its inimitable atmosphere and delicious food. For the latter, this Maribel's Dining Guide to Madrid (kindly provided by Aleks Nanevski) always came in handy.