 07 Sep, 2016 1 commit


JacquesHenri Jourdan authored

 06 Sep, 2016 6 commits


Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored
I had to perform some renaming to avoid name clashes.

 05 Sep, 2016 3 commits


Robbert Krebbers authored

JacquesHenri Jourdan authored

Robbert Krebbers authored

 04 Sep, 2016 1 commit


Robbert Krebbers authored

 02 Sep, 2016 1 commit


Robbert Krebbers authored

 01 Sep, 2016 4 commits


Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

 31 Aug, 2016 5 commits


Robbert Krebbers authored

Robbert Krebbers authored
Annoyingly, this requires one to prove the following in the model: (∀ x : A, ■ φ x) ⊢ ■ (∀ x : A, φ x)

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

 30 Aug, 2016 6 commits


Robbert Krebbers authored
Thanks to Ranald Clouston for suggesting the axiom: ▷ P ⊢ ▷ False ∨ (▷ False → P) This axiom is used to prove timeless of implication, wand and forall. Timelessness of the pure and ownM connectives is still proven in the model, but we first state the property in a way that it does not involved derived notions (like the except_last modality).

Robbert Krebbers authored
It is unused, and ownM_empty is stronger.

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored
For that we need a slightly stronger property for distributing a later over an existential quantifier.

Robbert Krebbers authored

 29 Aug, 2016 7 commits


Robbert Krebbers authored
This way we ensure that Coq gives an error message when one accidentially writes "N ⊆ E" instead of "nclose N ⊆ E". Before, it used the ⊆ instance of lists.

Robbert Krebbers authored

Robbert Krebbers authored
This happened for example in <[i:=x]>∅, where simpl unfold insert (despite it being declared simpl never) because ∅ reduces to a constructor.

Robbert Krebbers authored
This avoids Coq distinguishing iProp and uPred (iResUR _) when it should not.

Robbert Krebbers authored
(which are useful in Amin's logical relations development).

Ralf Jung authored

Ralf Jung authored

 28 Aug, 2016 2 commits


Robbert Krebbers authored
This also removes the double use of the name 'wp_fork' in both program_logic/weakestpre and heap_lang/lifting.

Robbert Krebbers authored

 27 Aug, 2016 1 commit


Zhen Zhang authored

 26 Aug, 2016 3 commits


Robbert Krebbers authored

Robbert Krebbers authored

Zhen Zhang authored
Add lock interface @jung looks good? See merge request !3
