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
Fengmin Zhu
Tutorial POPL20
Commits
d91bbf1d
Commit
d91bbf1d
authored
Jan 20, 2020
by
Robbert Krebbers
Browse files
Update links in README.
parent
fe406700
Changes
1
Hide whitespace changes
Inline
Sidebyside
Showing
1 changed file
with
17 additions
and
17 deletions
+17
17
README.md
README.md
+17
17
No files found.
README.md
View file @
d91bbf1d
...
...
@@ 35,50 +35,50 @@ Run `make` to compile the exercises.
Introduction to Iris and the HeapLang language:

[
language.v
](
solution
s/language.v
)
: An introduction to Iris's HeapLang

[
language.v
](
exercise
s/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.

[
polymorphism.v
](
solution
s/polymorphism.v
)
: The encoding of polymorphic

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

[
types.v
](
solution
s/types.v
)
: The definition of syntactic types and the

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

[
typed.v
](
solution
s/typed.v
)
: The syntactic typing judgment.

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

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

[
sem_typed.v
](
solution
s/sem_typed.v
)
: The definition of the semantic typing

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

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

[
sem_type_formers.v
](
solution
s/sem_type_formers.v
)
: The definition of the

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

[
sem_operators.v
](
solution
s/sem_operators.v
)
: The judgment for semantic

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

[
compatibility.v
](
solution
s/compatibility.v
)
: The semantic typing rules, i.e.,

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

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

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

[
fundamental.v
](
solution
s/fundamental.v
)
: The
*fundamental theorem*
, which

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

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

[
unsafe.v
](
solution
s/unsafe.v
)
: Proofs of "unsafe" programs, i.e. programs

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

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

[
parametricity.v
](
solution
s/parametricity.v
)
: The use of the semantic typing

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

[
two_state_ghost.v
](
solution
s/two_state_ghost.v
)
: The ghost theory for a

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

[
symbol_ghost.v
](
solution
s/symbol_ghost.v
)
: The ghost theory for the symbol

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

[
demo.v
](
solution
s/demo.v
)
: A simplified version of the development to the

[
demo.v
](
exercise
s/demo.v
)
: A simplified version of the development to the
simplified case, as shown during the lecture at the POPL'20 tutorial.
## Documentation
...
...
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