Homework 1 (due by 23/09): one quick graded exercise, plus (optional) a bonus question (to collect one extra point). If you have questions,
email me, or post in Discord.
(Graded): Exercise @ slide 17 in
LL slides
(IMPORTANT for next lesson). Slide 16 describes the logical steps in a cut-elimination procedure for LL. As we discussed in class,
these steps are not enough to eliminate the cuts from a derivation.
How do we treat the non-logical steps? As you imagine, similarly to classical or intuitionistic logic.
Please complete the two cases in slide 17: write the derivation with the cut as described in blue, and write how it should be transformed.
Bonus point: last question @ slide 21 in ARS slides . Do not use AI. Honor code. For bonus points, we will rely on a honesty system:
points are valid if, when emailing your solution, you explicitely declare that you did not use AI help.
That is all this first week. I prefer to postpone the announced exercise (you prove a quantitative rewriting property) to next week, after we have done
some practice together on other proofs.
No in-class graded exercises on 24/09.
***PLEASE CHECK THE INSTRUCTIONS FOR SUBMITTING HOMEWORK AT THE BOTTOM OF THIS PAGE***
24/09: Proof Nets, the graph syntax of Linear Logic. More on Linear Logic.
NO in-class graded exercises.
Homework 2 (due by 30/09) . Please, do not use AI.
EX1. Slides 27-30 in Multiplicative (MLL) Proof Nets
Please email the indicated proof-net, and its reduction. Camera pics of hand-written graphs are fine!
EX 2 and some notes. This exercise is about a quantitative properties in rewriting. Ideally, your solution should
be no longer than 1/2 page
- Exercise 1. Grade validation: stating that you did not use AI suffices--- here we adopt the honesty system.
- Exercise 2. Strive for a clear, concise proof. Once we have a correct proof,
it is just the beginning: to make it as elegant and simple as possible, it is the way to really understand and be able to use a property we uncovered.
Training on this kind of effort is time well spent.
Grade validation: the grade is determined (also) by a few in-class questions on the proof and its implications.
POLL (non graded) : please answer online to this
poll on MLL normalization .
The purpuse of the exercise is to allow you to think about the properties of the system -- There is no grade: think on your own.
01/10: MELL Proof-Nets. More on Abstract Rewriting. Sequentialization. Short in-class graded exercises (questions related to Homework 2 + one question on LL sequent calculus).
All documents allowed (eg: slides, your notes, any textbook, etc.); computers and mobile phones prohibited during the test.
Sequentialization: the MLL proof-net in slide 21 is the image of any sequent calculus derivation ? Provide one
Bonus: an alternative proof of Newman Lemma, following the suggestions in slide 39 of the ARS slides
Extra bonus (challanging, valid till 21/10, ) : bonus exercise,
slide 41 in MELL Proof Nets Slides . Feel free to ask in class if clarifications are needed.
8/10:
NO CLASS
15/10, 8h45-10h20 -- ONLINE CLASS (find the Zoom link on Discord, or email me)
MELL proof nets. Calculi: Call-by-Name and Call-by-Value. Rewriting: strategies and factorization.
short in-class graded exercises (question on MELL proof-nets)
Lab (aka TD, here ) on Proof-Nets reduction rules
Even if we are online, we try to work together on MELL normalization: if at all possible, do not hesitate to phisically meet with some class-mates, to team-up
Bonus: Have you already met (in your studies) any system which satisfies the quasi-diamond condistions in Homework 2
quasi-diamond condistions in Homework 2 ?
Please provide an example of a 'real' system, if you have seen one, or otherwise build a suitable one.
In preparation of the class on 22/10: asynchronous TD on Weak Call-by-Value Lambda Calculus.
These are ungraded exercise. I propose to work on the TD asynchronously, before the class, rather than online. You are very welcome to team up with classmates and
send a single form per team.
Please use this
CbV Reference Sheet, and
CbV slides (from 9 to 19, only)
EX 0 (preliminary exercise). Consider the three CbV sub-reduction at slide 18. Let M be a *closed* term.
Prove that M is a normal form for W-reduction iff M is a value
EX 1.
Online form. Please answer the questions (and justify your answer)
in the online form (questions are from slide 19).
Extra question: in the two exercises above, does it matter that the term M is closed? Why?
22/10, 8h45-10h45 -- ONLINE CLASS ( Zoom link on Discord)
Material and Lecture Notes
Linear Logic:
J.-Y. Girard: Linear Logic. Theor. Comput. Sci. 50: 1-102 (1987)
Honor code (no AI use).
For graded homework, you are asked not to use AI. We will rely on a honesty system:
points are valid if, when emailing your solution, you explicitely declare that you did not use AI help.
Homework submission:
Please:
Send by email-- please start the email subject with MPRI (my spam filter is very aggressive)
Include your NAME in the file_name:
Example: DM1_PaoloRossi.pdf, HW2_MarieEtudiante.pdf
Send a single file (you should be able to bind together even mobile pics)