Ilya Sergey

Associate Professor at National University of Singapore


I am a tenured Associate Professor at the School of Computing of National University of Singapore, where I run the VERSE research group as a part of PLSE@NUS lab. I hold a joint appointment at Yale-NUS College. I am also a Research Consultant at Mysten Labs.

I do research in programming languages, software verification, distributed systems, and program synthesis. I am the recipient of the AITO Dahl-Nygaard Junior Prize 2019. I designed and co-developed Scilla programming language and 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. 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:

School of Computing, National University of Singapore
COM1, 13 Computing Drive, Singapore 117417
Email:
Office:
COM3-02-56
Office Phone: +65 6601 1466
Availability: Outlook Calendar

announcements

  • Multiple postdoc positions are available in the 5-year MOE Tier 3 project on automated program repair via static analysis and verification. Check out the project page for the details and get in touch!
  • I am actively looking for motivated PhD students who would like to work on software analysis, verification, and certified synthesis, applying those techniques to concurrent and distributed systems. Feel free to email me if you'd like to chat about research opportunities (please, check the lab page for the relevant topics first) and apply here. The application deadlines are 15 June and 15 December.
  • Research internships: In case if you are interested in an internship, please send me an email with your CV and a paragraph of text describing your specific interests in the topics of my reseatch (see the lab page for more details). Strong background in PL/logic/verification or systems-building is a must. I welcome candidates who will commit six months or longer to focused research on-site, and generally unable to respond to requests otherwise.

news

Oct 2, 2024 I am excited to serve as the General Chair for ICFP’25 and as the Local Chair for the joint ICFP/SPLASH’25 conference, which will take place in Singapore on 12-18 October 2025.
Aug 27, 2024 Our paper on implementing concurrent data structures via batch-parallelism (joint work with Callista Le, Kiran Gopinathan, Koon Wen Lee, and Seth Gilbert) will appear at OOPSLA’24.
Aug 24, 2024 Our work on compositionally verying safety and liveness of BFT protocols (with Qiyuan Zhao, George Pîrlea, Karolina Grzeszkiewicz, and Seth Gilbert) will be presented at CCS’24.
Jul 12, 2024 Our work on higher-order specifications for deductive synthesis in SuSLik (done in collaboration with with Ziyi Yang, David Young, and Alex Potanin) is accepted to ECOOP’24.
May 26, 2024 Together with Amal Ahmed and Derek Dreyer, we are organising the first Workshop on Red-Hot Topics in Faculty Mentoring (RTFM), co-located with PLDI’24 in Copenhagen. The workshop will take place on June 25, 2024. If you’re a soon-to-be or a junior (or even a senior) academic faculty, consider attending it!
Apr 22, 2024 I gave a talk on Proving as Programming at NUS Workshop on Formal Proofs and Lean.
Apr 9, 2024 All materials for my course on Data Structures and Algorithms in OCaml, taught at Yale-NUS College in 2019-2021, are now made public. Enjoy!
Apr 5, 2024 Our paper on a hyperlogic for verifying sparse tensor programs in Coq (joint work with Vladimir Gladshtein, Qiyuan Zhao, Willow Ahrens, and Saman Amarasinghe) will appear at PLDI’24. See you in Copenhagen in June!

selected publications

  1. Concurrent Data Structures Made Easy
    Proc. ACM Program. Lang. 2024. Vol. 8, (OOPSLA), ACM.
  2. Compositional Verification of Composite Byzantine Protocols
    31st ACM Conference on Computer and Communications Security (CCS’24) 2024. ACM.
  3. Mechanised Hypersafety Proofs about Structured Data
    Proc. ACM Program. Lang. 2024. Vol. 8, (PLDI), ACM.
  4. Mostly Automated Proof Repair for Verified Libraries
    Kiran Gopinathan, Mayank Keoliya, and Ilya Sergey
    Proc. ACM Program. Lang. 2023. Vol. 7, (PLDI), ACM.
    ACM SIGPLAN Distinguished Paper Award
  5. Leveraging Rust Types for Program Synthesis
    Proc. ACM Program. Lang. 2023. Vol. 7, (PLDI), ACM.
    Distinguished Artifact Award
  6. Cyclic Program Synthesis
    PLDI 2021. ACM.
    ACM SIGPLAN Distinguished Paper Award
  7. Practical Smart Contract Sharding with Ownership and Commutativity Analysis
    George Pîrlea, Amrit Kumar, and Ilya Sergey
    PLDI 2021. ACM.

lecture notes

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

miscellanea

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.


© Copyright 2024 Ilya Sergey. Powered by Jekyll with al-folio theme.