Proofs and Programs : Linear Logic and Quantitative Semantics (LMFI 2024/2025). Part 1.

• 08/01: Introduction and first steps in Abstract Rewriting: Slides
  Please email me if you wish to receive the lecture notes on Abstract Rewriting
  
  Bonus point (before the class on 10/01): EX at slide 33
  


• 10/01: Abstract Rewriting : Confluence, Commutation, Modular techniques Slides
  
  • TD0
    
  • Homework 1 + some notes Deadline: due by January 15, before the class
  • Bonus point (due by January 17, before class): another proof of Newman Lemma (slide 50)




• 15/01: Factorization, strategies. Terms and programs: the Call-by-Value Lambda Calculus Slides
  Memo CbN CbV lambda calculus
  


• 17/01: From factorization to normalization. Values and weak evaluation (CbV and CbN) Slides
  - TD Operational Semantics/Weak reduction
  - TD1. Make your own normalization strategy.
  - Homework 2 (due by 22/01, before class)
  1. Answer the questions in Fact 6 (?) at slide 90 (you can safely skip point 2, which has lot of typos)
  2. From the TD1 : prove Lemma 7, point 2 (preservation of weak normal forms).
  
  
  Bonus point: From the TD1 , pick only one of the following :
  • Prove head normalization assuming head factorization (page 2, EX A), OR
  • prove Fact X, Ex B, point 2 (at the end pag 2)




• Homework 2, 2nd chance (deadline: Feb 03): From the TD1 :
  • prove Fact X, Ex B, point 2 (at the end pag 2)
  • EX C, point 1 (page 3) Does my definition define leftmost-outermost reduction? Answere yes or NO, and if not, please correct it




• 22/01: First steps in Linear Logic Material and Lecture Notes are listed at the end of the page.
  • Slides Intro to Linear Logic
  • bonus point (IMPORTANT) (by Jan 24, 14h00) slide 13: Slide 12 shows the logical steps in cut-elimination for LL. Non-logical steps are how you imagine... Just show one example of commutation step (I recommend the first one)
  • Bonus point (by Jan 24, 14h00): slide 7 states two distributivity laws. Please prove any direction, using the calculus in slide 9. That is: pick any of the sequents in slide 7, write it one-sides, and derive it with the calculus in slide 9



• 24/01: Proof Nets, the graph syntax of Linear Logic
• Slided MLL Proof Nets
• HOMEWORK 3 (due before next class on Jan 29)
  1. MAIN: slides 27-30. Build the proof-net as indicated in the slides 27-30. Follow the instructions at slide 30: please give me your answer to the question, but also the proof-net that you build, and its normalization!
  2. QUICKLY DONE: from the Slides Intro to Linear Logic : points 3 at slide 18 . Please use one-sided sequents, and atomic axioms



• 29/01: Multiplicative Proof Nets: correctness and normalization
  • TD MLL proof-nets


• 31/01: MELL Proof Nets
  
  • Proof-Nets reduction rules
  • TD MELL


• 05/02: MELL proof-nets: confluence and normalization. Translating CbN and CbV Lambda calculus.
  • Slides Proof Nets (including MELL and normalization)
  • TD MELL


• 07/02: Sequentialization, intro to GoI, some classical results. Openings: bayesian learning & proof nets.
  
  HOMEWORK 4. Due: ** February 19 **
  1. Pick 2 questions in the "Multiplicative Booleans" Section of this project by O. Laurent Computing with Proof-Nets
     (Note: pick a question which is new for us! questions 1, 2 and 3 bring no point!).
  2. From the TD1 , prove Theorem 10 (page 3) in the CbV case. Please use only weak reduction (ie, s=w)



---

Material and Lecture Notes

• Lecture notes on Abstract Rewriting . Please email me to receive the notes.
• Linear Logic: Notes (by O. Laurent).
  Notes on Proof Nets (English) (by O. Laurent)
  Draft book on Linear Logic (English)
  More material on LL is listed here .
  

---

About Homework:

Please:
1. Send by email-- please start the subject with LMFI (my spam filter is very aggressive)
2. Include your NAME in the file_name:
   Example: DM1_PaoloRossi.pdf, HW2_MarieEtudiante.pdf
3. Send a single file (you should be able to bind together even mobile pics)
Thank you!