 31 Jan, 2018 2 commits


Dan Frumin authored

Dan Frumin authored

 30 Jan, 2018 1 commit


Dan Frumin authored

 29 Jan, 2018 1 commit


Dan Frumin authored
Thanks to Robbert

 28 Jan, 2018 2 commits


Dan Frumin authored
Thunk the FG/CG_increment functions at the point of initialization. This allows us to avoid the use of lamsubst.

Dan Frumin authored

 25 Jan, 2018 1 commit


Dan Frumin authored
 relational specifications for weak increment  logically atomic specification for `ticket_lock.acquire`

 18 Jan, 2018 1 commit


Dan Frumin authored

 15 Jan, 2018 3 commits


Dan Frumin authored

Dan Frumin authored

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)

 06 Jan, 2018 1 commit


Dan Frumin authored

 03 Jan, 2018 3 commits


Dan Frumin authored

Dan Frumin authored

Dan Frumin authored

 14 Dec, 2017 1 commit


Dan Frumin authored

 13 Dec, 2017 1 commit


Dan Frumin authored

 12 Dec, 2017 1 commit


Dan Frumin authored

 10 Dec, 2017 1 commit


Dan Frumin authored

 07 Dec, 2017 2 commits


Dan Frumin authored

Dan Frumin authored
 Notation for types  Notation for pack and unit  Better (?) levels for the relational judgement

 04 Dec, 2017 1 commit


Dan Frumin authored
Now with one rule primitive we can prove several instances that allows us to eliminate  Fancy updates  Basic updates  Laters

 02 Dec, 2017 1 commit


Dan Frumin authored

 01 Dec, 2017 3 commits


Dan Frumin authored

Dan Frumin authored
{E,E;Δ,Γ} ⊨ ... => {E;Δ,Γ} ⊨ ... {⊤,⊤;Δ,Γ} ⊨ ... => {Δ,Γ} ⊨ ...

Dan Frumin authored

 29 Nov, 2017 4 commits


Dan Frumin authored

Dan Frumin authored

Dan Frumin authored

Dan Frumin authored

 27 Nov, 2017 1 commit


Dan Frumin authored

 23 Nov, 2017 1 commit


Dan Frumin authored

 21 Nov, 2017 1 commit


Dan Frumin authored

 08 Nov, 2017 1 commit


Dan Frumin authored

 07 Nov, 2017 1 commit


Dan Frumin authored
`decide` works much better because of the general lemmas and tacitcs

 30 Oct, 2017 2 commits


Dan Frumin authored
Add a pre_solve_closed ltac that basically changes the goal from `Closed X e` to `Closed ∅ e`. It is actually OK in practice.

Dan Frumin authored

 28 Oct, 2017 1 commit


Dan Frumin authored

 23 Oct, 2017 2 commits


Dan Frumin authored

Dan Frumin authored
 Involves bulling the partial bijection algebra from `runST`  Thanks to Amin for suggestions
