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.archives-ouvertes.fr/hal-03374648
Contributor : Paulin Jacobé de Naurois Connect in order to contact the contributor
Submitted on : Tuesday, October 12, 2021 - 11:35:03 AM
Last modification on : Wednesday, October 27, 2021 - 4:16:21 PM
Long-term archiving on: : Thursday, January 13, 2022 - 7:14:53 PM

File

PSLL-CSL - Final.pdf
Files produced by the author(s)

Identifiers

Citation

Paulin Jacobé de Naurois. Parallelism in Soft Linear Logic. Computer Science Logic, Feb 2022, Göttingen, Germany. ⟨10.4230/LIPIcs..10⟩. ⟨hal-03374648⟩

Share

Metrics

Les métriques sont temporairement indisponibles