Abstract: This paper describes some tools to support formal methods, and conversely some formal methods for developing such tools. We focus on distributed cooperative proving over the web. Our tools include a proof editor/assistant, servers for remote proof execution, a distributed truth protocol, an editor generator, and a new method for interface design called algebraic semiotics, which combines semiotics with algebraic specification. Some examples are given.
Joseph A. Goguen, Kai Lin, A. Mori, Grigore Rosu,