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
Arthur Azevedo de Amorim
Tutorial POPL20
Commits
1f7813e0
Commit
1f7813e0
authored
Jan 20, 2020
by
Robbert Krebbers
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Work on README.
parent
76bf7fcf
Changes
1
Hide whitespace changes
Inline
Sidebyside
Showing
1 changed file
with
105 additions
and
0 deletions
+105
0
README.md
README.md
+105
0
No files found.
README.md
0 → 100644
View file @
1f7813e0
# The Iris tutorial @ POPL'20
This tutorial comes in two versions:

The folder
`exercises`
: skeletons of the exercises with solutions left out.

The folder
`solutions`
: the exercises together with their solutions.
## Dependencies
For the tutorial material you need to have the following dependencies installed:

Coq 8.8.2 / 8.9.1 / 8.10.1

A development version of
[
Iris
](
https://gitlab.mpisws.org/iris/iris
)
*Note:*
the tutorial material will not work with earlier versions of Iris, it
is important to install the exact versions as given above.
## Installing Iris via opam
The easiest, and recommend, way of installing Iris and its dependencies is via
the OCaml package manager opam (2.0.0 or newer). You first have to add the Coq
opam repository and the Iris development repository (if you have not already
done so earlier):
opam repo add coqreleased https://coq.inria.fr/opam/released
opam repo add irisdev https://gitlab.mpisws.org/iris/opam.git
Then you can do
`make builddep`
to install exactly the right version of Iris.
## Compiling the exercises
Run
`make`
to compile the exercises.
## Overview
Introduction to Iris and the HeapLang language:

[
solutions/language.v
](
language.v
)
: An introduction to Iris's HeapLang
language, program specifications using weakest preconditions, and proofs of
these specifications using Iris's tactics for separation logic.

[
solutions/polymorphism.v
](
polymorphism.v
)
: The encoding of polymorphic
functions and existential packages in HeapLang.
Syntactic typing:

[
solutions/types.v
](
types.v
)
: The definition of syntactic types and the
typelevel substitution function.

[
solutions/typed.v
](
typed.v
)
: The syntactic typing judgment.
Semantic typing:

[
solutions/sem_types.v
](
sem_types.v
)
: The model of semantic types in Iris.

[
solutions/sem_typed.v
](
sem_typed.v
)
: The definition of the semantic typing
judgment in Iris.

[
solutions/sem_type_formers.v
](
sem_type_formers.v
)
: The definition of the
semantic counterparts of the type formers (like products, sums, functions,
references, etc.).

[
solutions/sem_operators.v
](
sem_operators.v
)
: The judgment for semantic
operator typing and proofs of the corresponding semantic rules.

[
solutions/compatibility.v
](
compatibility.v
)
: The semantic typing rules, i.e.,
the compatibility lemmas.

[
solutions/interp.v
](
interp.v
)
: The interpretation of syntactic types in terms
of semantic types.

[
solutions/fundamental.v
](
fundamental.v
)
: The
*fundamental theorem*
*
, which
states that any syntactically typed program is semantically typed..

[
solutions/safety.v
](
safety.v
)
: Proofs of semantic and syntactic type safety.

[
solutions/unsafe.v
](
unsafe.v
)
: Proofs of "unsafe" programs, i.e. programs
that are not syntactically typed, but can be proved to be semantically safe.

[
solutions/parametricity.v
](
parametricity.v
)
: The use of the semantic typing
for proving parametricity results.
Ghost theory for semantic safety of "unsafe" programs:

[
solutions/two_state_ghost.v
](
two_state_ghost.v
)
: The ghost theory for a
transition system with two states.

[
solutions/symbol_ghost.v
](
symbol_ghost.v
)
: The ghost theory for the symbol
ADT example.
Other:

[
solutions/demo.v
](
demo.v
)
: A simplified version of the development to the
simplified case, as shown during the lecture at the POPL'20 tutorial.
## Documentation
The files [
`proof_mode.md`
] and [
`heap_lang.md`
] in the Iris repository contain a
list of the Iris Proof Mode tactics as well as the specialized tactics for
reasoning about HeapLang programs.
[
`proof_mode.md`
]:
https://gitlab.mpisws.org/iris/iris/blob/master/docs/proof_mode.md
[
`heap_lang.md`
]:
https://gitlab.mpisws.org/iris/iris/blob/master/docs/heap_lang.md
If you would like to know more about Iris, we recommend to take a look at:

http://irisproject.org/tutorialmaterial.html
Lecture Notes on Iris: HigherOrder Concurrent Separation Logic
Lars Birkedal and Aleš Bizjak
Used for an MSc course on concurrent separation logic at Aarhus University

https://www.mpisws.org/~dreyer/papers/irisgroundup/paper.pdf
Iris from the Ground Up: A Modular Foundation for HigherOrder Concurrent
Separation Logic
Ralf Jung, Robbert Krebbers, JacquesHenri Jourdan, Aleš Bizjak, Lars
Birkedal, Derek Dreyer.
A detailed description of the Iris logic and its model
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