Matthieu Perrinel (ENS Lyon), Strong bound for light linear logic by levels
Schedule
- Jan. 31, 2012, 17:00 - 17:30
Abstract
The light linear logic by levels, introduced by Baillot and Mazza, is an extension of Girard's light linear logic. The aim of these logics is to characterize some complexity classes like FPtime and elementary time in the proofs-as-programs approach. Weak bounds (i.e. bounds for specific reduction strategies) were proven for two versions of light linear logic by levels (ml4 and ml4_0). However, the corresponding strategies are complex. Thus, it was difficult to transform those logics into true programming languages with explicit reduction strategy.
Extending Dal Lago's context semantics to light linear logic by levels, we show that ml4 and ml4_0 both enjoy a strong polynomial bound (valid for any reduction strategy).
Attachments
The light linear logic by levels, introduced by Baillot and Mazza, is an extension of Girard's light linear logic. The aim of these logics is to characterize some complexity classes like FPtime and elementary time in the proofs-as-programs approach. Weak bounds (i.e. bounds for specific reduction strategies) were proven for two versions of light linear logic by levels (ml4 and ml4_0). However, the corresponding strategies are complex. Thus, it was difficult to transform those logics into true programming languages with explicit reduction strategy. Extending Dal Lago's context semantics to light linear logic by levels, we show that ml4 and ml4_0 both enjoy a strong polynomial bound (valid for any reduction strategy).