VeriTaS: Verification of Type System Specifications
Developing a type system with a soundness proof is hard. The VeriTaS project aims at simplifying the development of sound type systems through automation of soundness proofs and through automated derivation of efficient type checkers from sound type system specifications. Within the VeriTaS project, I focus on developing an interface for the verification of progress and preservation proofs which shall automate standard parts such proofs. To achieve this, I propose to identify recurring proof strategies in progress and preservation proofs from the literature, to develop a format for abstractly representing these proof strategies, and to mechanize them by integrating with existing theorem provers.