This contains the Isabelle proofs for the paper "Trace models of concurrent valuation algebras"
In Traces.thy we set up the basic model of traces as sequences of values.
In StateTrace.thy we show that the State Model is a Concurrent Valuation Algebra, with the appropriate exchange law.
In a later development, the presheaf structure and other results were formalised, available here