Skip to Main content Skip to Navigation
Conference papers

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.
Document type :
Conference papers
Complete list of metadata

https://hal-lirmm.ccsd.cnrs.fr/lirmm-03271408
Contributor : Isabelle Gouat <>
Submitted on : Friday, June 25, 2021 - 4:58:37 PM
Last modification on : Tuesday, July 13, 2021 - 3:15:09 AM

File

TLLA_2021_paper_15.pdf
Files produced by the author(s)

Licence


Distributed under a Creative Commons Attribution - NonCommercial 4.0 International License

Identifiers

  • HAL Id : lirmm-03271408, version 1

Collections

Citation

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⟩

Share

Metrics

Record views

54

Files downloads

26