Natalia Moanga | Searcharxiv

arXiv2025

Operational semantics and program verification using many-sorted hybrid modal logic

We propose a general framework to allow: (a) specifying the operational semantics of a programming language; and (b) stating and proving properties about program correctness. Our framework is based on a many-sorted system of hybrid modal logic, for which we prove completeness results. We believe that our approach to program verification improves over the existing approaches within modal logic as (1) it is based on operational semantics which allows for a more natural description of the execution than Hoare's style weakest precondition used by dynamic logic; (2) being multi-sorted, it allows for a clearer encoding of semantics, with a smaller representational distance to its intended meaning.

cs.LO↗

arXiv2018

A many-sorted polyadic modal logic

This paper presents a many-sorted polyadic modal logic that generalizes some of the existing approaches. The algebraic semantics has led us to a many-sorted generalization of boolean algebras with operators, for which we prove the analogue of the Jónsson-Tarski theorem. While the transition from the mono-sorted logic to many-sorted one is a smooth process, we see our system as a step towards deepening the connection between modal logic and program verification, since our system can be seen as the propositional fragment of Matching logic, a first-order logic for specifying and reasoning about programs.

cs.LO↗