In this page I’ll list all papers and other academic works I’ve published. Eventually I’ll write posts about those works, which will be linked here.
Full Papers Published in Conference Proceedings
[PDF] Miguel Alfredo Nunes, Karina Girardi Roggia & Paulo Torrens, (2025). Soundness-Preserving Fusion of Modal Logics in Coq. In: C. Nogueira, S., Teodorov, C. (eds) Formal Methods: Foundations and Applications. SBMF 2024. Lecture Notes in Computer Science, vol 15403. Springer, Cham. 120 - 138.
Abstract
This work presents the formal verification of the concept of fusion of modal logics in the Coq proof assistent, along with a proof of the preservation of soundness. Our formalization is based on previous work by da Silveira et al. that formalizes several normal modal systems using Coq and proves their soundness and weak completeness. We give a high level description of the base library, how we modified it to fit our needs, how we defined fusion and how we proved the transfer of soundness. Our definition allows for the fusion of any normal modal logics, with any amount of modalities, requiring no changes to the definitions in the library.
[PDF] Ariel Agne Da Silveira, Rodrigo Ribeiro, Miguel Alfredo Nunes, Paulo Torrens, and Karina Girardi Roggia, (2022). A Sound Deep Embedding of Arbitrary Normal Modal Logics in Coq. In: Proceedings of the XXVI Brazilian Symposium on Programming Languages (SBLP ‘22). Association for Computing Machinery, 1–7.
Abstract
This work describes an encoding of modal logics using the Coq proof assistant. Our formalization differs from previous attempts by providing a uniform representation of several systems for modal logic using Coq’s rich type structure. We illustrate the usefulness of our library in a formalization of Löb’s theorem which closely follows a classical proof of this result.