HAL TEI export of lirmm-03271408 CCSD CC0 1.0 - Universal

HAL API Platform

 On relation between totality semantic and syntactic validity Thomas Ehrhard ed475c91ccd26a8f518e16547b8d21be irif.fr thomas-ehrhard 742157 45101-742157 https://orcid.org/0000-0001-5231-5504 https://www.idref.fr/132983664 Farzad Jafarrahmani f4a92f60bb21cb32cc29fbbc84f7b17a gmail.com 1048340 2069133-1048340 https://orcid.org/0000-0003-1827-5881 https://www.idref.fr/276687477 Alexis Saurin 113b4c8fba756851c11688df77d61e40 irif.fr alexis-saurin 16833 11426-16833 https://www.idref.fr/233760210 Isabelle Gouat 01a8910ec35817770bca127295d8d38a lirmm.fr 2021-06-25 16:58:37 2025-12-19 10:22:02 2021-06-25 17:08:04 2021-06-27 2021-06-25 contributor Isabelle Gouat 01a8910ec35817770bca127295d8d38a lirmm.fr CCSD lirmm-03271408 https://hal-lirmm.ccsd.cnrs.fr/lirmm-03271408 ehrhard:lirmm-03271408 <i>5th International Workshop on Trends in Linear Logic and Applications (TLLA 2021)</i>, Jun 2021, Rome (virtual), Italy 5th International Workshop on Trends in Linear Logic and Applications (TLLA 2021), Jun 2021, Rome (virtual), Italy CC BY-NC 4.0 - Attribution - Non-commercial use CNRS - Centre national de la recherche scientifique Laboratoire d'Informatique de Robotique et de Microélectronique de Montpellier Université Paris Cité Université Paris Cité Université Paris Cité - Faculté des Sciences 5th International Workshop on Trends in Linear Logic and Applications (TLLA 2021) Institut de Recherche en Informatique Fondamentale International No No Yes Yes On relation between totality semantic and syntactic validity Thomas Ehrhard ed475c91ccd26a8f518e16547b8d21be irif.fr thomas-ehrhard 742157 45101-742157 https://orcid.org/0000-0001-5231-5504 https://www.idref.fr/132983664 Farzad Jafarrahmani f4a92f60bb21cb32cc29fbbc84f7b17a gmail.com 1048340 2069133-1048340 https://orcid.org/0000-0003-1827-5881 https://www.idref.fr/276687477 Alexis Saurin 113b4c8fba756851c11688df77d61e40 irif.fr alexis-saurin 16833 11426-16833 https://www.idref.fr/233760210 5th International Workshop on Trends in Linear Logic and Applications (TLLA 2021) 2021-06-27 2021-06-28 Rome (virtual) Italy 2021-06-25 https://lipn.univ-paris13.fr/TLLA/2021/ English Computer Science [cs]/Logic in Computer Science [cs.LO] Conference papers Conference papers Conference papers

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.

 193993007 201621976X https://ror.org/02krdtz55 Q51783269 Institut de Recherche en Informatique Fondamentale IRIF (UMR_8243) 2020-01-01
Université Paris CitéBâtiment Sophie Germain, Case courrier 70148 Place Aurélie Nemours75205 Paris Cedex 13
https://www.irif.fr/ 02636817X 0000000122597504 https://ror.org/02feahw73 Centre National de la Recherche Scientifique CNRS 1939-10-19
https://www.cnrs.fr/ 236453505 0000 0004 7885 7602 https://ror.org/05f82e368 Université Paris Cité UPCité 2020-01-01
85 boulevard Saint-Germain75006 Paris
https://u-paris.fr/