Skip to Main content Skip to Navigation
Conference papers

Parallelism in Soft Linear Logic

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

https://hal-lirmm.ccsd.cnrs.fr/lirmm-03271468
Contributor : Isabelle Gouat <>
Submitted on : Friday, June 25, 2021 - 5:50:34 PM
Last modification on : Sunday, June 27, 2021 - 3:21:21 AM

File

TLLA_2021_paper_9.pdf
Files produced by the author(s)

Licence


Distributed under a Creative Commons Attribution - NonCommercial 4.0 International License

Identifiers

  • HAL Id : lirmm-03271468, version 1

Citation

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⟩

Share

Metrics

Record views

36

Files downloads

24