dissertation-artifacts The Coq proofs of my dissertation "Iso-Recursive Subtyping: New Theory and Extensions"