Coq proofs for "Views: Compositional Reasoning for Concurrent Programs"

Technical report "Views: Compositional Reasoning for Concurrent Programs", which extends our submission.
Coq proofs: framework soundness and examples.