Lics

IEEE Symposium on Logic in Computer Science

LICS Home - LICS Awards - LICS Newsletters - LICS Archive - LICS Organization - Logic-Related Conferences - Links

Sixteenth Annual IEEE Symposium on

Logic in Computer Science (LICS 2001)

Paper: Light Affine Lambda Calculus and Polytime Strong Normalization (at LICS 2001)

Winner of the Kleene Award in 2001
Authors: Kazushige Terui

Abstract

Light linear logic (LLL) and its variant, intuitionistic light affine logic (ILAL), are logics of polytime computation. All polynomial-time functions are representable by proofs of these logics (via the proofs-as-programs correspondence), and, conversely, that there is a specific reduction (cut-elimination) strategy which normalizes a given proof in polynomial time (the latter may well be called the polytime 'weak' normalization theorem). In this paper, we introduce an untyped term calculus, called the light affine lambda calculus (λLA), generalizing the essential ideas of light logics into an untyped framework. It is a simple modification of the λ-calculus, and has ILAL as a type assignment system. Then, in this generalized setting, we prove the polytime 'strong' normalization theorem: any reduction strategy normalizes a given λLA term (of fixed depth) in a polynomial number of reduction steps, and indeed in polynomial time

BibTeX

  @InProceedings{Terui-LightAffineLambdaCa,
    author = 	 {Kazushige Terui},
    title = 	 {Light Affine Lambda Calculus and Polytime Strong Normalization},
    booktitle =  {Proceedings of the Sixteenth Annual IEEE Symposium on Logic in Computer Science (LICS 2001)},
    year =	 {2001},
    month =	 {June}, 
    pages =      {209--220},
    location =   {Boston, MA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }
   

Last modified: 2017-04-0512:37
Andrzej Murawski