loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
22nd Annual IEEE Symposium on Logic in Computer Science (LICS 2007)
Stratified Bounded Affine Logic for Logarithmic Space
Wroclaw, Poland
July 10-July 14
ISBN: 0-7695-2908-9
Ulrich Sch?pp, Ludwig-Maximilians-Universitat Munchen, Germany
A number of complexity classes, most notably PTIME, have been characterised by sub-systems of linear logic. In this paper we show that the functions computable in log-arithmic space can also be characterised by a restricted version of linear logic. We introduce Stratified Bounded Affine Logic (SBAL), a restricted version of Bounded Linear Logic, in which not only the modality ! but also the universal quantifier is bounded by a resource polynomial. We show that the proofs of certain sequents in SBAL represent exactly the functions computable logarithmic space. The proof that SBAL-proofs can be compiled to LOGSPACE functions rests on modelling computation by interaction dialogues in the style of game semantics. We formulate the compilation of SBAL-proofs to space-efficient programs as an interpretation in a realisability model, in which realisers are taken from a Geometry of Interaction situation.
Citation:
Ulrich Sch?pp, "Stratified Bounded Affine Logic for Logarithmic Space," lics, pp.411-420, 22nd Annual IEEE Symposium on Logic in Computer Science (LICS 2007), 2007
Usage of this product signifies your acceptance of the Terms of Use.