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. In 2015-2018, 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 MSc in mathematics from Saint Petersburg State University. Before joining academia I worked as a software engineer at JetBrains in IntelliJ IDEA team.

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.

• I designed and co-developed Scilla, a programming language for safe smart contracts, used by Zilliqa.
• In 2019 I have been awarded the AITO Dahl-Nygaard Junior Prize.
• I organised the ICFP Programming Contest 2019 (aka Wrappy, aka Lambda-coin). Here are the report slides
• During my postdoc, I wrote lecture notes on proving theorems in Coq/Ssreflect. Consider using them for your Coq class.
• A few years ago, I've made the Concurreny Logic Family Tree slide. Feel free to borrow it for your talk on the subject.
• At different moments in the past I contributed to Facebook Infer and GHC. Very long time ago I used to work at JetBrains on Scala and Clojure support in IntelliJ IDEA.

Curriculum Vitae: [PDF]

What's New

Students and Research Associates

• Kiran Gopinathan, PhD Student at NUS SoC, since August 2019.
• Yunjeong Lee, PhD Student at NUS SoC, since August 2020.
• George Pîrlea, PhD Student at NUS SoC, since August 2020.
• Yasunari Watanabe, MSc Student at NUS SoC, AY 2020/21.


• Nick Chin, Capstone Student at Yale-NUS College, AY 2020/21.
• Tram Hoang, Capstone Student at Yale-NUS College, AY 2020/21.
• Alaukik Pant, Capstone Student at Yale-NUS College, AY 2020/21.
• Gabriel Petrov, Capstone Student at Yale-NUS College, AY 2020/21.
• Bryan Tan, Capstone Student at Yale-NUS College, AY 2020/21.

• Andreea Costea, working on deductive program synthesis and repair.
• Abhishek Tiwari, working on concurrent program repair.

Recent Publications and Manuscripts

• Certifying Certainty and Uncertainty in Approximate Membership Query Structures
  Kiran Gopinathan, and Ilya Sergey
  32nd International Conference on Computer-Aided Verification (CAV 2020). Los Angeles, CA, USA, July 2020.
  [PDF | GitHub]


• Concise Read-Only Specifications for Better Synthesis of Programs with Pointers
  Andreea Costea, Amy Zhu, Nadia Polikarpova, and Ilya Sergey
  29th European Symposium on Programming (ESOP 2020). Dublin, Ireland, April 2020.
  [PDF | GitHub]


• Safer Smart Contract Programming with Scilla
  Ilya Sergey, Vaivaswatha Nagaraj, Jacob Johannsen, Amrit Kumar, Anton Trunov, and Ken Chan Guan Hao
  34th ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications (OOPSLA 2019). Athens, Greece, October 2019.
  Recipient of OOPSLA 2019 Distinguished Artifact Award
  [PDF | GitHub | Accepted Artifact | Slides | Video]


• QED at Large: A Survey of Engineering of Formally Verified Software
  Talia Ringer, Karl Palmskog, Ilya Sergey, Milos Gligoric, and Zachary Tatlock
  Foundations and Trends in Programming Languages, Volume 5, Issue 2-3, September 2019.
  [PDF | Publisher's Site | Errata | Submit a Correction]


• Exploiting The Laws of Order in Smart Contracts
  Aashish Kolluri, Ivica Nikolić, Ilya Sergey, Aquinas Hobor, and Prateek Saxena
  28th ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA 2019). Beijing, China, July 2019.
  [PDF]


• Structuring the Synthesis of Heap-Manipulating Programs
  Nadia Polikarpova and Ilya Sergey
  46th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2019). Lisbon, Portugal, January 2019.
  Recipient of POPL 2019 Distinguished Paper Award
  [PDF | Extended Version | GitHub | Accepted Artifact | Slides]


• A True Positives Theorem for a Static Race Detector
  Nikos Gorogiannis, Peter O'Hearn, and Ilya Sergey
  46th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2019). Lisbon, Portugal, January 2019.
  [PDF | Extended Version | Accepted Artifact | Slides]

Lecture notes

• Programs and Proofs: Mechanizing Mathematics with Dependent Types
  Lecture notes with exercises.
  [PDF | Course page | GitHub]
  

Selected Projects and Software

• Certichain
  Mechanised reasoning about blockchain consensus protocols.
  [Project Page]
  
• Scilla
  A strongly typed functional intermediate language for smart contracts.
  [Web page | Position Paper | GitHub]
  
• SuSLik
  A synthesis tool for heap-manipulating orograms using Separation Logic.
  [Paper | GitHub]
  
• Disel: Distributed Separation Logic
  A mechanised framework for compositional verification of distributed systems.
  [Project page | GitHub]
  
• FCSL: Fine-grained Concurrent Separation Logic
  A Coq-based verification tool for fine-grained concurrent programs.
  [Project page | Main Paper]
  
• Pushdown k-CFA
  Pushdown context-sensistive control-flow analysis with optional Abstract Garbage Collection for LambdaJS and a subset of Scheme programming language.
  [GitHub | Paper]
  

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.

In Press

• Scilla - A Formal Verification Oriented Contract Language. Video Interview to Epicenter. 6 June 2018.
• Mike Orcutt. Ethereum’s smart contracts are full of holes. MIT Technology Review. 1 March 2018.
• Jordan Pearson. Millions of Dollars In Ethereum Are Vulnerable to Hackers Right Now. Motherboard, Vice. 22 February 2018.

Teaching

at Yale-NUS College and NUS School of Computing

• YSC3208: Programming Language Design and Implementation, Lecturer. Yale-NUS College.
  Autumn 2020
• YSC3248: Parallel, Concurrent and Distributed Programming, Lecturer. Yale-NUS College.
  Autumn 2019, Autumn 2020
• YSC2229: Introductory Data Structures and Algorithms, Lecturer. Yale-NUS College.
  Spring 2019, Spring 2020.
• YCC1122: Quantitative Reasoning, Lecturer. Yale-NUS College.
  Autumn 2019.

at Summer Schools

• SIGPL Summer School 2018, Dongguk University, Seoul, Korea. August 2018. Lecturer.
  [Lecture 1 | Lecture 2 | Lecture 3]
• Programs and Proofs: Mechanizing Mathematics with Dependent Types, Summer School, Lecturer.
  JetBrains Inc. / Saint-Petersburg State University. August 2014. [School page]

at University College London

• ENGS102P: Design and Professional Skills, Scenario Project Organiser. UCL. Spring 2018.
• COMP104P: Theory II, Anallysis of Algorithms, Lecturer. UCL. Spring 2016, Spring 2017, Spring 2018.
• COMP214P: Systems Engineering, Scenario Week Designer. UCL. Autumn 2017. [Intro | Conclusion]
• COMP205P: Software Engineering and HCI, Scenario Week Designer. UCL. Spring 2017. [Intro | Conclusion]
• COMP205P: Software Engineering and HCI, Scenario Week Designer. UCL. Spring 2016. [Intro | Conclusion]
• COMP2012: Directed Reading, Second Examiner. UCL. Spring 2016.

Collaborators

Over the years, I have been very lucky to work on joint research projects with some great people:

Miscellanea

I am married to CG artist Lilia Anisimova.

I am on Twitter as @ilyasergey.

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.