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
David Swasey
derek-popl18-talk
Commits
29bd9d7f
Commit
29bd9d7f
authored
Jan 07, 2018
by
David Swasey
Browse files
Adjust README for the symbol ADT.
parent
3454e5c0
Changes
2
Hide whitespace changes
Inline
Side-by-side
README.md
View file @
29bd9d7f
# IRIS EXAMPLES
Some example verification demonstrating the use of Iris.
This is a fork of the
[
iris-examples
](
https://gitlab.mpi-sws.org/FP/iris-examples.git
)
repository formalizing the safety proof sketched in Derek Dreyer's
POPL '18 talk.
## Prerequisites
...
...
@@ -29,9 +32,54 @@ To update, do `git pull`. After an update, the development may fail to compile
because of outdated dependencies. To fix that, please run
`opam update`
followed by
`make build-dep`
.
## Derek's POPL '18 talk
This repository contains the safety proof sketched in Derek Dreyer's
POPL '18 talk. It is derived from
[
earlier
work
](
https://gitlab.mpi-sws.org/FP/iris-examples.git
)
accompanying
the
[
Iris proof mode
paper
](
http://doi.acm.org/10.1145/3093333.3009855
)
.
The language, type system, and logical relation we use are defined in
theories/logrel/F_mu_ref_conc/lang.v
theories/logrel/F_mu_ref_conc/typing.v
theories/logrel/F_mu_ref_conc/logrel_unary.v
The language is System F with recursive types, references,
concurrency, and an unsafe expression
`assert e`
that gets stuck
unless
`e`
evaluates to
`true`
. (An additional file,
`theories/logrel/F_mu_ref_conc/rules.v`
, derives some Iris proof rules
from the language's operational semantics.)
The relevant metatheorems are proved in
theories/logrel/F_mu_ref_conc/fundamental_unary.v
theories/logrel/F_mu_ref_conc/soundness_unary.v
These are the fundamental theorem of logical relations and a semantic
proof of type soundness.
The symbol ADT is verified in
theories/logrel/F_mu_ref_conc/examples/symbol.v
The goal is to show that a syntactically unsafe implementation of
symbols is semantically safe:
pack <int,
let c = ref 0 in
<λ_. c++,
λ_. assert(s < *c)>
as ∃α. (unit → α) × (α → unit)
∈ E[∃α. (unit → α) × (α → unit)]
This is lemma
`type_symbol`
in that file.
## Case Studies
This repository contains the following case studies:
This repository also contains several case studies, disabled in
`_CoqProject`
:
*
[
barrier
](
theories/barrier
)
: Implementation and proof of a barrier as
described in
[
"Higher-Order Ghost State"
](
http://doi.acm.org/10.1145/2818638
)
.
...
...
@@ -56,6 +104,16 @@ This repository contains the following case studies:
*
[
lecture-notes
](
theories/lecture_notes
)
: Coq examples for the
[
Iris lecture notes
](
http://iris-project.org/tutorial-material.html
)
.
If you are interested in these, we recommend that you find them in
[
the original iris-examples
repository
](
https://gitlab.mpi-sws.org/FP/iris-examples.git
)
. To
verify safety for the symbol ADT, we extended the language in
`F_mu_rec_conc`
with existential types, but we neither updated that
language's binary logical relation nor proved that relation compatible
with
`pack`
and
`unpack`
. This means that examples that rely on the
binary logical relation for
`F_mu_rec_conc`
no longer compile.
(Everything else would compile if enabled in
`_CoqProject`
.)
## For Developers: How to update the Iris dependency
*
Do the change in Iris, push it.
...
...
_CoqProject
View file @
29bd9d7f
-Q theories iris_examples
-arg -w -arg -notation-overridden,-redundant-canonical-projection,-several-object-files
theories/barrier/proof.v
theories/barrier/specification.v
theories/barrier/barrier.v
theories/barrier/protocol.v
theories/barrier/example_client.v
theories/barrier/example_joining_existentials.v
#
theories/barrier/proof.v
#
theories/barrier/specification.v
#
theories/barrier/barrier.v
#
theories/barrier/protocol.v
#
theories/barrier/example_client.v
#
theories/barrier/example_joining_existentials.v
theories/lecture_notes/coq_intro_example_1.v
#
theories/lecture_notes/coq_intro_example_1.v
theories/spanning_tree/graph.v
theories/spanning_tree/mon.v
theories/spanning_tree/spanning.v
theories/spanning_tree/proof.v
#
theories/spanning_tree/graph.v
#
theories/spanning_tree/mon.v
#
theories/spanning_tree/spanning.v
#
theories/spanning_tree/proof.v
theories/logrel/prelude/base.v
theories/logrel/stlc/lang.v
theories/logrel/stlc/typing.v
theories/logrel/stlc/rules.v
theories/logrel/stlc/logrel.v
theories/logrel/stlc/fundamental.v
theories/logrel/stlc/soundness.v
theories/logrel/F_mu/lang.v
theories/logrel/F_mu/typing.v
theories/logrel/F_mu/rules.v
theories/logrel/F_mu/logrel.v
theories/logrel/F_mu/fundamental.v
theories/logrel/F_mu/soundness.v
theories/logrel/F_mu_ref/lang.v
theories/logrel/F_mu_ref/typing.v
theories/logrel/F_mu_ref/rules.v
theories/logrel/F_mu_ref/rules_binary.v
theories/logrel/F_mu_ref/logrel.v
theories/logrel/F_mu_ref/logrel_binary.v
theories/logrel/F_mu_ref/fundamental.v
theories/logrel/F_mu_ref/fundamental_binary.v
theories/logrel/F_mu_ref/soundness.v
theories/logrel/F_mu_ref/context_refinement.v
theories/logrel/F_mu_ref/soundness_binary.v
#
theories/logrel/stlc/lang.v
#
theories/logrel/stlc/typing.v
#
theories/logrel/stlc/rules.v
#
theories/logrel/stlc/logrel.v
#
theories/logrel/stlc/fundamental.v
#
theories/logrel/stlc/soundness.v
#
theories/logrel/F_mu/lang.v
#
theories/logrel/F_mu/typing.v
#
theories/logrel/F_mu/rules.v
#
theories/logrel/F_mu/logrel.v
#
theories/logrel/F_mu/fundamental.v
#
theories/logrel/F_mu/soundness.v
#
theories/logrel/F_mu_ref/lang.v
#
theories/logrel/F_mu_ref/typing.v
#
theories/logrel/F_mu_ref/rules.v
#
theories/logrel/F_mu_ref/rules_binary.v
#
theories/logrel/F_mu_ref/logrel.v
#
theories/logrel/F_mu_ref/logrel_binary.v
#
theories/logrel/F_mu_ref/fundamental.v
#
theories/logrel/F_mu_ref/fundamental_binary.v
#
theories/logrel/F_mu_ref/soundness.v
#
theories/logrel/F_mu_ref/context_refinement.v
#
theories/logrel/F_mu_ref/soundness_binary.v
theories/logrel/F_mu_ref_conc/lang.v
theories/logrel/F_mu_ref_conc/rules.v
theories/logrel/F_mu_ref_conc/typing.v
theories/logrel/F_mu_ref_conc/logrel_unary.v
theories/logrel/F_mu_ref_conc/fundamental_unary.v
theories/logrel/F_mu_ref_conc/rules_binary.v
theories/logrel/F_mu_ref_conc/soundness_unary.v
#theories/logrel/F_mu_ref_conc/rules_binary.v
#theories/logrel/F_mu_ref_conc/logrel_binary.v
#theories/logrel/F_mu_ref_conc/fundamental_binary.v
theories/logrel/F_mu_ref_conc/soundness_unary.v
#theories/logrel/F_mu_ref_conc/context_refinement.v
#theories/logrel/F_mu_ref_conc/soundness_binary.v
theories/logrel/F_mu_ref_conc/examples/lock.v
#
theories/logrel/F_mu_ref_conc/examples/lock.v
#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
theories/logrel/F_mu_ref_conc/examples/symbol.v
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