1. 06 Jun, 2018 2 commits
2. 15 May, 2018 1 commit
3. 02 May, 2018 1 commit
• Simplify the Treiber stack refinement · bf38948f
Dan Frumin authored
```The simplification is acheieved by removing the stackUR workaround.
That RA was used to enusure that the nodes that were parts of the
stack do not change themselves -- this is crucial for the safety of
pop and iter operations.

Now this is achieved by using duplicable propositions (∃ q, n ↦ᵢ{q} v)
to ensure that the node are still alive/not freed.```
4. 23 Apr, 2018 1 commit
5. 09 Apr, 2018 1 commit
6. 29 Mar, 2018 1 commit
7. 28 Mar, 2018 2 commits
8. 24 Mar, 2018 1 commit
9. 31 Jan, 2018 2 commits
10. 30 Jan, 2018 1 commit
11. 29 Jan, 2018 1 commit
12. 28 Jan, 2018 2 commits
13. 25 Jan, 2018 1 commit
14. 18 Jan, 2018 1 commit
15. 15 Jan, 2018 3 commits
• Strengthen `related_bind` · bf3aca9a
Dan Frumin authored
```We define a stronger rule `related_bind_up`, in which there is a baked
in semantic type `R`. The idea here is that we don't actually require
the expressions that we bind to have the same syntactic type.

```
{E;R::Δ;⤉Γ} ⊨ e1 ≤log≤ e2 : τ
∗ (∀ vv, ⟦ τ ⟧ (R::Δ) vv -∗ {E;Δ;Γ} ⊨ K[v1] ≤log≤ K'[v2] : τ')
____________________________________________________________
{E;Δ;Γ} ⊨ K[e1] ≤log≤ K'[e2] : τ'
```

We can then use `bin_log_related_weaken_2` to prove the original
binding rule.

The advantages of the new rule is that it allows us to prove the
following compatibility rule for seq:

```
{E;(R::Δ);⤉Γ} ⊨ e1 ≤log≤ e1' : τ1 -∗
{E;Δ;Γ} ⊨ e2 ≤log≤ e2' : τ2 -∗
{E;Δ;Γ} ⊨ (e1;; e2) ≤log≤ (e1';; e2') : τ2.
```

The idea here is that we can also pick any *semantic* type to related
e1 and e1'. For instance, if both e1 and e1' are expressions of type
Nat then it is not necessarily the case that we can relate them at
that type -- they might reduce to two different numerals -- but
it *should* be the case that we can relate their effects, if it makes
sense. E.g.

((#l <- #1;; #0) ;; e) ≤ ((#l <- #1;; #1) ;; e)```
16. 06 Jan, 2018 1 commit
17. 03 Jan, 2018 3 commits
18. 14 Dec, 2017 1 commit
19. 13 Dec, 2017 1 commit
20. 12 Dec, 2017 1 commit
21. 10 Dec, 2017 1 commit
22. 07 Dec, 2017 2 commits
23. 04 Dec, 2017 1 commit
24. 02 Dec, 2017 1 commit
25. 01 Dec, 2017 3 commits
26. 29 Nov, 2017 4 commits