Linear logic and logical paradigms of computation - MPRI

Linear logic and optimal reductions

Stefano Guerrini

2009/2010

• A sample exam (pdf)
  NB There is a missprint in the text. In item 2 of the first exercise, x must be replaced wist y. Therefore, M1=Iy(IIy) and M2=IIy(Iy)
• Solutions of the sample exam (pdf)

1. 27/11/2009:
   13h00-16h15 - Chevaleret 0D01 Optimal or family reduction
   
   • Slides: 04/12/09 version (download)
2. 04/12/2009:
   room: Chevaleret 0D01
   Sharing graphs
   
   • Slides: 21/12/09 version (download)
3. 11/12/2009:
   room: Chevaleret 0D01
   Sharing graphs 2
   
   • Slides: 21/12/09 version (download)
4. 11/12/2009:
   room: Chevaleret 8B01
   Correctness of the sharing implemantion of β-rule
   
   • Slides: 21/12/09 version (download)

Main readings

1. A. Asperti and S. Guerrini. The Optimal Implementation of Functional Programming Languages In Cambridge Tracts in Theoretical Computer Science. Vol. 45. Cambridge University Press, 1998. Ch. 5 (download)
2. S. Guerrini. Sharing Implementations of Graph Rewriting Systems. TERMGRAPH 2004. ENTCS 127(5). Elsevier, 2005.(download)

Other references

1. A. Asperti and S. Guerrini. – The Optimal Implementation of Functional Programming Languages. Cambridge University Press, 1998.
2. J.-J. Lévy. Optimal Reductions in the lambda-calculus. In : To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, J.P. Seldin and J.R. Hindley (eds.), pp. 159-191. Academic Press, 1980.
3. S. Guerrini. – Proof nets and the lambda-calculus. In : Linear Logic in Computer Science, T. Ehrhard, P. Ruet, J.-Y. Girard and P. Scott (eds.). Cambridge University Press, 2004.
4. A. Asperti and H.G. Mairson – Parallel beta is not elementary recursive. In : Proc. 25-th Annual ACM Symposium on Principles of Programming Languages (POPL '98), Albuquerque, New Mexico. ACM Press, 1998.