Parallelism in Soft Linear Logic - LIRMM - Laboratoire d’Informatique, de Robotique et de Microélectronique de Montpellier
Communication Dans Un Congrès Année : 2021

Parallelism in Soft Linear Logic

Résumé

We extend the Soft Linear Logic of Lafont with a new kind of modality, called parallel. Contractions on parallel modalities are only allowed in the cut and the left rules, in a controlled, uniformly distributive way. We show that SLL, extended with this parallel modality, is sound and complete for PSPACE. We propose a corresponding typing discipline for the λ-calculus, extending the STA typing system of Gaboardi and Ronchi, and establish its PSPACE soundness and completeness. The use of the parallel modality in the cut-rule drives a polynomial-time, parallel call-by-value evaluation strategy of the terms.
Fichier principal
Vignette du fichier
TLLA_2021_paper_9.pdf (258.88 Ko) Télécharger le fichier
Origine Fichiers produits par l'(les) auteur(s)

Dates et versions

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

Licence

Identifiants

  • HAL Id : lirmm-03271468 , version 1

Citer

Paulin Jacobé de Naurois. Parallelism in Soft Linear Logic. 5th International Workshop on Trends in Linear Logic and Applications (TLLA 2021), Jun 2021, Rome (virtual), Italy. ⟨lirmm-03271468⟩
65 Consultations
84 Téléchargements

Partager

More