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
examples
Commits
c3a8a2a3
Commit
c3a8a2a3
authored
Dec 14, 2017
by
Ralf Jung
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
README; trailing newline
parent
9bad5ed7
Pipeline
#5936
passed with stage
in 9 minutes and 33 seconds
Changes
2
Pipelines
1
Hide whitespace changes
Inline
Side-by-side
Showing
2 changed files
with
5 additions
and
4 deletions
+5
-4
README.md
README.md
+4
-3
_CoqProject
_CoqProject
+1
-1
No files found.
README.md
View file @
c3a8a2a3
...
...
@@ -28,9 +28,10 @@ Run `make` to build the full development.
This repository contains the following case studies:
*
[
barrier
](
theories/barrier
)
: The implementation and proof of a barrier as
described in "Higher-Order 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>
:
*
[
barrier
](
theories/barrier
)
: Implementation and proof of a barrier as
described in
[
"Higher-Order Ghost State"
](
http://doi.acm.org/10.1145/2818638
)
.
*
[
logrel
](
theories/logrel
)
: Logical relations from the
[
IPM paper
](
http://doi.acm.org/10.1145/3093333.3009855
)
:
-
STLC
*
Unary logical relations proving type safety
-
F_mu (System F with recursive types)
...
...
_CoqProject
View file @
c3a8a2a3
...
...
@@ -47,4 +47,4 @@ theories/logrel/F_mu_ref_conc/examples/counter.v
theories/logrel/F_mu_ref_conc/examples/stack/stack_rules.v
theories/logrel/F_mu_ref_conc/examples/stack/CG_stack.v
theories/logrel/F_mu_ref_conc/examples/stack/FG_stack.v
theories/logrel/F_mu_ref_conc/examples/stack/refinement.v
\ No newline at end of file
theories/logrel/F_mu_ref_conc/examples/stack/refinement.v
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