Reasoning about UNITY Programs
using Isabelle

EPSRC logo The UNITY formalism is an extremely simple framework for looking at concurrency. It cannot be called realistic, but it is a good basis for investigating fundamental questions.
  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.