2026-07-22T18:45:15Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:5405 2024-03-06T10:36:23Z ddc:004 open_access

Simple Parsimonious Types and Logarithmic Space Mazza, Damiano implicit computational complexity linear logic geometry of interaction 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). Schloss Dagstuhl – Leibniz-Zentrum für Informatik Damiano Mazza 2015 Is Part Of LIPIcs, Volume 41, 24th EACSL Annual Conference on Computer Science Logic (CSL 2015) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CSL.2015.24 urn:nbn:de:0030-drops-54053 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.24 eng https://creativecommons.org/licenses/by/3.0/legalcode