Hi, I would like to request comments on something that I've been working on.
πDILL is a type system based on intuitionistic linear logic, formulated in the dual context-style: https://doi.org/10.1017/S0960129514000218
In this PR I tried to write down the interpretation for this system using heap_lang (instead of pi-calculus), and interpret the types with Actris channels.
Why I thought this might be interesting?
- I wanted to learn Actris
- The type system fundamentally requires higher-order channels (something that is well supported in Actris)
- It shows an example of "non-manifest" sharing, where one endpoint (a "server") is shared among clients, but all the client-server interactions are totally disjoint from each other.
Overview of changes in this PR:
- Some facts about substitutions; the
is_closed_expr_setwas taken from ReLoC. - A lemma about
big_sepM2. - In order to implement this "non-manifest sharing" (for the interpretation of
! Atypes) I had to tweak the iProto_owns definition and formulate a log-atomic style specifications for thesendoperation.
I think the first two items are orthogonal to Actris/DILL so it might sense to see if those results can be generalized and move upstream.