Nanopass Back-Translation of Call-Return Trees for Mechanized Secure Compilation Proofs. - Jérémy Thibault; Joseph Lenormand; Catalin Hritcu (CoRR, 2025)