Merge branch 'lc-weakestpre' into 'master'
Add later credits to the WP See merge request !808
Showing
- CHANGELOG.md 15 additions, 6 deletionsCHANGELOG.md
- iris/base_logic/lib/later_credits.v 2 additions, 2 deletionsiris/base_logic/lib/later_credits.v
- iris/bi/updates.v 19 additions, 1 deletioniris/bi/updates.v
- iris/program_logic/adequacy.v 33 additions, 21 deletionsiris/program_logic/adequacy.v
- iris/program_logic/ectx_lifting.v 13 additions, 13 deletionsiris/program_logic/ectx_lifting.v
- iris/program_logic/lifting.v 31 additions, 19 deletionsiris/program_logic/lifting.v
- iris/program_logic/ownp.v 5 additions, 3 deletionsiris/program_logic/ownp.v
- iris/program_logic/total_weakestpre.v 1 addition, 1 deletioniris/program_logic/total_weakestpre.v
- iris/program_logic/weakestpre.v 76 additions, 19 deletionsiris/program_logic/weakestpre.v
- iris_heap_lang/derived_laws.v 2 additions, 2 deletionsiris_heap_lang/derived_laws.v
- iris_heap_lang/primitive_laws.v 7 additions, 7 deletionsiris_heap_lang/primitive_laws.v
- iris_heap_lang/proofmode.v 1 addition, 0 deletionsiris_heap_lang/proofmode.v
- tex/program-logic.tex 5 additions, 4 deletionstex/program-logic.tex
Loading
Please register or sign in to comment