Mechanized Type Soundness Proofs using Definitional Interpreters This repository contains the Coq Mechanizations presented in my master's thesis.