CPP21.md

Code corresponding to the paper

All code corresponding to the paper can be found in the directory theories/logrel. The file 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
• 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 an implicit variable 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 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: 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: 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. The definition of the list type and the weakest precondition for llength can be found in theories/logrel/lib/list.v It is type checked using a manual typing proof.