Commit e378869b authored by Amin Timany's avatar Amin Timany

Change F_mu_ref_par to F_mu_ref_conc

parent 958678fb
From iris_logrel.F_mu_ref_par Require Export fundamental_binary.
From iris_logrel.F_mu_ref_conc Require Export fundamental_binary.
Inductive ctx_item :=
| CTX_Rec
......
From iris.proofmode Require Import invariants ghost_ownership tactics.
From iris_logrel.F_mu_ref_par Require Export examples.lock.
From iris_logrel.F_mu_ref_par Require Import soundness_binary.
From iris_logrel.F_mu_ref_conc Require Export examples.lock.
From iris_logrel.F_mu_ref_conc Require Import soundness_binary.
Definition CG_increment (x : expr) : expr :=
Rec (Store x.[ren (+ 2)] (BinOp Add ( 1) (Load x.[ren (+ 2)]))).
......
From iris.proofmode Require Import invariants ghost_ownership tactics.
From iris_logrel.F_mu_ref_par Require Export rules_binary typing.
From iris_logrel.F_mu_ref_conc Require Export rules_binary typing.
Definition newlock : expr := Alloc ( false).
Definition acquire : expr :=
......
From iris.proofmode Require Import invariants ghost_ownership tactics.
From iris_logrel.F_mu_ref_par Require Import examples.lock.
From iris_logrel.F_mu_ref_conc Require Import examples.lock.
Import uPred.
Definition CG_StackType τ :=
......
From iris_logrel.F_mu_ref_par Require Import typing.
From iris_logrel.F_mu_ref_conc Require Import typing.
Definition FG_StackType τ :=
TRec (Tref (TSum TUnit (TProd τ.[ren (+1)] (TVar 0)))).
......
From iris.program_logic Require Import auth.
From iris_logrel.F_mu_ref_par Require Import soundness_binary.
From iris_logrel.F_mu_ref_par.examples Require Import lock.
From iris_logrel.F_mu_ref_par.examples.stack Require Import
From iris_logrel.F_mu_ref_conc Require Import soundness_binary.
From iris_logrel.F_mu_ref_conc.examples Require Import lock.
From iris_logrel.F_mu_ref_conc.examples.stack Require Import
CG_stack FG_stack stack_rules.
From iris.proofmode Require Import invariants ghost_ownership tactics.
......
From iris.proofmode Require Import invariants ghost_ownership tactics.
From iris_logrel.F_mu_ref_par Require Import logrel_binary.
From iris_logrel.F_mu_ref_conc Require Import logrel_binary.
From iris.algebra Require Import gmap dec_agree.
From iris.program_logic Require Import auth.
Import uPred.
......
From iris_logrel.F_mu_ref_par Require Export logrel_binary.
From iris_logrel.F_mu_ref_conc Require Export logrel_binary.
From iris.proofmode Require Import tactics pviewshifts invariants.
From iris_logrel.F_mu_ref_par Require Import rules_binary.
From iris_logrel.F_mu_ref_conc Require Import rules_binary.
From iris.algebra Require Export upred_big_op.
Section bin_log_def.
......
From iris_logrel.F_mu_ref_par Require Export logrel_unary.
From iris_logrel.F_mu_ref_par Require Import rules.
From iris_logrel.F_mu_ref_conc Require Export logrel_unary.
From iris_logrel.F_mu_ref_conc Require Import rules.
From iris.algebra Require Export upred_big_op.
From iris.proofmode Require Import tactics pviewshifts invariants.
......
From iris.proofmode Require Import tactics.
From iris.program_logic Require Export weakestpre.
From iris_logrel.F_mu_ref_par Require Export rules_binary typing.
From iris_logrel.F_mu_ref_conc Require Export rules_binary typing.
Import uPred.
(* HACK: move somewhere else *)
......
From iris.proofmode Require Import tactics.
From iris.program_logic Require Export weakestpre.
From iris_logrel.F_mu_ref_par Require Export rules typing.
From iris_logrel.F_mu_ref_conc Require Export rules typing.
Import uPred.
Definition logN : namespace := nroot .@ "logN".
......
......@@ -3,7 +3,7 @@ From iris.program_logic Require Export weakestpre global_functor invariants.
From iris.program_logic Require Import lifting.
From iris.algebra Require Import upred_big_op frac dec_agree.
From iris.program_logic Require Import ownership auth.
From iris_logrel.F_mu_ref_par Require Export lang.
From iris_logrel.F_mu_ref_conc Require Export lang.
Import uPred.
Definition heapN : namespace := nroot .@ "heap".
......
From iris.program_logic Require Import lifting.
From iris.algebra Require Import upred_big_op frac dec_agree.
From iris.program_logic Require Import ownership auth.
From iris_logrel.F_mu_ref_par Require Export rules.
From iris_logrel.F_mu_ref_conc Require Export rules.
From iris.proofmode Require Import tactics weakestpre invariants.
Import uPred.
......
From iris_logrel.F_mu_ref_par Require Export context_refinement.
From iris_logrel.F_mu_ref_conc Require Export context_refinement.
From iris.algebra Require Import upred_big_op frac dec_agree.
From iris.program_logic Require Import ownership auth.
From iris.proofmode Require Import tactics pviewshifts invariants.
......
From iris_logrel.F_mu_ref_par Require Export fundamental_unary.
From iris_logrel.F_mu_ref_conc Require Export fundamental_unary.
From iris.proofmode Require Import tactics pviewshifts.
From iris.program_logic Require Import ownership adequacy auth.
......
From iris_logrel.F_mu_ref_par Require Export lang.
From iris_logrel.F_mu_ref_conc Require Export lang.
Inductive type :=
| TUnit : type
......
......@@ -18,20 +18,20 @@ F_mu_ref/rules.v
F_mu_ref/logrel.v
F_mu_ref/fundamental.v
F_mu_ref/soundness.v
F_mu_ref_par/lang.v
F_mu_ref_par/rules.v
F_mu_ref_par/typing.v
F_mu_ref_par/logrel_unary.v
F_mu_ref_par/fundamental_unary.v
F_mu_ref_par/rules_binary.v
F_mu_ref_par/logrel_binary.v
F_mu_ref_par/fundamental_binary.v
F_mu_ref_par/soundness_unary.v
F_mu_ref_par/context_refinement.v
F_mu_ref_par/soundness_binary.v
F_mu_ref_par/examples/lock.v
F_mu_ref_par/examples/counter.v
F_mu_ref_par/examples/stack/stack_rules.v
F_mu_ref_par/examples/stack/CG_stack.v
F_mu_ref_par/examples/stack/FG_stack.v
F_mu_ref_par/examples/stack/refinement.v
\ No newline at end of file
F_mu_ref_conc/lang.v
F_mu_ref_conc/rules.v
F_mu_ref_conc/typing.v
F_mu_ref_conc/logrel_unary.v
F_mu_ref_conc/fundamental_unary.v
F_mu_ref_conc/rules_binary.v
F_mu_ref_conc/logrel_binary.v
F_mu_ref_conc/fundamental_binary.v
F_mu_ref_conc/soundness_unary.v
F_mu_ref_conc/context_refinement.v
F_mu_ref_conc/soundness_binary.v
F_mu_ref_conc/examples/lock.v
F_mu_ref_conc/examples/counter.v
F_mu_ref_conc/examples/stack/stack_rules.v
F_mu_ref_conc/examples/stack/CG_stack.v
F_mu_ref_conc/examples/stack/FG_stack.v
F_mu_ref_conc/examples/stack/refinement.v
\ No newline at end of file
......@@ -45,4 +45,4 @@ Ltac solve_proper_alt :=
Reserved Notation "⟦ τ ⟧" (at level 0, τ at level 70).
Reserved Notation "⟦ τ ⟧ₑ" (at level 0, τ at level 70).
Reserved Notation "⟦ Γ ⟧*" (at level 0, Γ at level 70).
\ No newline at end of file
Reserved Notation "⟦ Γ ⟧*" (at level 0, Γ at level 70).
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