New paper

“Lem: reusable engineering of real world semantics”, joint work with Dominic P. Mulligan, Scott Owens, Kathryn E. Gray, Tom Ridge and Peter Sewell”.

To appear at the International Conference on Functional Programming (ICFP) 2014.

New paper

“Certified complexity (CerCo)”, joint work with Roberto Amadio, Nicolas Ayache, Francois Bobot, Jaap Boender, Brian Campbell, Ilias Garnier, Antoine Madet, James McKinna, Dominic Mulligan, Mauro Piccolo, Randy Pollack, Yann Regis-Gianas, Claudio Sacerdoti Coen, Ian Stark and Paolo Tranquilli.

To appear in the postproceedings of the third international workshop on Foundational and Practical Aspects of Resource Analysis (FOPARA) 2013.

New paper

“On the correctness of an optimising assembler”, joint work with Claudio Sacerdoti Coen, describing a formalisation and proof of correctness in Matita of an optimising assembler for the Intel MCS-51 8-bit microprocessor, part of the CerCo project.

To be presented at Certified Proof and Programs (CPP) 2012.