au-ts / cogent

Cogent Project
https://trustworthy.systems/projects/TS/cogent.pml
Other
158 stars 26 forks source link

Subtyping proofs #415

Open crizkallah opened 2 years ago

crizkallah commented 2 years ago

Is it easy to merge this branch with master?

Subtyping.thy has some proofs about evaluation being deterministic that would be good to have.