Diaframe is a plugin for Iris trying to improve and expand the automation of proofs.
Diaframe is a plugin for Iris aimed at (partially) automating proofs.
This repository contains the Coq mechanization of Diaframe. The (technical) appendix to Diaframe can be found in the [wiki](https://gitlab.mpi-sws.org/iris/automation/-/wikis/Appendix-to-Diaframe).
