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 and School of Computing of National University of Singapore, where I run the VERSE research lab.

I do research in programming language design and implementation, software verification, program synthesis and repair. 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 language 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.

Short bio in plain text and 3rd person

coordinates

Postal Address:

 Yale-NUS College, 28 College Avenue West
#01-501, Singapore 138533
Email:
Offices:
 #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)

news

Apr 20, 2021 Looking forward to serve on the programme committees of International Symposium on DIStributed Computing (DISC’21) and of the 3rd International Workshop on Formal Methods for Blockchains (FMBC’21). Make sure to submit your papers on (verified) distributed systems, blockchains, and their applications for quality feedback (and, hopefully, publication)!
Apr 12, 2021 Our PLDI’21 paper on smart contract sharding with static analysis is now available.
Feb 26, 2021 Two papers (conditionally) accepted at PLDI’21:
  • The paper on Practical Smart Contract Sharding with Ownership and Commutativity Analysis (co-authored with George Pîrlea and Amrit Kumar) provides the first PL-based approach to parallelise validation of smart contract transactions in Ethereum-style sharded blockchains. Preprint coming soon!
  • The paper on Cyclic Program Synthesis (joint work with Shachar Itzhaky, Hila Peleg, Nadia Polikarpova and Reuben Rowe) describes the first technique for automatically synthesising heap-manipulating programs with recursive "helper" functions, from declarative specifications, without any other hints.
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.

selected publications

  1. Practical Smart Contract Sharding with Ownership and Commutativity Analysis
    George Pîrlea, Amrit Kumar, and Ilya Sergey
    PLDI 2021. ACM.
    PDF Artifact
  2. Certifying Certainty and Uncertainty in Approximate Membership Query Structures
    Kiran Gopinathan, and Ilya Sergey
    CAV 2020. LNCS, Vol. 12225, Pages 279–303. Springer.
    PDF Code Blog Slides Video
  3. Safer Smart Contract Programming with Scilla
    Ilya Sergey, Vaivaswatha Nagaraj, Jacob Johannsen, Amrit Kumar, Anton Trunov, and Ken Chan Guan Hao
    Proc. ACM Program. Lang. 2019. Vol. 3 (OOPSLA), Pages 185:1–185:30. ACM.
    OOPSLA 2019 Distinguished Artifact Award
    PDF Code Artifact Slides Video
  4. 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
    PDF arXiv Code Artifact Slides Video
  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.
    PDF Code Slides

lecture notes

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

miscellanea

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 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.