Process calculi

Stream: CSLib

[Fabrizio Montesi]

Creating a topic to discuss efforts on process calculi.

[Fabrizio Montesi]

@Pieter Cuijpers I think recruiting students to work on process calculi/algebra sounds great. A few pointers:

• We do have an LTS module, see https://cs-lean.github.io/Cslib/Foundations/Semantics/LTS/Basic.html. It has the signature you expect (State → Label → State → Prop). Theory of nondeterministic automata extends LTS.
• In the same directory you'll find several definitions of equivalences and proofs about them. I've basically formalised most of the key concepts in Sangiorgi's 'Introduction to Bisimulation and Coinduction'.
• We have CCS (as given in Sangiorgi2011) formalised in https://cs-lean.github.io/Cslib/Languages/CCS/Basic.html, with a proof that bisimilarity is a congruence.

[Fabrizio Montesi]

On ongoing work: I have a student who's formalising the Curry-Howard isomorphism between the (right variant of the) internal pi-calculus and classical linear logic.

[Pieter Cuijpers]

Yes, looking into the CCS work and the LTS definitions as we speak.
My roots are more ACP style, and I was thinking of steps towards formalizing a book like Handbook of Process Algebra (probably too ambitious). The CCS & bisim as a congruence is probably a good place to start for some of my students. (Still have to see how many I can get interested, though).

I have some "starting questions" about LTS, but I'll start a new topic for that.