Commit 698be0b8 authored by Jonas Kastberg's avatar Jonas Kastberg

Added difference of ground type encoding

parent ccf977d9
Pipeline #27939 passed with stage
in 5 minutes and 48 seconds
## Differences
The semantic encoding of ground types use existential quantification in the
mechanisation (e.g. `λ w. ∃ (x:Z), w = int`, while the paper uses set
inclusion (e.g. `λ w. w ∈ Z`). The definitions are effectively identical.
## Examples
The parallel receive example in Section 4 can be found in
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment