These papers typically contain (semi-)formal descriptions of the type system and various proofs about it. The technical material for this paper is in an appendi

These papers typically contain (semi-)formal descriptions of the type system and various proofs about it. The technical material for this paper is in an appendix: https://www.cs.cornell.edu/andru/papers/gallifrey-types/appendix.pdf https://www.cs.cornell.edu/andru/papers/gallifrey-types/appe... For real-world languages, this is even more involved, and existing formalizations only cover supposedly distinct sub-languages, not the full language (with the risk being that there are unexpected interactions). Most languages also have complicated things like higher-order functions or some form of polymorphism, and the new type system would have to be integrated with that.