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

*Winner of the Kleene Award in 2001***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} }