Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Iris
Iron
Commits
e9a9e56e
Commit
e9a9e56e
authored
Oct 31, 2018
by
Robbert Krebbers
Browse files
README tweaks.
parent
1a34a493
Changes
1
Hide whitespace changes
Inline
Sidebyside
README.md
View file @
e9a9e56e
...
...
@@ 30,9 +30,9 @@ Iron has been built and tested with the following dependencies
specific to this logic that are used later.

The machinery for connecting the generalized proofmode/MoSeL from to
fractional predicates is contained in
(theories/proofmode)
[theories/proofmode].
fractional predicates is contained in
[
theories/proofmode
]
(
theories/proofmode
)
.

In
(theories/iron_logic)
[theories/iron_logic] much of the core Iron logic

In
[
theories/iron_logic
]
(
theories/iron_logic
)
much of the core Iron logic
discussed in Section 2 is defined.
*
_Uniformity_ with respect to fractions is defined in
[
theories/iron_logic/iron.v
](
theories/iron_logic/iron.v
)
as
`Uniform`
and
...
...
@@ 48,7 +48,7 @@ Iron has been built and tested with the following dependencies
[
theories/heap_lang/heap.v
](
theories/heap_lang/heap.v
)
as
`heapG`
. So too
are the definitions of ↦ and 𝖊 (in the formalization called
`perm`
).
*
The theorems stated in Section 5 about updates to the heap ghost
state are proven in
(theories/heap_lang/heap.v)
[theories/heap_lang/heap.v].
state are proven in
[
theories/heap_lang/heap.v
]
(
theories/heap_lang/heap.v
)
.
*
The state interpretation from Section 5 is defined in
[
theories/heap_lang/heap.v
](
theories/heap_lang/heap.v
)
as
`heap_ctx`
.
*
Theorems 2.1, 2.2, 4.1, and 4.2 are proven in
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Attach a 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