News | Group | Pubs | Projects | Talks | Teaching | Miscellanea

Ilya Sergey

Lecturer (Assistant Professor) at UCL

Department of Computer Science
University College London
Gower Street, London WC1E 6BT
United Kingdom
Room 5.02, Malet Place Engineering Building
Office Phone: +44 20 7679 0319 (Internal: 30319)
Calendar: (it takes a while to load)
Office hours: Thursday, 14:00-15:00 (please, email me first).

I do research in programming language theory, including, but not limited to types, semantics, and software verification. Lately, I have been mostly focusing on developing sound and scalable methodologies for building provably correct concurrent and distributed systems (with applications to blockchains and smart contracts). For my work, I write a lot of mechanised proofs in Coq, as well as functional code in Scala, OCaml, and Haskell.

Since November 2015, I am a member of the Programming Principles, Logic and Verification group at the Department of Computer Science of University College London. Prior to joining UCL, from December 2012 to October 2015, I was a postdoc at IMDEA Software Institute. From November 2008 to November 2012, I was a research assistant in the CS Department of KU Leuven, where I obtained my PhD. During my doctoral studies I was a visiting PhD fellow in the Department of Computer Science of Aarhus University and a research intern in the PPT group at MSR Cambridge. I got my MSc degree in Mathematics and CS in 2008 from Dept. of Mathematics and Mechanics of Saint Petersburg State University. Before joining academia I worked as a software developer at JetBrains.

If you are looking for the "CSL Family Tree" slide, you can find it here. Other slides from my recent talks are here.

Curriculum Vitae: [PDF]

What's new

Feb 7 I will be serving on the programme committee of APLAS 2018. The symposium is going to take place on the 3rd–7th December in Middle-earth New Zealand, so make sure to submit your awesome works to go there!
Jan 16 Kristoffer Just Andersen from Aarhus University joins the group as a visiting PhD researcher for five months to work on program logics for composable distributed systems.
Jan 3 Our joint position paper with Amrit Kumar and Aquinas Hobor on Scilla, a new verification-friendly intermediate-level language for smart contracts, is available on arXiv.
Dec 21 Our paper on a modular specification and a refinement-based proof of Multi-Paxos consensus protocol (joint work with Álvaro García Pérez, Alexey Gotsman and Yuri Meshman) is accepted to appear at ESOP 2018. The accompanying proof-of-concept prototype is available here.
Dec 11 Once again, I'm organising a Scenario Week Competition on Computational Geometry problems, as a part of UCL course on Systems Engineering. UPD: The concluding slides with the statistics are here.
Nov 15 Our paper on a Mechanised Blockchain Consensus (joint work with George Pîrlea) is accepted to appear at CPP 2018. The accompanying Coq development is available here.
Nov 7 I am excited to welcome Maria A Schett and Thomas Sibut-Pinote, who have joined the group to work on program logics and semantics for reasoning about distributed systems and smart contracts.
Nov 6 Programs and Proofs are updated for Coq 8.7.
Sep 26 Our paper on a Separation Logic for verification of distributed systems, with James R. Wilcox and Zachary Tatlock, is accepted to appear at POPL 2018.
Sep 12 I will be serving on the programme committee of ICFP 2018.

All news

Students and Research Associates

I am very fortunate to work with these brilliant people:
Current and past affiliates

Recent publications and manuscripts

[All publications | DBLP | Google Scholar]
Lecture notes

Selected Projects and Software

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.

Check my GitHub profile for my other projects.



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


I am married to CG artist Lilia Anisimova.

I'm on Twitter as @ilyasergey. Some pictures from my travels and other events can be found on Instagram.

While living in Madrid, I enjoyed its inimitable atmosphere and delicious food. For the latter, this Maribel's Dining Guide to Madrid (courtesy of Aleks Nanevski) always came in handy.

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.

Last modified: Mon Feb 19 13:29:51 GMT 2018