A protocol for distributed cooperative work
Joseph A. Goguen, Grigore Roşu · Electronic Notes in Theoretical Computer Science · 2000
After a brief review of hidden algebra, we give behavioral specifications for set theory and closure operators, and then use these to give a behavioral specification of an abstract protocol to support distributed cooperative work structured by dependencies in such a way as to form what we call a weak closure operator. We give some correctness proofs for this protocol, and then describe a concrete instance of it, called the tatami protocol, that supports distributed cooperative proving. Finally, we draw some methodological conclusions.