Logical Foundations of Programming Languages

General Informations

• Course CR03 of the M2IF, ENS de Lyon.
• Main page of the course.
• Lecturers:
  • Olivier Laurent (Monday 10:15am - 12:15pm).
  • Colin Riba (Thursday 3:45pm - 5:45pm).
• 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].
  • To be returned before the course of the 28th of October 2021 (see instructions inside).

Thursday Courses

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

• Course 2 (16th Sept. 2021).
  
  • Gödel's System T:
    • Set-Theoretic Denotational Semantics.
  • Categories:
    • Definition and Basic Examples.

• Course 3 (23rd Sept. 2021).
  
  • Categories:
    • Finite Products.

• Course 4 (30th Oct. 2021).
  
  • Categories:
    • Cartesian Closed Categories.
    • Interpretation of the Simply-Typed Lambda-Calculus.
    • Lambda-Theories.
    Reference:
    • Chapter 4 of the book
      Domains and Lambda-Calculi, R. Amadio & P.-L. Curien.

• Course 5 (7th Oct. 2021).
  
  • PCF [slides].
  • The CCC of CPOs and Scott-Continuous Functions.
  • Denotational Semantics of PCF in CPOs.

• Course 6 (14th Oct. 2021).
  
  • Categories:
    • Functors.
    • Natural Transformations.

• Course 7 (21th Oct. 2021).
  
  • Categories:
    • Universal Arrows.
    • Adjunctions.
      
      • Chapter IV of the book:
        Categories for the Working Mathematician, S. Mac Lane.

• Course 8 (28th Oct. 2021).
  
  • Categories:
    • Monads.
    Reference:
    • Chapter VI of the book:
      Categories for the Working Mathematician, S. Mac Lane.

Back home.