- Oct 23, 2017
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
Now that we have the plain modality, we can get rid of the basic updates in the soundness statement.
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Amin Timany authored
-
Robbert Krebbers authored
-
- Oct 19, 2017
- Oct 18, 2017
- Oct 12, 2017
-
-
Ralf Jung authored
-
- Oct 10, 2017
-
-
Robbert Krebbers authored
Introduce a connective `ilocked` to stop `iNext` and `iFrame`. See merge request FP/iris-coq!67
-
Robbert Krebbers authored
-
Ralf Jung authored
use primitive projections for our mixins See merge request FP/iris-coq!69
-
Ralf Jung authored
-
Ralf Jung authored
Remove an unused argument for `newcounter_mono_spec`. See merge request FP/iris-coq!70
-
Dan Frumin authored -
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
-
- Oct 09, 2017
- Oct 07, 2017
-
-
Ralf Jung authored
-
- Oct 05, 2017
-
-
Robbert Krebbers authored
update stdpp See merge request FP/iris-coq!68
-
Hai Dang authored
-
