Author name cluster

Sonia Marin

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

3 papers

2 author rows

CSL Conference 2024 Conference Paper

Intuitionistic Gödel-Löb Logic, à la Simpson: Labelled Systems and Birelational Semantics

Anupam Das 0002
Iris van der Giessen
Sonia Marin

We derive an intuitionistic version of Gödel-Löb modal logic (GL) in the style of Simpson, via proof theoretic techniques. We recover a labelled system, ℓIGL, by restricting a non-wellfounded labelled system for GL to have only one formula on the right. The latter is obtained using techniques from cyclic proof theory, sidestepping the barrier that GL’s usual frame condition (converse well-foundedness) is not first-order definable. While existing intuitionistic versions of GL are typically defined over only the box (and not the diamond), our presentation includes both modalities. Our main result is that ℓIGL coincides with a corresponding semantic condition in birelational semantics: the composition of the modal relation and the intuitionistic relation is conversely well-founded. We call the resulting logic IGL. While the soundness direction is proved using standard ideas, the completeness direction is more complex and necessitates a detour through several intermediate characterisations of IGL.

Details

LOPSTR Conference 2023 Conference Paper

A Logical Interpretation of Asynchronous Multiparty Compatibility

Marco Carbone
Sonia Marin
Carsten Schürmann 0001

Abstract Session types specify the protocols that communicating processes must follow in a concurrent system. When composing two or more processes, a session typing system must check whether such processes are compatible, i. e. , that all sent messages are eventually received and no deadlock ever occurs. After the propositions-as-types paradigm, relating session types to linear logic, previous work has shown that duality, in the binary case, and more generally coherence, in the multiparty case, are sufficient syntactic conditions to guarantee compatibility for two or more processes, yet do not characterise all compatible set of processes. In this work, we generalise duality/coherence to a notion of forwarder compatibility. Forwarders are specified as a restricted family of proofs in linear logic, therefore defining a specific set of processes that can act as middleware by transfering messages without using them. As such, they can guide a network of processes to execute asynchronously. Our main result establishes forwarder compatibility as a sufficient and necessary condition to fully capture all well-typed multiparty compatible processes.

Details

FLAP Journal 2021 Journal Article

Justification Logic for Constructive Modal Logic.

Roman Kuznets
Sonia Marin
Lutz Straßburger

We provide a treatment of the intuitionistic 3 modality in the style of justification logic. We introduce a new type of terms, called satisfiers, that justify consistency, obtain justification analogs for the constructive modal logics CK, CD, CT, and CS4, and prove the realization theorem for them.

Details