This is an old revision of the document!
Speculative Linearizability
Automata Specification in Isabelle/HOL
Archive containing the theory files
An older version of the theory can be found in the Archive of Formal Proofs.
Trace-Based Specification in Isabelle/HOL
Specification Definition and proofs about the longest common prefix of a set of lists Recursive functions on lists IOA framework with finite trace semantics