Showing 1–4 of 4 results for author: Moangă, N

Many-Sorted Hybrid Modal Languages

Authors: Ioana Leuştean, Natalia Moangă, Traian Florin Şerbănuţă

Abstract: We continue our investigation into hybrid polyadic multi-sorted logic with a focus on expresivity related to the operational and axiomatic semantics of rogramming languages, and relations with first-order logic. We identify a fragment of the full logic, for which we prove sound and complete deduction and we show that it is powerful enough to represent both the programs and their semantics in an un… ▽ More We continue our investigation into hybrid polyadic multi-sorted logic with a focus on expresivity related to the operational and axiomatic semantics of rogramming languages, and relations with first-order logic. We identify a fragment of the full logic, for which we prove sound and complete deduction and we show that it is powerful enough to represent both the programs and their semantics in an uniform way. Although weaker than other hybrid systems previously developed, this system is expected to have better computational properties. Finally, we provide a standard translation from full hybrid many-sorted logic to first-order logic. △ Less

Submitted 2 July, 2020; originally announced July 2020.

Comments: arXiv admin note: text overlap with arXiv:1905.05036, arXiv:1907.05029

From Hybrid Modal Logic to Matching Logic and Back

Authors: Ioana Leuştean, Natalia Moangă, Traian Florin Şerbănuţă

Abstract: Building on our previous work on hybrid polyadic modal logic we identify modal logic equivalents for Matching Logic, a logic for program specification and verification. This provides a rigorous way to transfer results between the two approaches, which should benefit both systems. Building on our previous work on hybrid polyadic modal logic we identify modal logic equivalents for Matching Logic, a logic for program specification and verification. This provides a rigorous way to transfer results between the two approaches, which should benefit both systems. △ Less

Submitted 4 September, 2019; v1 submitted 11 July, 2019; originally announced July 2019.

Comments: In Proceedings FROM 2019, arXiv:1909.00584

Journal ref: EPTCS 303, 2019, pp. 16-31

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

Authors: Ioana Leustean, Natalia Moanga, Traian Florin Serbanuta

Abstract: 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 (… ▽ More 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. △ Less

Submitted 13 May, 2019; originally announced May 2019.

A many-sorted polyadic modal logic

Authors: Ioana Leustean, Natalia Moanga, Traian Florin Serbanuta

Abstract: 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 deepe… ▽ More 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. △ Less

Submitted 30 November, 2018; v1 submitted 26 March, 2018; originally announced March 2018.