Phase Semantics for Linear Logic with Least and Greatest Fixed Points - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2022

Phase Semantics for Linear Logic with Least and Greatest Fixed Points

Résumé

The truth semantics of linear logic (i.e. phase semantics) is often overlooked despite having a wide range of applications and deep connections with several denotational semantics. In phase semantics, one is concerned about the provability of formulas rather than the contents of their proofs (or refutations). Linear logic equipped with the least and greatest fixpoint operators (µMALL) has been an active field of research for the past one and a half decades. Various proof systems are known viz. finitary and non-wellfounded, based on explicit and implicit (co)induction respectively. In this paper, we extend the phase semantics of multiplicative additive linear logic (a.k.a. MALL) to µMALL with explicit (co)induction (i.e. µMALL ind). We introduce a Tait-style system for µMALL called µMALLω where proofs are wellfounded but potentially infinitely branching. We study its phase semantics and prove that it does not have the finite model property.
Fichier principal
Vignette du fichier
LIPIcs-FSTTCS-2022-35.pdf (914.17 Ko) Télécharger le fichier
Origine : Fichiers éditeurs autorisés sur une archive ouverte
Licence : CC BY - Paternité

Dates et versions

hal-04061582 , version 1 (06-04-2023)

Licence

Paternité

Identifiants

Citer

Abhishek De, Farzad Jafarrahmani, Alexis Saurin. Phase Semantics for Linear Logic with Least and Greatest Fixed Points. FSTTCS 2022 - 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, Dec 2022, Chennai, India. pp.35:1--35:23, ⟨10.4230/LIPIcs.FSTTCS.2022.35⟩. ⟨hal-04061582⟩
27 Consultations
25 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More