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 (Singapore), holding a joint appointment with NUS School of Computing, where I am also a Co-PI at NUS Crystal Centre. 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, Research Intern at NUS SoC, 2019-2020.
• Yasunari Watanabe, Capstone Project Student at Yale-NUS, 2019-2020.

Recent Publications and Manuscripts

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


• QED at Large: A Survey of Engineering of Formally Verified Software
  Talia Ringer, Karl Palmskog, Ilya Sergey, Milos Gligoric, Zachary Tatlock
  Foundations and Trends in Programming Languages, Volume 5, Issue 2-3, September 2019.
  [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]


• Distributed Protocol Combinators
  Kristoffer Just Andersen and Ilya Sergey
  21st International Symposium on Practical Aspects of Declarative Languages (PADL 2019). Lisbon, Portugal, January 2019.
  [PDF | Code]


• Finding the Greedy, Prodigal, and Suicidal Contracts at Scale
  Ivica Nikolić, Aashish Kolluri, Ilya Sergey, Prateek Saxena, and Aquinas Hobor
  2018 Annual Computer Security Applications Conference (ACSAC 2018). San Juan, Puerto Rico, USA, December 2018.
  [PDF | Tool]

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

• YSC3248: Parallel, Concurrent and Distributed Programming, Lecturer. Yale-NUS College. Autumn 2019.
• YCC1122: Quantitative Reasoning, Lecturer. Yale-NUS College. Autumn 2019.
• YSC2229: Introductory Data Structures and Algorithms, Lecturer. Yale-NUS College. Spring 2019.
• SIGPL Summer School 2018, Dongguk University, Seoul, Korea. August 2018. Lecturer. [Lecture 1 | Lecture 2 | Lecture 3]
• 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.
• Programs and Proofs: Mechanizing Mathematics with Dependent Types, Summer School
  Lecturer. JetBrains Inc. / Saint-Petersburg State University. August 2014. [School page]

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.