TD Semantique des langages de programmation (M1 2021/2022)

Course Main Page

First week: Abstract Rewriting Systems

  • 26/01: Slides ARS (most slides comes from Middeldorp's beautiful class)
    Updated on 27/01 (proofs added)
    Collect your first bonus point: slide 20. (Deadline: Jan 27, 14:00)

    • TD sessions:

  • 27/01: TD1
    CC Homework 1. Deadline: February 7. Home1 (Notice that there are three exercises!)

  • 10/02: TD3
    - CC: Homework 2. From TD3 : Ex 4.2, Ex 5. Deadline: February 16.
    Higly recommende before next time (not rated): Ex. 6.1.1 (evaluate the terms)
    Bonus point (optional): Ex. 6.2.1 (define a term T which iterates n times a function f starting from m).

  • 17/02: TD3
    SLIDES Recursive Functions
    - CC: Homework 3. (1) Encode multiplication, (2.) Compute: fact 2 (See Slides) Deadline: February 22


  • 23/02: TD + 40 min in class partial exam on lambda calculus
    No Homework. Bonus point (optional): Ex. 9 from TD3 Deadline: March 3


  • 02/03: vacations

  • 9/03: typed lambda calculus: TD6 and Memo
    • CC: Homework 4. Due for March 15. Please do the following, from the TD6:
    1. Ex 2.Point 2: write a type derivation for this term, using the type we found in class
    2. Ex 2. Points 3, 4, 6. Are these term typable? If yes, provide a derivation).
    3. Ex 6.
    4. Ex 7. Point 1 and 2.


  • 16/03: typed lambda calculus. No new homework.

  • 23/03: TD7: Let-polymorphism
    CC: Homework 5. From TD7. Ex.3: last 3 points. Ex.4: points 2 and 4 (due for March 30 before class)

    30/03 Homework 5. TD8: Operational Semantics
    CC, Homework 6 (due for April 5):
    1. Is the following statement derivable? If yes, please write the derivation.
      (I(\lambda x.xxx)) false \Downarrow false
    2. From TD8: Ex 1 (case CbV). -- Prove that in weak CbV, the closed normal forms are exactly the values.
    3. BONUS (optional) From TD8: Ex 3.2 (case CbN), assuming that the lemma holds (important: we only consider closed terms!)

  • 06/04: TD

  • 07/04: TD

  • 14/04 : 14h30 on ZOOM TD10 Confluence and critical pairs.






    • A nice reference on lambda calculus

    Lecture Notes on Lambda Calculus
    Recommended: Section 3. Programming in the untyped lambda calculus, in particular 3.3 Fixed points and recursive functions .

    About Homework:

    Please:
    1. Include your NAME in the file_name:
      Example: DM1_PaoloRossi.pdf, HW2_MarieEtudiante.pdf
    2. If possible, send a single file (you should be able to bind together even mobile pics)
    Thank you!