Interactive proofs in higher order concurrent separation logic: iris proof mode demo

There has been tremendous progress on program logics for increasingly sophisticated programming language that reason about challenging features. In this talk, I presented a paper that mechanizes reasoning in CSL by embedding it in the Coq proof assistant. The goal of this paper is to make reasoning in the object logic in the same style as reasoning in Coq proof assistant. When using a proof assistants to reason in an embedded logic one cannot benefit from the proof contexts and basic tactics of the proof assistants. This results in proofs that are at a too low level of abstraction because they are cluttered with bookkeeping code related to manipulating the object logic. I will be talking about a so-called proof mode that extends the Coq proof assistant with named proof contexts for the object logic. I also gave a demo where we dived into emacs with examples of how proofs are done in both Coq and Iris proof modes.