Some of our HOL libraries can be downloaded from the links below. Keep in mind that HOL versions move very fast, which is a good thing, but it also means that our code may be obsolete by now. Maintenance proof code is indeed still a problem --hopefully one which will be solved in the near future.

1. A Theory of General UNITY (v 2002) .

   This theory attemps to provide a general setup for various UNITY variants. People can create a variant by instantiating the general theory. Common laws will be inherited for free.

2. COMUNITY (v 2002) .

   A theory for compositional reasoning for distributed systems in the tradition of UNITY's axiomatical style. It is simple and nice, the way UNITY is, but extends the classical UNITY with a general and powerful composition laws.

   [On-going]

3. A Theory of Refinement for UNITY (v 2000) by Tanja Vos.

4. Verfied Distributed Algorithms by Tanja Vos.

5. A HOL library to make inductive data types with negative occurences by Tanja Vos .

6. A Theory of Compositional UNITY (v 1999).

   A theory that extends UNITY with compositional reasoning for mutual exclusion based distributed systems. Like the classical UNITY, the style is axiomatical style. It is simple and nice.

   The latest build runs on Taupo 6.

7. Verified (Hierarchical) Self-stabilization Algorithms by W. Prasetya.

8. A Theory of UNITY (v 1995).

   My Ph.D. original work on formalizing UNITY. Features: self-stabilization, convergence, compositional reasoning.

   Runs on a very old version of HOL (1988).