A Sound Deep Embedding of Arbitrary Normal Modal Logics in Coq - Silveira, Ariel Agne Da; Ribeiro, Rodrigo; Nunes, Miguel Alfredo; Torrens, Paulo; Roggia, Karina (Anais do Simpósio Brasileiro de Linguagens de Programação (SBLP); 2022: Anais do XXVI Simpósio Brasileiro de Linguagens de Programação, 2022)
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.