Creative Commons Attribution 4.0 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: https://drops.dagstuhl.de/opus/volltexte/2022/15746/
Jacobé de Naurois, Paulin
Parallelism in Soft Linear Logic
| pdf-format: |
|
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 | |
| Seminar: | 30th EACSL Annual Conference on Computer Science Logic (CSL 2022) | |
| Issue date: | 2022 | |
| Date of publication: | 27.01.2022 |
