On relation between totality semantic and syntactic validity - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2021

On relation between totality semantic and syntactic validity

Résumé

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
Origine : Fichiers produits par l'(les) auteur(s)

Dates et versions

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

Licence

Paternité - Pas d'utilisation commerciale

Identifiants

  • HAL Id : lirmm-03271408 , version 1

Citer

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⟩
185 Consultations
128 Téléchargements

Partager

Gmail Facebook X LinkedIn More