M2 LMFI 2025-2026
Preuves et programmes: cours spécialisé
Linear Logic and Quantitative Semantics (Part I)

https://master.math.u-paris.fr/modules/m2lmfi-ppcs/

Organisation
5 weeks, 4 hours per week: January 7th, January 21st, January 28th, February 4th, and March 11th. Courses in the other weeks are taught by Gabriele Vanoni and Patrick Baillot.
Time and place
11am-1pm and 2pm-4pm, location shown here
Language
French or English upon request.

Initial programme

  • January 7th: sequent calculus & abstract machines.
    • Positive connectives: λ-calculus with sums, call-by-value λ-calculus.
    • Abstract rewriting theory with higher-order rewriting systems.
  • January 21st-February 4th (3 weeks): linear logic, tools & applications
    • Unifying call-by-name and call-by-value, application to focusing proof-search for LJ.
    • Linear logic: proof nets, Girard translations, focusing
    • Constructive classical logic through a linear logic lens
  • March 11th: linearity in programming language semantics
    • Linear call-by-push-value: effect and resource modalities
    • Concepts with linearity in programming languages

Details week per week

Week 1 (January 7th)

The first class was cancelled. In the second class, we saw problems with positive connectives (here, sums) in the λ-calculus, and we introduced an alternative term model of computation with an abstract machine calculus, that has three term categories: commands, expressions and contexts. We gave typing rules for the system and saw that the rules correspond to that of sequent calculus.

Notes

Notes in French: GdT Logique 1 (Section 2) and GdT Logique 2 (Sections 1 and 2).

Homework (for January 21st)

To be returned by e-mail or physical paper.

  1. Write down the typing derivations in the λ-calculus corresponding to the commuting conversions between ∨ and both of ∧ and ∨ (4 derivations to write).
  2. In terms of the abstract machine calculus, define tu, πᵢt and δ(t,u,v) together with their typing derivations, such that the derivations correspond to the elimination rules for →,∧,∨ in natural deduction.

Week 2 (January 21st)

We reviewed the calculus from the last time and introduced the notions of underlying sequent, active (e.g. principal) formula, and activation and deactivation. We reviewed the definitions of elimination rules in terms of left-introduction rules. We saw a computational intuition for the three categories t,c,e. We saw how to express structural rules (contraction, weakening) in terms of variable substitution.

We refined the abstract machine calculus to make η-expansions easy to express for all connectives. We introduced a distinction between positive and negative connectives based on their η-expansions, and introduced a new connective: the positive conjunction.

We saw how the η-expansions suggest certain choices in the reductions, and introduced explicit polarity annotations to remove critical pairs in the calculus. We mentioned criteria for a higher-order rewriting system to be confluent: left-linearity and absence of critical pairs. We defined call by name and call by value versions of λ-calculus abstraction and application.

Notes

  • 1st course: GdT Logique 2 (Section 2)
  • 2nd course: for similar material from a paper you can have a look at Polarised Intermediate Representation of Lambda Calculus with Sums (Sections I to III).
  • We have settled on the syntax of polarised intuitionistic sequent calculus (LJpη) from Note on LCBPV figs. 1, 2 & 3 (handed out in class, see also fig. 4) without the connectives !,0,⊤ for the moment (only 1,⊗,⇾,&,⊕).
  • Going further: confluence of higher-order rewriting systems which are orthogonal (left-linear, no critical pair): see Femke van Raamsdonk, “Higher-Order Rewriting” (1999), doi:10.1007/3-540-48685-2_17.

Suggested exercise

  • Write the typing derivations for the η-expansions of ⊗,⇾,&,⊕.

Homework (for January 28th)

  • Consider the λ-term “(λx.z)((λy.yy)(λy.yy))”. Calculate the reductions of this term according to:
    1. the call by name definitions of λ and application (given in class, or cf. Note on LCBPV, fig. 4, column “call-by-name encoding” taking ε=ε₂=⊖)
    2. the call by value definitions of λ and application (given in class, or cf. Note on LCBPV, fig. 4, column “call-by-value encoding” taking ε=ε₁=ε₂=+)
  • (Optionally) If you are unsatisfied with your previous answers to homework n°2 from January 7th (derivation of elimination rules from left-introduction rules), and wish to do it again, or if you did not return anything yet, you can do so.

Week 3 (January 28th)

Week 4 (February 4th)

Week 5 (March 11th)