  This paper is a structured introduction to Light Affine Logic, and to its
intuitionistic fragment. Light Affine Logic has a polynomially costing cut
elimination (P-Time correctness), and encodes all P-Time Turing machines
(P-Time completeness). P-Time correctness is proved by introducing the Proof
nets for Intuitionistic Light Affine Logic. P-Time completeness is demonstrated
in full details thanks to a very compact program notation. On one side, the
proof of P-Time correctness describes how the complexity of cut elimination is
controlled, thanks to a suitable cut elimination 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. On the other side, the proof of P-Time completeness, together with a
lot of programming examples, gives a flavor of the non trivial task of
programming with resource limitations, using Intuitionistic Light Affine Logic
derivations as programs.
