Lecture 1: Hilbert Calculus, Natural Deduction, Sequent Calculus
Teacher: Michele Pagani
Linear Logic and logical paradigms of computation (M2 MPRI)
Exercise Sheet 1:
Teacher: Michele Pagani
Exercise Sheet 3:
Teacher: Delia Kesner
Lecture 2: MLL/MALL/MELL, Lafont menu, Negative encoding
Teacher: Michele Pagani
Lecture 3: Proof nets
Teacher: Michele Pagani
Lecture 4: Cut-elimination for MLL
Teacher: Michele Pagani
Lecture 5: Language-oriented MELL
Teacher: Delia Kesner
Lecture 6: MELL Proof nets
Teacher: Delia Kesner
Lecture 7: Static translation
Teacher: Delia Kesner
Lecture 8: $λlxr$-calculus vs. $λ$-calculus
Teacher: Delia Kesner
Lecture 9: Cost models
Teacher: Beniamino Accatoli
Lecture 10: Abstract Machines
Reminder:
Lecture 11:
Important concepts in rewriting theory: when redexes are created
TD: Abstract Machines
Exercise 1
Lecture 12: Building Intuitionistic and Classical proofs
Teacher: Dave Miller, INRIA
Lecture 13: Abstract Logic Programming
Abstract Logic Programming: Proof theory formulations (corresponds to chapter 5 in Dave Miller’s lecture notes)
Lecture 14: The $\bullet ; \bullet ⊢_o \bullet$ Proof System
[⊢_O = ⊢_I = ⊢_C \qquad hC ⊆ hH \qquad ⊢_O = ⊢_I]