Language-parameterized Proofs for Functional Languages with Subtyping

Language designers often strive to prove that their programming languages satisfy the properties that were intended at the time of design. \(\textsc {Lang}\text {-}\textsc {n}\text {-}\textsc {Prove}\) is a DSL for expressing language-parametrized proofs, that is, proofs that apply to classes of languages rather than a single language. Prior work has used \(\textsc {Lang}\text {-}\textsc {n}\text {-}\textsc {Prove}\) to express the language-parametrized proofs of type soundness (excluding the substitution lemmas) for a certain class of functional languages. In this paper, we address this class of languages when subtyping is added to them. We provide the language-parametrized proofs of their type soundness (excluding the substitution lemmas) and of the equivalence between algorithmic and declarative subtyping. To express these proofs naturally, we have extended \(\textsc {Lang}\text {-}\textsc {n}\text {-}\textsc {Prove}\) with new operations. Our extension of \(\textsc {Lang}\text {-}\textsc {n}\text {-}\textsc {Prove}\) generates Abella proofs that machine-check the type soundness of a nontrivial class of functional languages with declarative and algorithmic subtyping, when just a few simple lemmas are admitted.