Phase Semantics for Linear Logic with Least and Greatest Fixed Points

Autor:	De, Abhishek, Jafarrahmani, Farzad, Saurin, Alexis
Přispěvatelé:	Institut de Recherche en Informatique Fondamentale (IRIF (UMR_8243)), Centre National de la Recherche Scientifique (CNRS)-Université Paris Cité (UPCité), Design, study and implementation of languages for proofs and programs (PI.R2), Centre National de la Recherche Scientifique (CNRS)-Inria de Paris, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université Paris Cité (UPCité)-Institut de Recherche en Informatique Fondamentale (IRIF (UMR_8243)), Centre National de la Recherche Scientifique (CNRS)-Université Paris Cité (UPCité)-Centre National de la Recherche Scientifique (CNRS)-Université Paris Cité (UPCité), Les assistants à la démonstration au cœur du raisonnement mathématique (PICUBE), Inria de Paris, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Institut de Recherche en Informatique Fondamentale (IRIF (UMR_8243)), ANR-21-CE48-0019,RECIPROG,Raisonner avec des preuves circulaires pour la programmation(2021), European Project
Jazyk:	angličtina
Rok vydání:	2022
Předmět:	Fixed points Theory of computation → Linear logic Phase semantics Cosure ordinals Theory of computation → Proof theory Linear logic Cut elimination [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] closure ordinals Theory of computation → Proof theory phrases Linear logic
Zdroj:	FSTTCS 2022-42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science 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⟩
Popis:	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. LIPIcs, Vol. 250, 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2022), pages 35:1-35:23
Databáze:	OpenAIRE
Externí odkaz:	https://explore.openaire.eu/search/publication?articleId=doi_dedup___::16de1d38ebbb5a6dae1e386be7718d27 https://hal.science/hal-04061582/document Zobrazit plný text záznamu