 05 Jun, 2018 10 commits


Ralf Jung authored

Ralf Jung authored

Ralf Jung authored

Ralf Jung authored

Ralf Jung authored

Ralf Jung authored
The BI interface is then instantiated using these laws. In particular, this shows that the rules we claim to be admissible actually are.

Ralf Jung authored

Ralf Jung authored
Fixes #193

Ralf Jung authored

Ralf Jung authored

 04 Jun, 2018 5 commits


Ralf Jung authored

Ralf Jung authored

Ralf Jung authored
Show that atomic_step is an AccElim so we can open invariants; get entirely rid of the Em ⊆ Eo sidecondition

Ralf Jung authored

Ralf Jung authored
New atomic updates: defined as a fixed point with existential quantifier; intro lemma using class of Laterable assertions

 01 Jun, 2018 5 commits


Ralf Jung authored

Ralf Jung authored

Robbert Krebbers authored

Robbert Krebbers authored

Ralf Jung authored

 31 May, 2018 3 commits


Robbert Krebbers authored

Robbert Krebbers authored
If the BI is not affine, this should not happen, as it may lead to information loss. This commit fixes issue #190.

Robbert Krebbers authored
Thanks to @dfrumin.

 30 May, 2018 2 commits


Robbert Krebbers authored

Ralf Jung authored

 29 May, 2018 10 commits


Ralf Jung authored

Ralf Jung authored

Ralf Jung authored


Ralf Jung authored

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored
These instances are the same as those for e.g. the later modality.

Robbert Krebbers authored

Ralf Jung authored

 28 May, 2018 1 commit


Ralf Jung authored
provide big_op lemmas outside of bi module See merge request FP/iriscoq!149

 25 May, 2018 3 commits
 24 May, 2018 1 commit


Ralf Jung authored
