Skip to main navigation Skip to search Skip to main content

Simple parsimonious types and logarithmic space

  • University Paris 13

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

19 Citations (Scopus)

Abstract

We present a functional characterization of deterministic logspace-computable predicates based on a variant (although not a subsystem) of propositional linear logic, which we call parsimonious logic. The resulting calculus is simply-typed and contains no primitive besides those provided by the underlying logical system, which makes it one of the simplest higher-order languages capturing logspace currently known. Completeness of the calculus uses the descriptive complexity characterization of logspace (we encode first-order logic with deterministic closure), whereas soundness is established by executing terms on a token machine (using the geometry of interaction).

Original languageEnglish
Title of host publication24th EACSL Annual Conference on Computer Science Logic, CSL 2015
EditorsStephan Kreutzer
PublisherSchloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
Pages24-40
Number of pages17
ISBN (Electronic)9783939897903
DOIs
Publication statusPublished - 1 Sept 2015
Externally publishedYes
Event24th EACSL Annual Conference on Computer Science Logic, CSL 2015 - Berlin, Germany
Duration: 7 Sept 201510 Sept 2015

Publication series

NameLeibniz International Proceedings in Informatics, LIPIcs
Volume41
ISSN (Print)1868-8969

Conference

Conference24th EACSL Annual Conference on Computer Science Logic, CSL 2015
Country/TerritoryGermany
CityBerlin
Period7/09/1510/09/15

Keywords

  • Geometry of interaction
  • Implicit computational complexity
  • Linear logic

Fingerprint

Dive into the research topics of 'Simple parsimonious types and logarithmic space'. Together they form a unique fingerprint.

Cite this