A Sound Deep Embedding of Arbitrary Normal Modal Logics in Coq

  • Ariel Agne Da Silveira UFOP
  • Rodrigo Ribeiro UFOP
  • Miguel Alfredo Nunes UDESC
  • Paulo Torrens UDESC
  • Karina Roggia UDESC

Resumo


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.

Palavras-chave: soundness, Modal logic, Coq proof assistant
Publicado
03/10/2022
Como Citar

Selecione um Formato
SILVEIRA, Ariel Agne Da; RIBEIRO, Rodrigo; NUNES, Miguel Alfredo; TORRENS, Paulo; ROGGIA, Karina. A Sound Deep Embedding of Arbitrary Normal Modal Logics in Coq. In: SIMPÓSIO BRASILEIRO DE LINGUAGENS DE PROGRAMAÇÃO (SBLP), 26. , 2022, Uberlândia. Anais [...]. Porto Alegre: Sociedade Brasileira de Computação, 2022 . p. 1–7.