News

2018

Jun 20 Kiran Gopinathan and Oscar King join the group as research interns for Summer 2018. They will be working on implementation and verification of blockchain protocols.
Jun 7 I will be leaving UCL in October 2018, and will move to Singapore, joining Yale-NUS College as an Assistant Professor.
Jun 6 Amrit and I gave a long interview to Epicenter about Scilla and formal verification of smart contracts.
Jun 1 Next year, I will be serving on the Programme Committees of PLDI 2019 and OOPSLA 2019. Looking forward for reading lots of (your) exciting submissions on types, logics, compilers, verification, and program synthesis!
Mar 21 I am thrilled to be amongst the recipients of the Google Faculty Research Award 2017 and looking forward to advance the state of the art in verified optimisations for distributed systems. Here is the full list of this year recipients.
Mar 7 I am really excited to join the amazing Zilliqa team as an advisor on formal methods to collaborate on safe and secure programming languages for smart contracts.
Mar 1 I've made an appearance in another article on smart contracts, this time by MIT Technology Review. Not sure I fully agree with its tone, though.
Feb 22 Our technical report on a symbolic analysis of Ethereum smart contracts for trace vulnerabilities got featured in an article by Vice's Motheboard. Amongst other things, our paper gives hints on how to become $6,000,000 richer, so you might want to read it.
Feb 15 I will be on the programme committee of POPL 2019. I should probably encourage you to submit your cutting edge PL research there, but I know you will do it anyway.
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 now available.

2017

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.
Aug 10 Awarded an eight-month grant by Research Institute in Verified Trustworthy Software Systems for the project Automated Reasoning with Fine-Grained Concurrent Collections, in collaboration with Nikos Gorogiannis.
Jul 20 I'm co-chairing (together with Yves Bertot) the CoqPL 2018 workshop, co-located with POPL 2018 in Los Angeles, CA in January. Details and submission guidelines here.
May 18 I'm chairing the ICFP 2017 Student Research Competition. A good poster presentation is a great chance to show off your (or your PhD students') research, and it will drastically improve your chances to get valuable feedback before submitting a POPL paper. There are also money prizes, so go ahead and submit an extended abstract! Deadline is July 10.
Apr 24 Invited to serve on the PC of 15th Asian Symposium on Programming Languages and Systems (APLAS 2017) and Scala Symposium 2017.
Apr 12Paper on verified concurrent data structures with changeable-post-factum histories is accepted to ECOOP 2017.
Mar 24I'm giving an invited talk at Programming Languages and Compilers conference in Rostov-on-Don on 3-5 April 2017.
Mar 6The registration for the 6th South of England Regional Programming Language Seminar (S-REPLS 6), which will take place at UCL on May 25, is now open. Please, indicate your attendance by participating in this poll.
Mar 5 Our position paper on type theory for compositionally verified distributed systems will appear at SNAPL 2017.
Feb 20 I'm organising a Scenario Week Competition on Computational Geometry problems, as a part of UCL course on Software Engineering. The concluding slides from the competition are here.

2016

Dec 15 An extended version of our POPL'14 paper on cardinality analysis featuring new cool evaluation of the analysis (im)precision has been accepted for publication in Journal of Functional Programming.
Nov 15 Announced a postdoc poisition on compositionally verified distributed systems. Details above.
Oct 3 Awarded with EPSRC First Grant on Program Logics for Distributed Systems.
Sep 25 Invited to serve on the PC of Static Analysis Symposium 2017.
Nov 1 I'm serving on the PC of the 1st Workshop on Trusted Smart Contracts. Submit your ideas on programmable cryptocurrencies!
Aug 27 Paper on specifying and verifying non-linearizable concurrent objects is accepted to OOPSLA 2016.
Jun 10 The slide with the flow of ideas in modern concurrency logics is now available here.
Jun 5 I'm serving on the PC of Scala Symposium 2016. Submit papers on your Scala projects!
May 25 Paper on QuickChecking computational geometry algorithms is accepted to ICFP 2016.
Mar 15 I will be serving on the programme committee of TAPAS 2016. Submit proposals for your talks on static analysis!
Feb 17 "Programs and Proofs" are now updated for Coq 8.5 and Ssreflect 1.6.
Feb 1 I'm organizing Scenario Week on Computational Geometry as a part of Software Engineering and HCI course at UCL.
Jan 15 I will be serving on the programme committee of POPL 2017.
Jan 10 PPLV@UCL has an opening for a lecturer position.

2015

Dec 30 New blog post on Lamport's critique of compositionality.
Dec 12 I will be teaching the Theory II module in Spring 2016.

Main page