Newer
Older
The state of the repository at the time of submission can be found at
[https://gitlab.mpi-sws.org/iris/actris/-/tree/cpp21](https://gitlab.mpi-sws.org/iris/actris/-/tree/cpp21)
# Code corresponding to the paper
All code corresponding to the paper can be found in the directory
[theories/logrel](../theories/logrel). The file [README.md](../README.md)
contains an overview of the files in that directory.
# Differences between the paper and the mechanisation
- The semantic encoding of ground types use existential quantification in the
mechanization (e.g., `λ w. ∃ (x:Z), w = int`, while the paper uses set
inclusion (e.g., `λ w. w ∈ Z`). The definitions are effectively identical.
- Polymorphism in the paper is written over the type kinds, e.g., `∀ (X : k).A`,
whereas that is written `∀ (X : lty k Σ). A` in Coq. This notation is used to
for technical reasoning. The underlying definitions are the same between
Coq and the paper.
- The polymorphic session types are defined in an nested fashion, as a sequence
of quantifiers, followed by the actual type, for mechanisation purposes
using telescopes. The definitions are effectively identical to the paper.
- The typing rule for branching (`ltyped_branch`) is written as a function
instead of an n-ary rule with multiple premises.
- The disjunction of the compute client invariant is encoded using a boolean
flag, as it makes mechanisation easier.
- The mechanisation employs a typing judgement for values (`ltyped_val`),
for technical reasons. More details on this is found in
[theories/logrel/term_typing_judgment.v](../theories/logrel/term_typing_judgment.v)
- Minor simplifications have been made for the displayed Coq code of Section 5,
such as assuming that implicit variables (e.g., `{!heapG Σ}`) are available from
a `Context`, rather than as implicits variables of the definitions.
The definitions between the paper and Coq code are identical,
as this is just refactoring.
# Examples
- The compute service example in Section 3 can be found in
[theories/logrel/examples/compute_service.v](../theories/logrel/examples/compute_service.v)
The program recursively receive computation requests, which it computes and
then send back. It is entirely type checked with the rules of the type system
- The parallel receive example in Section 4 can be found in
[theories/logrel/examples/par_recv.v](../theories/logrel/examples/par_recv.v):
This program performs two "racy" parallel receives on the same channel from
two different threads, using locks to allow the channel to be shared.
- The parallel compute client example in Section 4 can be found in
[theories/logrel/examples/compute_client_list.v](../theories/logrel/examples/compute_client_list.v):
This program sends computation requests and receives their results in parallel,
analogous to the producer-consumer pattern. It uses a lock to share the channel
and a shared counter, that keeps track of the number of computations in transit.
The computation service can be found in
[theories/logrel/examples/compute_service.v](../theories/logrel/examples/compute_service.v).
The definition of the list type and the weakest precondition for `llength`
can be found in [theories/logrel/lib/list.v](../theories/logrel/lib/list.v)
It is type checked using a manual typing proof.