5. The π-calculus in binding bigraphs
The monadic π-calculus with replicated input, encoded after Jensen (Mobile
Processes in Bigraphs, 2006, Ch. 6–7) in pure bigraphs over a signature with
binding ports, every encoding obeying Jensen's scope rule: structural
congruence and reduction of processes are compared with equality and
reaction of their encodings.
Symbols are those of the Notation chapter. Everything else is in Pi/:
substitution and free names (Calculus.lean), the signature and the shapes
of processes (Sig.lean, Enc.lean), the two rules and the proof of
soundness (Sound.lean), prenex forms and completeness (Canon.lean,
Iff.lean, Complete.lean), and Jensen's pair of replicated processes
(Calculus.lean, Examples.lean).