Library iris.chan2heap.compiler_correctness

From iris.chan2heap Require Import simple_reln chan2heap.

Theorem compiler_correctness ty ec:
  has_typ ∅ ec ty →
  safe_refine (c2h_refine) (c2h ec) ∅ ec ∅.
Proof.
  intros. eapply soundness.
  intros. eapply fundamental.
  eauto.
Qed.

Print Assumptions compiler_correctness.