Formalizing the Semantics of Concurrent Revisions

An Isabelle/HOL formalization of the concurrent revisions model has an operational semantics, with an informal proof of determinacy, and a number of subtle ambiguities in the specification of the semantics are identified.