Skip to content

WIP: Interpretation of πDILL

Dan Frumin requested to merge dfrumin/actris:ill into master

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:

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_set was taken from ReLoC.
  • A lemma about big_sepM2.
  • In order to implement this "non-manifest sharing" (for the interpretation of ! A types) I had to tweak the iProto_owns definition and formulate a log-atomic style specifications for the send operation.

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.

Merge request reports