Abstract Actor Confluence

[Aqissiaq]

A possible direction/extension would be proving confluence "once and for all" for abstract actor systems, and then instantiating for ABS. The idea is to use the proof in Appendix A of this paper.

Here an actor is given by a local state, a local multiset of messages and a (partial) transition function that may emit a message, and the global semantics allow for

• local steps by the transition function
• popping and processing a message

In the branch abstract-actors there is a functorial implementation of the abstract proof (theories/abstract_confluence.v) and an instantiation for some very simple actor theories (theories/simple_confluence.v).