## 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)
• ### 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 .