DROPS

Document

DOI: 10.4230/LIPIcs.CSL.2022.26

Parallelism in Soft Linear Logic

Authors: Paulin Jacobé de Naurois

Published in: LIPIcs, Volume 216, 30th EACSL Annual Conference on Computer Science Logic (CSL 2022)

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.

Cite as

Paulin Jacobé de Naurois. Parallelism in Soft Linear Logic. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 26:1-26:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@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/entities/document/10.4230/LIPIcs.CSL.2022.26},
  URN =		{urn:nbn:de:0030-drops-157468},
  doi =		{10.4230/LIPIcs.CSL.2022.26},
  annote =	{Keywords: Implicit Complexity, Typing, Linear Logic, Functional Programming}
}

Document

DOI: 10.4230/LIPIcs.FSCD.2019.29

Pointers in Recursion: Exploring the Tropics

Authors: Paulin Jacobé de Naurois

Published in: LIPIcs, Volume 131, 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)

Abstract

We translate the usual class of partial/primitive recursive functions to a pointer recursion framework, accessing actual input values via a pointer reading unit-cost function. These pointer recursive functions classes are proven equivalent to the usual partial/primitive recursive functions. Complexity-wise, this framework captures in a streamlined way most of the relevant sub-polynomial classes. Pointer recursion with the safe/normal tiering discipline of Bellantoni and Cook corresponds to polylogtime computation. We introduce a new, non-size increasing tiering discipline, called tropical tiering. Tropical tiering and pointer recursion, used with some of the most common recursion schemes, capture the classes logspace, logspace/polylogtime, ptime, and NC. Finally, in a fashion reminiscent of the safe recursive functions, tropical tiering is expressed directly in the syntax of the function algebras, yielding the tropical recursive function algebras.

Cite as

Paulin Jacobé de Naurois. Pointers in Recursion: Exploring the Tropics. In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 131, pp. 29:1-29:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{jacobedenaurois:LIPIcs.FSCD.2019.29,
  author =	{Jacob\'{e} de Naurois, Paulin},
  title =	{{Pointers in Recursion: Exploring the Tropics}},
  booktitle =	{4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)},
  pages =	{29:1--29:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-107-8},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{131},
  editor =	{Geuvers, Herman},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.29},
  URN =		{urn:nbn:de:0030-drops-105360},
  doi =		{10.4230/LIPIcs.FSCD.2019.29},
  annote =	{Keywords: Implicit Complexity, Recursion Theory}
}

Search Results

Documents authored by Jacobé de Naurois, Paulin

Parallelism in Soft Linear Logic

Abstract

Cite as

Pointers in Recursion: Exploring the Tropics

Abstract

Cite as

Thanks for your feedback!

Could not send message