Light Affine Logic (Proof Nets, Programming Notation, P-Time Correctness and Completeness)
<|reference_start|>Light Affine Logic (Proof Nets, Programming Notation, P-Time Correctness and Completeness): 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.<|reference_end|>
@article{asperti2000light,
    title={Light Affine Logic (Proof Nets, Programming Notation, P-Time Correctness
  and Completeness)},
    author={Andrea Asperti and Luca Roversi},
    journal={arXiv preprint arXiv:cs/0006010},
    year={2000},
    number={RT-54-2000},
    archivePrefix={arXiv},
    eprint={cs/0006010},
    primaryClass={cs.LO}
}