Tentative Programme for 2 hours:

• From II order Intuitionistic, Multiplicative and Exponential Linear Logic to Intuitionistic Light Affine Logic.
• Intuitionistic Light Affine Logic as Proof-nets.
• The Cut-elimination of Intuitionistic Light Affine Logic.
• The Round-by-Round Strategy and its Main Properties.
• PolyStep Soundness of Intuitionistic Light Affine Logic.
• PolyTime Strong Soundness of Intuitionistic Light Affine Logic.
• The Expressive Power of Intuitionistic Light Affine Logic.
• Conclusions and Open Problems.

Download the lecture notes (a ps.gz of about 750Kb)

Back