Ilya Sergey

Associate Professor (tenure track) at Yale-NUS College and NUS School of Computing
Lead Language Designer at Zilliqa

I am a tenure-track Associate Professor at Yale-NUS College with a joint appointment at School of Computing of National University of Singapore, where I run the VERSE research lab.

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 Saint Petersburg State University. Before joining academia I worked as a software engineer at JetBrains.


Postal Address:

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
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! :tada: :computer:
Apr 6, 2020 Our paper on mechanised verification of probabilistic properties of Bloom filters and their generalisations has been accepted to CAV 2020.

selected publications

  1. Certifying Certainty and Uncertainty in Approximate Membership Query Structures
    Kiran Gopinathan, and Ilya Sergey
    CAV 2020. LNCS, Vol. 12225, Pages 279–303. Springer.
  2. Safer Smart Contract Programming with Scilla
    Proc. ACM Program. Lang. 2019. Vol. 3 (OOPSLA), Pages 185:1–185:30. ACM.
    OOPSLA 2019 Distinguished Artifact Award
  3. Structuring the Synthesis of Heap-Manipulating Programs
    Nadia Polikarpova, and Ilya Sergey
    Proc. ACM Program. Lang. 2019. Vol. 3 (POPL), Pages 72:1–72:30. ACM.
    POPL 2019 Distinguished Paper Award
  4. Mechanising Blockchain Consensus
    George Pîrlea, and Ilya Sergey
    CPP 2018. Pages 78–90. ACM.
  5. Programming and Proving with Distributed Protocols
    Ilya Sergey, James R. Wilcox, and Zachary Tatlock
    Proc. ACM Program. Lang. 2018. Vol. 2 (POPL), Pages 28:1–28:30. ACM.

lecture notes

  1. Programs and Proofs: Mechanizing Mathematics with Dependent Types
    Ilya Sergey
    Lecture notes with exercises.


I am married to CG artist Lilia Anisimova.

Last time I checked, my Erdős number 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 Kickstarter.

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.