Logical Foundations of Programming Languages

General Informations

• Course CR17 of the M2IF, ENS de Lyon.
• Main page of the course.
• Lecturers:
  • Olivier Laurent (Thursday 1:30pm - 3:30pm).
  • Colin Riba (Wednesday 8:00am - 10:00am).
• Description:
  • The objective of this course is to present the three sides of the Curry-Howard-Lambek correspondence between proofs, programs and denotational semantics, with an emphasis on the proof-theoretical insights provided by Linear Logic.
• Homework:
  • The homework in [pdf] (with corrections of a few typos).
  • To be completed for the 1st of November 2020 (see instructions inside).

Wednesday Courses

• Course 1 (9th Sept. 2020).
  
  • Introduction [slides].
  • Gödel's System T:
    • Definition and Basic Properties.

• Course 2 (16th Sept. 2020).
  
  • Gödel's System T:
    • Normalization.

• Course 3 (23rd Sept. 2020).
  
  • Gödel's System T:
    • Set-Theoretic Denotational Semantics.
  • Curry-Howard Correspondence:
    • Minimal Intuitionistic Logic [slides].

• Course 4 (30th Sept. 2020).
  
  • Curry-Howard Correspondence:
    • Full Intuitionistic Propositional Logic [slides].
  • Categories:
    • Definition and Basic Examples.

• Course 5 (7th Oct. 2020).
  
  • Categories:
    • Finite Products.

• Course 6 (14th Oct. 2020).
  
  • Categories:
    • Cartesian Closed Categories.
    • Interpretation of the Simply-Typed Lambda-Calculus.

• Course 7 (22nd Oct. 2020).
  
  • Cartesian Closed Categories:
    • Lambda-Theories.
  • PCF:
    • Definition [slides].
  • CPOs and Scott-continuity:
    • Definitions.
    • CPOs and Scott-continuous functions form a CCC.

• Course 8 (4th Nov. 2020).
  
  • Denotational Semantics of PCF in CPOs:
    • Scott-continuous functions on nat.
    • Interpretation of fixpoints.
    • Continuity of stream functions [slides].
  • Comments on the homework.

Back home.