License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CSL.2018.9
URN: urn:nbn:de:0030-drops-96763
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2018/9676/
Go to the corresponding LIPIcs Volume Portal

Baillot, Patrick ; Ghyselen, Alexis

Combining Linear Logic and Size Types for Implicit Complexity

pdf-format:
LIPIcs-CSL-2018-9.pdf (0.6 MB)

Abstract

Several type systems have been proposed to statically control the time complexity of lambda-calculus programs and characterize complexity classes such as FPTIME or FEXPTIME. A first line of research stems from linear logic and restricted versions of its !-modality controlling duplication. A second approach relies on the idea of tracking the size increase between input and output, and together with a restricted recursion scheme, to deduce time complexity bounds. However both approaches suffer from limitations : either a limited intensional expressivity, or linearity restrictions. In the present work we incorporate both approaches into a common type system, in order to overcome their respective constraints. Our system is based on elementary linear logic combined with linear size types, called sEAL, and leads to characterizations of the complexity classes FPTIME and 2k-FEXPTIME, for k >= 0.

BibTeX - Entry

@InProceedings{baillot_et_al:LIPIcs:2018:9676,
  author =	{Patrick Baillot and Alexis Ghyselen},
  title =	{{Combining Linear Logic and Size Types for Implicit Complexity}},
  booktitle =	{27th EACSL Annual Conference on Computer Science Logic  (CSL 2018)},
  pages =	{9:1--9:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-088-0},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{119},
  editor =	{Dan Ghica and Achim Jung},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2018/9676},
  URN =		{urn:nbn:de:0030-drops-96763},
  doi =		{10.4230/LIPIcs.CSL.2018.9},
  annote =	{Keywords: Implicit computational complexity, lambda-calculus, linear logic, type systems, polynomial time complexity, size types}
}

Keywords: Implicit computational complexity, lambda-calculus, linear logic, type systems, polynomial time complexity, size types
Collection: 27th EACSL Annual Conference on Computer Science Logic (CSL 2018)
Issue Date: 2018
Date of publication: 29.08.2018

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI