Reusable Programming Language Components

Type systems play a central role in preventing software errors by classifying program terms and enabling compile-time detection of incorrect behavior. A key guarantee of such systems is type soundness, which ensures that well-typed programs do not exhibit certain classes of runtime errors. While formalizing a programming language’s semantics and proving type soundness provides strong assurance of correctness, this process is often prohibitively time-consuming and complex. This thesis addresses this challenge by investigating how the specification and verification effort can be reduced through the reuse of existing components and proofs, with the goal of enabling more efficient development of reliable programming languages.