Reasoning about UNITY programs
using Isabelle

1. L. C. Paulson.
   Mechanizing UNITY in Isabelle. ACM Transactions on Computational Logic 1 1 (2000), 3–32.
2. Sidi O. Ehmety and L. C. Paulson.
   Representing component states in higher-order logic. In: Richard J. Boulton and Paul B. Jackson (editors),Theorem Proving in Higher Order Logics (2001)
   
3. L. C. Paulson.
   Mechanizing a theory of program composition for UNITY. ACM Transactions on Programming Languages and Systems 25 5 (2001), 626–656.
4. Sidi O. Ehmety and L. C. Paulson.
   Program composition in Isabelle/UNITY. In: Michel Charpentier and Beverly Sanders (editors),Formal Methods for Parallel Programming: Theory and Application (2002).
5. Sidi O. Ehmety and L. C. Paulson.
   Mechanizing Compositional Reasoning for Concurrent Systems: Some Lessons. Formal Aspects of Computing 17 (2005), 58–68.

Research funded by the EPSRC grants GR/K57381 and GR/M 75440.