License: 
Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CSL.2022.26
URN: urn:nbn:de:0030-drops-157468
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2022/15746/
Jacobé de Naurois, Paulin
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.
BibTeX - Entry
@InProceedings{jacobedenaurois:LIPIcs.CSL.2022.26,
author = {Jacob\'{e} de Naurois, Paulin},
title = {{Parallelism in Soft Linear Logic}},
booktitle = {30th EACSL Annual Conference on Computer Science Logic (CSL 2022)},
pages = {26:1--26:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-218-1},
ISSN = {1868-8969},
year = {2022},
volume = {216},
editor = {Manea, Florin and Simpson, Alex},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2022/15746},
URN = {urn:nbn:de:0030-drops-157468},
doi = {10.4230/LIPIcs.CSL.2022.26},
annote = {Keywords: Implicit Complexity, Typing, Linear Logic, Functional Programming}
}
|
Keywords: |
|
Implicit Complexity, Typing, Linear Logic, Functional Programming |
|
Collection: |
|
30th EACSL Annual Conference on Computer Science Logic (CSL 2022) |
|
Issue Date: |
|
2022 |
|
Date of publication: |
|
27.01.2022 |
