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.
-
Gödel's System T:
-
Course 3 (23rd Sept. 2020).
-
Gödel's System T:
- Set-Theoretic Denotational Semantics.
-
Curry-Howard Correspondence:
- Minimal Intuitionistic Logic [slides].
-
Gödel's System T:
-
Course 4 (30th Sept. 2020).
-
Curry-Howard Correspondence:
- Full Intuitionistic Propositional Logic [slides].
-
Categories:
- Definition and Basic Examples.
-
Curry-Howard Correspondence:
-
Course 5 (7th Oct. 2020).
-
Categories:
- Finite Products.
-
Categories:
-
Course 6 (14th Oct. 2020).
-
Categories:
- Cartesian Closed Categories.
- Interpretation of the Simply-Typed Lambda-Calculus.
-
Categories:
-
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.
-
Cartesian Closed Categories:
-
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.
-
Denotational Semantics of PCF in CPOs:
Back home.