Abstract:
We present a comprehensive set of tactics for working with a shallow embedding of a higher-order separation logic for a subset of Java in Coq. The tactics make it possible to reason at a level of abstraction> similar to pen-and-paper separation-logic proof outlines. In particular, the tactics allow the user to reason in the embedded logic rather than in the concrete model, where the stacks and heaps are exposed. The development is generic in the choice of heap model, and most of the development is also independent of the choice of programming language.
Short bio:
I got my doctorate in 2010 from the University of Uppsala, under the supervision of professor Joachim Parrow, on mechanising theories for process calculi in the interactive proof assistant Isabelle. Since April 2010, I have been employed as a postdoc at the IT University of Copenhagen. My focus has been on providing tools for mechanising proofs of correctness of programs written in object-oriented languages using separation logic.
Contact:
The speaker will be visiting Imperial on March 7 and 8. Contact Sergio Maffeis if you would like to arrange a meeting.