- Nov 01, 2019
-
-
Ralf Jung authored
Update version in URL for Iris appendix See merge request iris/iris!321
-
Paolo G. Giarrusso authored
I'd consider (in addition or alternative) to link to a new http://plv.mpi-sws.org/iris/appendix-master.pdf, always matching the latest version.
-
Robbert Krebbers authored
Soundness lemma for internal equality of `uPred`. See merge request iris/iris!315
-
Robbert Krebbers authored
-
Ralf Jung authored
-
Ralf Jung authored
Semantic invariants See merge request iris/iris!319
-
Ralf Jung authored
-
Robbert Krebbers authored
drop Coq 8.7 and add 8.10 Closes #242 See merge request iris/iris!320
-
Ralf Jung authored
-
Ralf Jung authored
-
-
Ralf Jung authored
rename LitErased -> LitPoison See merge request iris/iris!318
-
- Oct 31, 2019
- Oct 25, 2019
-
-
Robbert Krebbers authored
-
- Oct 22, 2019
-
-
Ralf Jung authored
-
- Oct 18, 2019
-
-
Ralf Jung authored
-
- Oct 14, 2019
-
-
Robbert Krebbers authored
Add `Atomic` instances for all atomic `heap_lang` constructs. See merge request iris/iris!317
-
Robbert Krebbers authored
-
- Oct 12, 2019
-
-
Robbert Krebbers authored
Also removed some admissible instances: - `Atomic s (ResolveProph (Val v1) (Val v2))` (this one was already admissible) - `Atomic s Skip` (became admissible due to the instance for β)
-
- Oct 11, 2019
-
-
Ralf Jung authored
Prove that non-value WP is contractive. See merge request iris/iris!316
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
- Oct 09, 2019
-
-
Ralf Jung authored
-
- Oct 05, 2019
-
-
Derek Dreyer authored
-
- Sep 20, 2019
-
-
Ralf Jung authored
-
- Sep 19, 2019
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
Let `iProp` refer to `uPred ... : Type` instead of `uPredO ... : ofeT` See merge request iris/iris!314
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Ralf Jung authored
-
- Sep 13, 2019
-
-
Jacques-Henri Jourdan authored
Reorder Requires so that we do not depend of Export bugs. See merge request iris/iris!313
-
Jacques-Henri Jourdan authored
The general idea is to first import/export modules which are further than the current one, and then import/export modules which are close dependencies. This commit tries to use the same order of imports for every file, and describes the convention in ProofGuide.md. There is one exception, where we do not follow said convention: in program_logic/weakestpre.v, using that order would break printing of texan triples (??).
-
Robbert Krebbers authored
-
- Sep 11, 2019
-
-
Robbert Krebbers authored
Add `iStopProof` tactic Closes #265 See merge request !311
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-