A Sound Deep Embedding of Arbitrary Normal Modal Logics in Coq. - Ariel Agne Da Silveira; Rodrigo Ribeiro; Miguel Alfredo Nunes; Paulo Torrens; Karina Girardi Roggia (SBLP, 2022)