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 CurryHowardLambek correspondence between proofs, programs and denotational semantics, with an emphasis on the prooftheoretical 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:
 SetTheoretic Denotational Semantics.

CurryHoward Correspondence:
 Minimal Intuitionistic Logic [slides].

Gödel's System T:

Course 4 (30th Sept. 2020).

CurryHoward Correspondence:
 Full Intuitionistic Propositional Logic [slides].

Categories:
 Definition and Basic Examples.

CurryHoward Correspondence:

Course 5 (7th Oct. 2020).

Categories:
 Finite Products.

Categories:

Course 6 (14th Oct. 2020).

Categories:
 Cartesian Closed Categories.
 Interpretation of the SimplyTyped LambdaCalculus.

Categories:

Course 7 (22nd Oct. 2020).

Cartesian Closed Categories:
 LambdaTheories.

PCF:
 Definition [slides].

CPOs and Scottcontinuity:
 Definitions.
 CPOs and Scottcontinuous functions form a CCC.

Cartesian Closed Categories:

Course 8 (4th Nov. 2020).

Denotational Semantics of PCF in CPOs:
 Scottcontinuous functions on nat.
 Interpretation of fixpoints.
 Continuity of stream functions [slides].
 Comments on the homework.

Denotational Semantics of PCF in CPOs:
Back home.