Abstract
In program verification, it is common to embed a highlevel object logic into the meta logic of a proof assistant to hide lowlevel aspects of the verification. To verify imperative and concurrent programs, separation logic hides explicit reasoning about heaps and pointer disjointness. To verify programs with cyclic features such as modules or higherorder state, modal logic provides modalities to hide explicit reasoning about stepindices that are used to stratify recursion.
The meta logic of proof assistants such as Coq is well suited to embed highlevel object logics and prove their soundness. However, proof assistants such as Coq do not have native infrastructure to facilitate proofs in embedded logics  their proof contexts and builtin tactics for interactive and automated proofs are tailored to the connectives of the meta logic, and do not extend to those of the object logic. 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.
In this talk I will describe our work in the Iris project to address this problem  first for interactive proofs, and then for semiautomated proofs. The Iris Proof Mode provides highlevel tactics for interactive proofs in higherorder concurrent separation logic with modalities. Recent work on RefinedC and Diaframe have built on top of the Iris Proof Mode to obtain proof automation for lowlevel C programs and finegrained concurrent programs.
BibTeX  Entry
@InProceedings{krebbers:LIPIcs.ITP.2023.2,
author = {Krebbers, Robbert},
title = {{Interactive and Automated Proofs in Modal Separation Logic}},
booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)},
pages = {2:12:1},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783959772846},
ISSN = {18688969},
year = {2023},
volume = {268},
editor = {Naumowicz, Adam and Thiemann, Ren\'{e}},
publisher = {Schloss Dagstuhl  LeibnizZentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2023/18377},
URN = {urn:nbn:de:0030drops183770},
doi = {10.4230/LIPIcs.ITP.2023.2},
annote = {Keywords: Program Verification, Separation Logic, StepIndexing, Modal Logic, Interactive Theorem Proving, Proof Automation, Iris, Coq}
}
Keywords: 

Program Verification, Separation Logic, StepIndexing, Modal Logic, Interactive Theorem Proving, Proof Automation, Iris, Coq 
Collection: 

14th International Conference on Interactive Theorem Proving (ITP 2023) 
Issue Date: 

2023 
Date of publication: 

26.07.2023 