Commit 21f897d7 authored by Dan Frumin's avatar Dan Frumin

Add the typesafety proof

parent 4bbf89ee
From iris_logrel.F_mu_ref_conc Require Export context_refinement adequacy.
From iris_logrel.F_mu_ref_conc Require Export context_refinement adequacy fundamental_binary.
From iris.algebra Require Import auth frac agree.
From iris.base_logic Require Import big_op lib.auth.
From iris.proofmode Require Import tactics.
......@@ -62,6 +62,17 @@ Proof.
eapply logrel_adequate; eauto.
Qed.
Theorem F_mu_ref_conc_typesfety e e' τ σ thp σ' :
⊢ₜ e : τ
rtc step ([e], σ) (thp, σ') e' thp
is_Some (to_val e') reducible e' σ'.
Proof.
intros.
eapply (logrel_typesafety logrelΣ []); eauto.
intros.
by apply binary_fundamental.
Qed.
Lemma logrel_simul Σ `{logrelPreG Σ}
Δ e e' τ v thp hp :
( `{logrelG Σ}, {,;Δ;} e log e' : τ)
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment