Pyrosome: Verified Compilation for Modular Metatheory. - Dustin Jamner; Gabriel Kammer; Ritam Nag; Adam Chlipala (CoRR, 2025)