Google Git
Sign in
opensecura / 3p / nicta / cogent / refs/heads/master / . / cogent / isa
tree: e1f8d959ab2dd50bf8f421d914b5df153e5ce274 [path history] [tgz]
  1. shallow/
  2. AssocLookup.thy
  3. Cogent.thy
  4. CogentHelper.thy
  5. Correspondence.thy
  6. Data.thy
  7. ML_Old.thy
  8. Mono.thy
  9. Mono_Tac.thy
  10. ProofTrace.thy
  11. README.md
  12. ROOT
  13. StringMap.thy
  14. Subtyping.thy
  15. TypeProofGen.thy
  16. TypeTrackingSemantics.thy
  17. TypeTrackingTyping.thy
  18. UpdateSemantics.thy
  19. Util.thy
  20. ValueSemantics.thy
cogent/isa/README.md

Typesystem Proofs

These proofs are about the Cogent type-system, and it's semantics.