Intuitionistic light affine logic

This paper is a structured introduction to Intuitionistic Light Affine Logic (ILAL). ILAL has a polynomially costing normalization, and it is expressive enough to encode, and simulate, all PolyTime Turing machines. The bound on the normalization cost is proved by introducing the proof-nets for ILAL. The bound follows from a suitable normalization strategy that exploits structural properties of the proof-nets. This allows to have a good catch on the meaning of the paragraph modality, which is a peculiarity of light logics. The expressive power of ILAL is demonstrated in full details. Such a proof gives a flavor of the non trivial task of programming with resource limitations, using ILAL derivations as programs.