# Reasoning about UNITY programs

using Isabelle

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.
- L. C. Paulson
**.**Mechanizing UNITY in Isabelle.*ACM Transactions on Computational Logic***1**1 (2000), 3–32. - 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)* - L. C. Paulson
**.**Mechanizing a theory of program composition for UNITY.*ACM Transactions on Programming Languages and Systems***25**5 (2001), 626–656. - Sidi O. Ehmety and L. C. Paulson.

Program composition in Isabelle/UNITY.*I*Michel Charpentier and Beverly Sanders (editors),*n*:*Formal Methods for Parallel Programming: Theory and Application*(2002). - 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.