2 Search Results for "Jacobé de Naurois, Paulin"

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-dev.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-dev.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}
}
  • Refine by Author
  • 2 Jacobé de Naurois, Paulin

  • Refine by Classification
  • 2 Theory of computation → Complexity theory and logic
  • 1 Software and its engineering → Recursion
  • 1 Theory of computation → Complexity classes
  • 1 Theory of computation → Linear logic

  • Refine by Keyword
  • 2 Implicit Complexity
  • 1 Functional Programming
  • 1 Linear Logic
  • 1 Recursion Theory
  • 1 Typing

  • Refine by Type
  • 2 document

  • Refine by Publication Year
  • 1 2019
  • 1 2022

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact