Preuves et programmes : Outils classiques (LMFI 2022/2023)

Part 2

• 08/02: Slides
Please email me if you wish to receive the lecture notes on Abstract Rewriting

- CC: Homework 1 (and some notes) Deadline: February 20



• 21/02: Slides


• 22/02: Slides
  Memo CbN CbV lambda calculus
  Homework 2. Due before next lesson (so by 27/02).
  
  1. Prove the Lemma in slide 56 (also found as Lemma 1 in These notes )
  2. From the TD1:
     
     • Prove Lemma 7, point 2 (preservation of weak normal forms).
     • Optional: Fact 7, Ex B. (end pag 2 in TD1)
  
  
• 28/02:
  • We have proved CbN head normalization (classical result for lambda calculus) and CbV convergence (classical result by Plotkin 75)
    
  • BONUS exercise: TD1, ex C: assuming head factorization, prove that leftmost outermost reduction is a normalizing strategy for beta reduction.
  • Slides Linear Logic
  • Homework 3.1 : Ex 1 (on slide 13) due before the class on March 1


• 1/03:
  • Build your own normalizing strategy
  • Proof Nets, the graph syntax of Linear Logic (MLL)


• 2/03: 8h45, room 2014. Proof Nets, the graph syntax of Linear Logic. Material and Lecture Notes are listed at the end of the page.
  • Slides Linear Logic
  • Slided Proof Nets
  • TD MLL proof-nets
  • Homework 3.2 Due: March 06
    • EX. on Slide 18 (dont do point 3 if you have done in class already)
    • BONUS exercise: which property of confluence holds for MELL reduction?
      Please answer YES NO or DIFFICULT TO CHECK. If you answer YES or NO, please justify your answer
      
      1. Is diamond?
      2. has Random Descent?
      3. is locally confluent?
      4. is strongly confluent?
      5. is confluent?
      The reducition rules are here MELL reduction rules
  
  
  • 7/03: Slides Proof Nets (including MELL)
    Notes on Proof Nets (by O. Laurent)
  
  
  • 8/03: Slides Proof Nets (including MELL)
    
    • Homework 4 HW4: Computing with Proof-Nets Due: March 14
      Instructions: Pick (up to) 3 questions in the "Multiplicative Booleans" Section. (Note: Question 2 brings no points. Question 3 is ok to submit).
    • BONUS QUESTION A (deadline: March 21) : To prove weak normalization of MELL reduction, we have proved together that the strategy "choose a maximal cut at maximal depth" terminates. (See also Proposition 2.2 in these notes on Proof Nets ). The choice of a cut to reduce is clearly non unique, so the strategy is non-deterministic.
      Question: this strategy has random descent? That is, the number of steps to termination is always the same?
    • BONUS QUESTION B (deadline: March 21) : slide 60 Just work with MLL (even with MLL, this exercise is more challanging than usual)
  
  
  • 14/03: Today we focus on understanding inductive and co-inductive definitions. Technically, it all rests on Tarski-Knaster Theorem.
  • Slides
  • Homework 5.1 : EX 2, Slide 42 (try to do before next class, if possible) More technical homework (due by March 20) to come
    



• 15/03:
  • Operational Semantics/ Weak reduction (Ch. 8 in Amadio's book)
  • Slides Coinduction/Simulation
  • Homework 5 (due before the class on March 22): Ex 1, Ex 2, Ex 3 in the Slide 14-18 here



• 21/03: NO CLASS TODAY: This class is moved to 28/03


• 22/03: Programs equivalence and Applicative Bisimulation. Today we work with CbN and CbV simulation. We prepare the ground for proving that two terms are contextual equivalent iff they are bisimilar Said otherwise: the largest simulation coincides with the contextual pre-order.
  • TD on Applicative Simulation
  • Homework 7 : Ex. 5 point 4 or 3 (from the TD above) and HW7 Due: Tuesday 28/03 (before class)
    


• 28/03: Applicative Bisimulation, Howe method for higher-order languages. We finally prove that the largest simulation coincides with the contextual pre-order.. Which is a bit surprising (at least for me).



---

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 .
  
• Notes on CbN and CbV weak reduction / Contextual equivalence and simulation (Lambda Calculi as core functional languages):
  • Lecture notes by L. Ong: Section 5 (and 6)
  • Operational methods in semantics by R. Amadio: Chapter 8 (weak reduction) and 9 (simulation).
• Co-Induction. Please email me to receive the notes.

---

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!