The repository for the project Iris with ControlFlow.
The theories folder is the source code of our Coq formalization.
- lang.v defines the programming language with control flow statements and proves relative properties.
- notation.v defines notations and syntax sugars for the programming language.
- multi_post.v defines our weakest precondition with multiple post-conditions and proves some useful proof rules of it.
The docs folder gives documentations of our formalization.
There is only a draft of our documentation, and we are still working on a more detailed version.