Preuves et programmes : Outils classiques (LMFI 2023/2024). Part 1.

• 09/01: 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 22
  Bonus points (by January 20): EX at slide 39


• 10/01, 16h15-18h15: Slides Abstract Rewriting : Confluence, Commutation, Factorization
  - TD0
  - CC: Homework 1 (and some notes) Deadline: January 22
  
  
• No class
• No class


• 23/01: Slides Terms and programs: Call-by-Value Lambda Calculus
  Memo CbN CbV lambda calculus
  Bonus points (before the class on 24/01): "Fact 6 (?)" at slide 75 TYPOS in bonus exercise (sorry): there is a Latex problem with question 2, which should be similar to question 1:
  
  1. M -->_l * V iff M -->_r * V . True?
  2. M -->_w * V iff M -->_l * V . True?
  However, you can safely skip question 2.


• 24/01 14h00
  - TD1 Make your own normalization strategy.
  - Homework 2: From the TD1:
  
  1. Prove Lemma 7, point 2 (preservation of weak normal forms).
  2. Prove either:
     • (easier) Fact 7, Ex B, at the end pag 2 in TD1 OR
     • (more points) Theorem 10 (CbN or CbV)
  Please do not submit more exercises than required! (if you do more, just send your best)


• 30/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 (by Jan 31, 16h00): 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
  
  
• 31/01, 16h15: Proof Nets, the graph syntax of Linear Logic
• Slided MLL Proof Nets
• TD MLL proof-nets
• HOMEWORK 3 (due before next class)
  • QUICKLY DONE: from the Slides Intro to Linear Logic : Ex 1.1 at slide 13 and Ex 2.3 at slide 18. Please use one-sided sequents
  • MAIN: EX on proof-nets (please fill the form online, putting your name)


• 06/02, Proof Nets, the graph syntax of Linear Logic
  Slided Proof Nets


• 07/02, 16h15 MELL Proof Nets
  
  • Slides Proof Nets (including MELL)
  • TD MELL <--- these questions are part of today class (this is NOT homework!)
  • Homework 4 HW4: Computing with Proof-Nets Due: February 13
    Instructions: Pick 2 questions in the "Multiplicative Booleans" Section. (Note: Question 2 and 3 bring no point!).
  • BONUS QUESTION (deadline: Feb 21, our last class) : slide 61 Just work with MLL (even with MLL, this exercise is more demanding than usual)
  • Notes on Proof Nets (by O. Laurent)


• 13/02 Complements on Linear Logic: Sequentialization, Translation of Lambda Calculus, Geometry of Interaction. Some elements in current research


• 14/02, 16h15 Today we focus on understanding inductive and co-inductive definitions. Technically, it all rests on Tarski-Knaster Theorem.
• Slides: Intro to Co-inductive techniques and Simulation
• Big Steps/Small Steps Semantics : TD Operational Semantics/Weak reduction (Ch. 8 in Amadio's book)
• Homework 5 (due before next class): EX 1 and Ex 2: see slides 44-48. Note that CbN convergence (in slide 45, 46, 49) is defined in the TD Operational Semantics


• 20/02. Programs Equivalence: Contextual Equivalence and Applicative Bisimilarity
  • Slides: Sum-Up Co-inductive techniques and Simulation
  • TD Simulation


• 21/02, 14h00. Applicative Bisimulation, Howe method for higher-order languages.
  Today we prove that the largest simulation coincides with the contextual pre-order.. Which is a bit surprising (at least for me).
  Last BONUS Exercise: 1+1 =2 ? (deadline: March 4). Prove that the terms succ one and two (slide 18 here ) are CbV applicatively bisimilar The definition of CbV simulation is in the TD Simulation. (if CbV is difficult, you can also use CbN)

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 (Applicative Similarity).
• Co-Induction. Please email me to receive the chapters.

About Homework:

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)