On relation between totality semantic and syntactic validity - LIRMM - Laboratoire d’Informatique, de Robotique et de Microélectronique de Montpellier
Conference Papers Year : 2021

On relation between totality semantic and syntactic validity

Abstract

In this paper, we present a denotational semantic for non-wellfounded proofs of µLL ∞ , linear logic extended with least and greatest fixed points, by adapting the categorical semantics of µLL ∞ [EJ21]. Two instances of this categorical setting are REL (category of sets and relations), and NUTS (category of sets equipped with a notion of totality and relations preserving it) which is studied in [EJ21]. In particular, we relate validity condition for non-wellfounded proofs and totality of NUTS. More precisely, we show each µLL ∞ valid proof will have interpreted as a total element in NUTS.
Fichier principal
Vignette du fichier
TLLA_2021_paper_15.pdf (174.79 Ko) Télécharger le fichier
Origin Files produced by the author(s)

Dates and versions

lirmm-03271408 , version 1 (25-06-2021)

Licence

Identifiers

  • HAL Id : lirmm-03271408 , version 1

Cite

Thomas Ehrhard, Farzad Jafarrahmani, Alexis Saurin. On relation between totality semantic and syntactic validity. 5th International Workshop on Trends in Linear Logic and Applications (TLLA 2021), Jun 2021, Rome (virtual), Italy. ⟨lirmm-03271408⟩
207 View
148 Download

Share

More