Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Dan Frumin
ReLoC-v1
Commits
ab899eb7
Commit
ab899eb7
authored
May 28, 2016
by
Amin Timany
Browse files
Give a qualified name to the top-level development
parent
814b3e14
Changes
33
Hide whitespace changes
Inline
Side-by-side
F_mu/fundamental.v
View file @
ab899eb7
Require
Import
iris
.
program_logic
.
hoare
.
Require
Import
iris
.
program_logic
.
lifting
.
Require
Import
iris
.
algebra
.
upred_big_op
.
Require
Import
F_mu
.
lang
F_mu
.
typing
F_mu
.
rules
F_mu
.
logrel
.
Require
Import
iris_logrel
.
F_mu
.
lang
iris_logrel
.
F_mu
.
typing
iris_logrel
.
F_mu
.
rules
iris_logrel
.
F_mu
.
logrel
.
Import
uPred
.
Section
typed_interp
.
...
...
F_mu/lang.v
View file @
ab899eb7
Require
Export
prelude
.
base
.
Require
Export
iris_logrel
.
prelude
.
base
.
Require
Import
iris
.
program_logic
.
language
.
Require
Export
Autosubst
.
Autosubst
.
...
...
F_mu/logrel.v
View file @
ab899eb7
Require
Import
iris
.
program_logic
.
hoare
.
Require
Import
iris
.
program_logic
.
lifting
.
Require
Import
iris
.
algebra
.
upred_big_op
.
Require
Import
F_mu
.
lang
F_mu
.
typing
F_mu
.
rules
.
Require
Import
iris_logrel
.
F_mu
.
lang
iris_logrel
.
F_mu
.
typing
iris_logrel
.
F_mu
.
rules
.
Import
uPred
.
(
**
interp
:
is
a
unary
logical
relation
.
*
)
...
...
F_mu/rules.v
View file @
ab899eb7
Require
Import
iris
.
program_logic
.
lifting
.
Require
Import
iris
.
algebra
.
upred_big_op
.
Require
Import
F_mu
.
lang
.
Require
Import
iris_logrel
.
F_mu
.
lang
.
Section
lang_rules
.
...
...
F_mu/soundness.v
View file @
ab899eb7
...
...
@@ -2,7 +2,9 @@ Require Import iris.proofmode.tactics.
Require
Import
iris
.
program_logic
.
hoare
.
Require
Import
iris
.
program_logic
.
lifting
.
Require
Import
iris
.
algebra
.
upred_big_op
.
Require
Import
F_mu
.
lang
F_mu
.
typing
F_mu
.
rules
F_mu
.
logrel
F_mu
.
fundamental
.
Require
Import
iris_logrel
.
F_mu
.
lang
iris_logrel
.
F_mu
.
typing
iris_logrel
.
F_mu
.
rules
iris_logrel
.
F_mu
.
logrel
iris_logrel
.
F_mu
.
fundamental
.
Require
Import
iris
.
program_logic
.
adequacy
.
Import
uPred
.
...
...
F_mu/typing.v
View file @
ab899eb7
Require
Import
prelude
.
base
.
Require
Import
F_mu
.
lang
.
Require
Import
iris_logrel
.
prelude
.
base
.
Require
Import
iris_logrel
.
F_mu
.
lang
.
Inductive
type
:=
|
TUnit
:
type
...
...
F_mu_ref/fundamental.v
View file @
ab899eb7
Require
Import
iris
.
program_logic
.
hoare
.
Require
Import
iris
.
program_logic
.
lifting
.
Require
Import
iris
.
algebra
.
upred_big_op
.
Require
Import
F_mu_ref
.
lang
F_mu_ref
.
typing
F_mu_ref
.
rules
F_mu_ref
.
logrel
.
Require
Import
iris_logrel
.
F_mu_ref
.
lang
iris_logrel
.
F_mu_ref
.
typing
iris_logrel
.
F_mu_ref
.
rules
iris_logrel
.
F_mu_ref
.
logrel
.
From
iris
.
program_logic
Require
Export
lifting
.
From
iris
.
algebra
Require
Import
upred_big_op
frac
dec_agree
.
From
iris
.
program_logic
Require
Export
invariants
ghost_ownership
.
...
...
F_mu_ref/lang.v
View file @
ab899eb7
Require
Export
prelude
.
base
.
Require
Export
iris_logrel
.
prelude
.
base
.
Require
Import
iris
.
prelude
.
gmap
.
Require
Import
iris
.
program_logic
.
language
.
Require
Export
Autosubst
.
Autosubst
.
...
...
F_mu_ref/logrel.v
View file @
ab899eb7
Require
Import
iris
.
program_logic
.
hoare
.
Require
Import
iris
.
program_logic
.
lifting
.
Require
Import
iris
.
algebra
.
upred_big_op
.
Require
Import
F_mu_ref
.
lang
F_mu_ref
.
typing
F_mu_ref
.
rules
.
Require
Import
iris_logrel
.
F_mu_ref
.
lang
iris_logrel
.
F_mu_ref
.
typing
iris_logrel
.
F_mu_ref
.
rules
.
From
iris
.
program_logic
Require
Export
lifting
.
From
iris
.
algebra
Require
Import
upred_big_op
frac
dec_agree
.
From
iris
.
program_logic
Require
Export
invariants
ghost_ownership
.
...
...
F_mu_ref/rules.v
View file @
ab899eb7
Require
Import
iris
.
program_logic
.
lifting
.
Require
Import
iris
.
algebra
.
upred_big_op
.
Require
Import
F_mu_ref
.
lang
.
Require
Import
iris_logrel
.
F_mu_ref
.
lang
.
From
iris
.
program_logic
Require
Export
lifting
.
From
iris
.
algebra
Require
Import
upred_big_op
frac
dec_agree
.
From
iris
.
program_logic
Require
Export
invariants
ghost_ownership
.
...
...
F_mu_ref/soundness.v
View file @
ab899eb7
...
...
@@ -2,8 +2,9 @@ Require Import iris.proofmode.weakestpre iris.proofmode.tactics.
Require
Import
iris
.
program_logic
.
hoare
.
Require
Import
iris
.
program_logic
.
lifting
.
Require
Import
iris
.
algebra
.
auth
.
Require
Import
F_mu_ref
.
lang
F_mu_ref
.
typing
F_mu_ref
.
rules
F_mu_ref
.
logrel
F_mu_ref
.
fundamental
.
Require
Import
iris_logrel
.
F_mu_ref
.
lang
iris_logrel
.
F_mu_ref
.
typing
iris_logrel
.
F_mu_ref
.
rules
iris_logrel
.
F_mu_ref
.
logrel
iris_logrel
.
F_mu_ref
.
fundamental
.
Require
Import
iris
.
program_logic
.
adequacy
.
Import
uPred
.
...
...
F_mu_ref/typing.v
View file @
ab899eb7
Require
Import
prelude
.
base
.
Require
Import
F_mu_ref
.
lang
.
Require
Import
iris_logrel
.
prelude
.
base
.
Require
Import
iris_logrel
.
F_mu_ref
.
lang
.
Inductive
type
:=
|
TUnit
:
type
...
...
F_mu_ref_par/examples/counter.v
View file @
ab899eb7
From
iris
.
proofmode
Require
Import
invariants
ghost_ownership
tactics
.
From
F_mu_ref_par
Require
Import
lang
examples
.
lock
typing
From
iris_logrel
.
F_mu_ref_par
Require
Import
lang
examples
.
lock
typing
logrel_binary
fundamental_binary
rules_binary
rules
.
Import
uPred
.
...
...
F_mu_ref_par/examples/lock.v
View file @
ab899eb7
From
iris
.
proofmode
Require
Import
invariants
ghost_ownership
tactics
.
From
F_mu_ref_par
Require
Import
lang
rules
rules_binary
typing
.
From
iris_logrel
.
F_mu_ref_par
Require
Import
lang
rules
rules_binary
typing
.
Import
uPred
.
Definition
newlock
:
expr
:=
Alloc
(
♭
false
).
...
...
F_mu_ref_par/examples/stack/CG_stack.v
View file @
ab899eb7
From
iris
.
proofmode
Require
Import
invariants
ghost_ownership
tactics
.
From
F_mu_ref_par
Require
Import
lang
examples
.
lock
typing
From
iris_logrel
.
F_mu_ref_par
Require
Import
lang
examples
.
lock
typing
logrel_binary
fundamental_binary
rules_binary
rules
.
Import
uPred
.
...
...
F_mu_ref_par/examples/stack/stack_rules.v
View file @
ab899eb7
From
iris
.
proofmode
Require
Import
invariants
ghost_ownership
tactics
.
From
F_mu_ref_par
Require
Import
lang
rules
logrel_binary
.
From
iris_logrel
.
F_mu_ref_par
Require
Import
lang
rules
logrel_binary
.
From
iris
.
algebra
Require
Import
gmap
dec_agree
auth
upred_big_op
.
From
iris
.
program_logic
Require
Import
ownership
auth
.
Import
uPred
.
...
...
F_mu_ref_par/fundamental_binary.v
View file @
ab899eb7
Require
Import
iris
.
program_logic
.
hoare
.
Require
Import
iris
.
program_logic
.
lifting
.
Require
Import
iris
.
algebra
.
upred_big_op
.
Require
Import
F_mu_ref_par
.
lang
F_mu_ref_par
.
typing
F_mu_ref_par
.
rules
F_mu_ref_par
.
rules_binary
F_mu_ref_par
.
logrel_binary
.
Require
Import
iris_logrel
.
F_mu_ref_par
.
lang
iris_logrel
.
F_mu_ref_par
.
typing
iris_logrel
.
F_mu_ref_par
.
rules
iris_logrel
.
F_mu_ref_par
.
rules_binary
iris_logrel
.
F_mu_ref_par
.
logrel_binary
.
From
iris
.
program_logic
Require
Export
lifting
.
From
iris
.
algebra
Require
Import
upred_big_op
frac
dec_agree
.
From
iris
.
program_logic
Require
Export
invariants
ghost_ownership
.
...
...
F_mu_ref_par/fundamental_unary.v
View file @
ab899eb7
Require
Import
iris
.
program_logic
.
hoare
.
Require
Import
iris
.
program_logic
.
lifting
.
Require
Import
iris
.
algebra
.
upred_big_op
.
Require
Import
F_mu_ref_par
.
lang
F_mu_ref_par
.
typing
F_mu_ref_par
.
rules
F_mu_ref_par
.
logrel_unary
.
Require
Import
iris_logrel
.
F_mu_ref_par
.
lang
iris_logrel
.
F_mu_ref_par
.
typing
iris_logrel
.
F_mu_ref_par
.
rules
iris_logrel
.
F_mu_ref_par
.
logrel_unary
.
From
iris
.
program_logic
Require
Export
lifting
.
From
iris
.
algebra
Require
Import
upred_big_op
frac
dec_agree
.
From
iris
.
program_logic
Require
Export
invariants
ghost_ownership
.
...
...
F_mu_ref_par/lang.v
View file @
ab899eb7
Require
Export
prelude
.
base
.
Require
Export
iris_logrel
.
prelude
.
base
.
Require
Import
iris
.
prelude
.
gmap
.
Require
Import
iris
.
program_logic
.
language
.
Require
Export
Autosubst
.
Autosubst
.
...
...
F_mu_ref_par/logrel_binary.v
View file @
ab899eb7
Require
Import
iris
.
program_logic
.
hoare
.
Require
Import
iris
.
program_logic
.
lifting
.
Require
Import
iris
.
algebra
.
upred_big_op
.
Require
Import
F_mu_ref_par
.
lang
F_mu_ref_par
.
typing
F_mu_ref_par
.
rules
F_mu_ref_par
.
rules_binary
.
Require
Import
iris_logrel
.
F_mu_ref_par
.
lang
iris_logrel
.
F_mu_ref_par
.
typing
iris_logrel
.
F_mu_ref_par
.
rules
iris_logrel
.
F_mu_ref_par
.
rules_binary
.
From
iris
.
program_logic
Require
Export
lifting
.
From
iris
.
algebra
Require
Import
upred_big_op
frac
dec_agree
.
From
iris
.
program_logic
Require
Export
invariants
ghost_ownership
.
...
...
Prev
1
2
Next
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment