Computer Science – Logic in Computer Science
Scientific paper
2000-06-05
Computer Science
Logic in Computer Science
Scientific paper
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.
Asperti Andrea
Roversi Luca
No associations
LandOfFree
Light Affine Logic (Proof Nets, Programming Notation, P-Time Correctness and Completeness) does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with Light Affine Logic (Proof Nets, Programming Notation, P-Time Correctness and Completeness), we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Light Affine Logic (Proof Nets, Programming Notation, P-Time Correctness and Completeness) will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-578822