Secure the Clones
The Coq development

Modules

• Axioms.v: We add the excluded middle and put as axiom a bijection between positive and positive*positive (it could be of course implemented with a few hacking).
• Lib.v: Tactics and notations.
• Semantics.v: Language semantics and copy policy semantics.
• Types.v: Type syntax and typing rules.
• Misc.v: Auxiliary lemmas.
• Overriding.v: Proofs of some overriding properties.
• InterpMonotony.v: Proofs of type interpretation monotony.
• PreserveWfType.v: Proofs of preservation of type well-formedness.
• PreserveInvSem.v: Proofs of preservation of semantic state invariant.
• InterpAnnot.v: Proofs about semantic interpretation of copy annotations.
• Modified.v: Proofs about method call side effects.
• Soundness.v: Last proofs about type soundness. We at last establish:
  

  Theorem soundness : forall p, well_formed p -> wt_program  p -> secure_program p.

Total size of the development: about 6000 loc.