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.
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.


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.


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