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:
- Ex 2.Point 2: write a type derivation for this term, using the type we found in class
- Ex 2. Points 3, 4, 6. Are these term typable? If yes, provide a derivation).
- Ex 6.
- 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):
- Is the following statement derivable? If yes, please write the derivation.
(I(\lambda x.xxx)) false \Downarrow false
- From TD8: Ex 1 (case CbV). -- Prove that in weak CbV, the closed normal forms are exactly the values.
- 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:
- Include your NAME in the file_name:
Example: DM1_PaoloRossi.pdf, HW2_MarieEtudiante.pdf
- If possible, send a single file (you should be able to bind together even mobile pics)
Thank you!