Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Iris
examples
Commits
90d27fc2
Commit
90d27fc2
authored
Dec 14, 2017
by
Ralf Jung
Browse files
no tabs
parent
5d574803
Pipeline
#5934
canceled with stage
in 1 minute and 50 seconds
Changes
1
Pipelines
2
Hide whitespace changes
Inline
Sidebyside
Showing
1 changed file
with
12 additions
and
12 deletions
+12
12
README.md
README.md
+12
12
No files found.
README.md
View file @
90d27fc2
...
...
@@ 31,18 +31,18 @@ This repository contains the following case studies:
*
[
barrier
](
theories/barrier
)
: The implementation and proof of a barrier as
described in "HigherOrder Ghost State"
<http://doi.acm.org/10.1145/2818638>
.
*
[
logrel
](
theories/logrel
)
: the following logical relations from the paper
<http://doi.acm.org/10.1145/3093333.3009855>
:
*
STLC
*
Unary logical relations proving type safety
*
F_mu (System F with recursive types)
*
Unary logical relations proving type safety
*
F_mu_ref (System F with recursive types and references)
*
Unary logical relations proving type safety
*
Binary logical relations for proving contextual refinements
*
F_mu_ref_conc (System F with recursive types, references and concurrency)
*
Unary logical relations proving type safety
*
Binary logical relations for proving contextual refinements
*
Proof of refinement for a pair of finegrained/coarsegrained concurrent counter implementations
*
Proof of refinement for a pair of finegrained/coarsegrained concurrent stack implementations

STLC
*
Unary logical relations proving type safety

F_mu (System F with recursive types)
*
Unary logical relations proving type safety

F_mu_ref (System F with recursive types and references)
*
Unary logical relations proving type safety
*
Binary logical relations for proving contextual refinements

F_mu_ref_conc (System F with recursive types, references and concurrency)
*
Unary logical relations proving type safety
*
Binary logical relations for proving contextual refinements

Proof of refinement for a pair of finegrained/coarsegrained concurrent counter implementations

Proof of refinement for a pair of finegrained/coarsegrained concurrent stack implementations
## For Developers: How to update the Iris dependency
...
...
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