Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
What's new
10
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Open sidebar
Iris
Iris
Commits
2a1db329
Commit
2a1db329
authored
Oct 26, 2016
by
Ralf Jung
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
README: update for base_logic folder
parent
e224e891
Pipeline
#2899
passed with stage
in 9 minutes and 25 seconds
Changes
1
Pipelines
1
Hide whitespace changes
Inline
Side-by-side
Showing
1 changed file
with
9 additions
and
4 deletions
+9
-4
README.md
README.md
+9
-4
No files found.
README.md
View file @
2a1db329
...
@@ -32,9 +32,13 @@ running:
...
@@ -32,9 +32,13 @@ running:
Robbert Krebbers
<http://robbertkrebbers.nl/thesis.html>
.
Robbert Krebbers
<http://robbertkrebbers.nl/thesis.html>
.
*
The folder
[
algebra
](
algebra
)
contains the COFE and CMRA constructions as well
*
The folder
[
algebra
](
algebra
)
contains the COFE and CMRA constructions as well
as the solver for recursive domain equations.
as the solver for recursive domain equations.
*
The folder
[
program_logic
](
program_logic
)
builds the semantic domain of Iris,
*
The folder
[
base_logic
](
base_logic
)
defines the Iris base logic and the
defines and verifies primitive view shifts and weakest preconditions, and
primitive connectives. It also contains derived constructions that are
builds some language-independent derived constructions (e.g., STSs).
entirely independent of the choice of resources.
*
The folder
[
program_logic
](
program_logic
)
specializes the base logic to build
Iris, the program logic. Most crucially, this includes world satisfaction
and weakest preconditions. Furthermore, some language-independent derived
constructions (e.g., STSs) are defined in this folder.
*
The folder
[
heap_lang
](
heap_lang
)
defines the ML-like concurrent heap language
*
The folder
[
heap_lang
](
heap_lang
)
defines the ML-like concurrent heap language
*
The subfolder
[
lib
](
heap_lang/lib
)
contains a few derived constructions
*
The subfolder
[
lib
](
heap_lang/lib
)
contains a few derived constructions
within this language, e.g., parallel composition.
within this language, e.g., parallel composition.
...
@@ -51,4 +55,5 @@ running:
...
@@ -51,4 +55,5 @@ running:
## Documentation
## Documentation
A LaTeX version of the core logic definitions and some derived forms is
A LaTeX version of the core logic definitions and some derived forms is
available in
[
docs/iris.tex
](
docs/iris.tex
)
.
available in
[
docs/iris.tex
](
docs/iris.tex
)
. A compiled PDF version of this
document is
[
http://plv.mpi-sws.org/iris/appendix-3.0.pdf
](
available
online).
Write
Preview
Markdown
is supported
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