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
Iris
examples
Commits
4afbed2e
Commit
4afbed2e
authored
Dec 15, 2017
by
Ralf Jung
Browse files
README
parent
f4246d3a
Pipeline
#5941
passed with stage
in 5 minutes and 56 seconds
Changes
1
Pipelines
1
Hide whitespace changes
Inline
Side-by-side
README.md
View file @
4afbed2e
...
...
@@ -42,10 +42,12 @@ This repository contains the following case studies:
-
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 fine-grained/coarse-grained concurrent counter implementations
-
Proof of refinement for a pair of fine-grained/coarse-grained concurrent stack implementations
*
[
spanning-tree
](
theories/spanning_tree
)
: Proof of partial functional
correctness of a concurrent spanning tree algorithm.
-
Proof of refinement for a pair of fine-grained/coarse-grained concurrent
counter implementations
-
Proof of refinement for a pair of fine-grained/coarse-grained concurrent
stack implementations
*
[
spanning-tree
](
theories/spanning_tree
)
: Proof of a concurrent spanning tree
algorithm.
## For Developers: How to update the Iris dependency
...
...
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