I do research in programming languages, software verification, and program synthesis. Lately, I have been focusing on developing sound and scalable methodologies for building provably correct concurrent and distributed systems. I am the recipient of the AITO Dahl-Nygaard Junior Prize 2019. I designed and co-developed Scilla, a programming language for safe smart contracts, used by Zilliqa. I organised the ICFP Programming Contest 2019. In the past, I contributed to Facebook Infer and Glasgow Haskell Compiler. Very long time ago, I used to work on Scala and Clojure support in IntelliJ IDEA.
Before moving to Singapore, I was a faculty at University College London in 2015-2018. Prior to that, I was a postdoc at IMDEA Software Institute. I hold a PhD in Computer Science from KU Leuven, and an MSc in mathematics from St Petersburg University. Before joining academia I worked as a software engineer at JetBrains.
Yale-NUS College, 28 College Avenue West
#01-501, Singapore 138533
||#RC3-01-03E, Cendana (Yale-NUS), COM2-02-42 (NUS SoC)|
|Office Phone:||+65 6516 1903|
|Office Hours:||Wednesdays, 5:00-7:00pm (Spring term 2021)|
|Availability:||Outlook Calendar (takes a while to load)|
|Dec 11, 2020||I will serve as a Programme Committee Chair for ESOP’22.|
|Dec 1, 2020||Yutaka Nagashima joins the team as a postdoc. Welcome, Yutaka!|
|Nov 30, 2020||Our paper on Automated Repair of Heap-Manipulating Programs from Separation Logic-style specifications will appear at VMCAI 2021.|
|Nov 2, 2020||An extended paper on Distributed Protocol Combinators with an expanded toolset and more case studies has been accepted for publication in Journal of Functional Programming. Now we can do Paxos!|
|Sep 25, 2020||I am delighted to present our work on CoSplit at PurPL Seminar Series.|
|Sep 18, 2020||Our work on compiling Scilla to LLVM will appear at 2020 Virtual LLVM Developers Meeting.|
|Aug 9, 2020||Yunjeong Lee and George Pîrlea join the team as PhD students at NUS School of Computing. Welcome!|
|Apr 6, 2020||Our paper on mechanised verification of probabilistic properties of Bloom filters and their generalisations has been accepted to CAV 2020.|
Certifying Certainty and Uncertainty in Approximate Membership Query StructuresCAV 2020. LNCS, Vol. 12225, Pages 279–303. Springer.
Safer Smart Contract Programming with ScillaProc. ACM Program. Lang. 2019. Vol. 3 (OOPSLA), Pages 185:1–185:30. ACM.OOPSLA 2019 Distinguished Artifact Award
Structuring the Synthesis of Heap-Manipulating ProgramsProc. ACM Program. Lang. 2019. Vol. 3 (POPL), Pages 72:1–72:30. ACM.POPL 2019 Distinguished Paper Award
Mechanising Blockchain ConsensusCPP 2018. Pages 78–90. ACM.
Programming and Proving with Distributed ProtocolsProc. ACM Program. Lang. 2018. Vol. 2 (POPL), Pages 28:1–28:30. ACM.
Programs and Proofs: Mechanizing Mathematics with Dependent TypesLecture notes with exercises.
I am married to CG artist Lilia Anisimova.
Last time I checked, my Erdős number was 4.
Here is a high-resolution "official" photo of me, suitable for
appropriate occasions. Just in case, here's a more casual picture, couresy of
Elena Alhimovich. Yet
another old 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.