Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
Publications of Lawrence C Paulson
[go: Go Back, main page]

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.EPSRC logo

Last revised: 3 January, 2008