Logic programming and logarithmic space

CléMent Aubert, Marc Bagnol, Paolo Pistone, Thomas Seiller

Research output: Chapter in Book/Report/Conference proceedingConference contribution

4 Scopus citations


We present an algebraic view on logic programming, related to proof theory and more specifically linear logic and geometry of interaction. Within this construction, a characterization of logspace (deterministic and non-deterministic) computation is given via a syntactic restriction, using an encoding of words that derives from proof theory.

We show that the acceptance of a word by an observation (the counterpart of a program in the encoding) can be decided within logarithmic space, by reducing this problem to the acyclicity of a graph. We show moreover that observations are as expressive as two-ways multihead finite automata, a kind of pointer machine that is a standard model of logarithmic space computation.

Original languageEnglish (US)
Title of host publicationProgramming Languages and Systems - 12th Asian Symposium, APLAS 2014, Proceedings
EditorsJacques Garrigue
PublisherSpringer Verlag
Number of pages19
ISBN (Electronic)9783319127354
StatePublished - 2014
Externally publishedYes
Event12th Asian Symposium on Programming Languages and Systems, APLAS 2014 - Singapore, Singapore
Duration: Nov 17 2014Nov 19 2014

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Other12th Asian Symposium on Programming Languages and Systems, APLAS 2014


  • Automata
  • Geometry of interaction
  • Implicit complexity
  • Logarithmic space
  • Logic programming
  • Pointer machines
  • Proof theory
  • Unification

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)


Dive into the research topics of 'Logic programming and logarithmic space'. Together they form a unique fingerprint.

Cite this