CR02: Linear Logic and Game Semantics (2014-2015)

Monday 10:15am - 12:15pm in room B1


The course will start with an introduction to the proof theory of linear logic. This refinement of intuitionistic logic was introduced by Jean-Yves Girard in 1986 and is now one of the main tools in the fine-grained analysis of proof theory of propositional logic, but also a key ingredient for the study of denotational semantics of functional languages.

Probably the most original contribution to denotational semantics of the last twenty years, game semantics took its inspiration from linear logic and allows us to interpret a wide range of programming languages in a very precise way. The interpretation is based on a interactive presentation of the execution traces of programs which provides us with a compositional (i.e. modular) interpretation of programs. The course will mainly focus on the so called Hyland-Ong/Nickau approach to game semantics.



Content (preliminary)



General References

Lecture 1

Lecture 2

Lecture 3

Lecture 4

Lecture 5

Lecture 6

Lecture 7

Lecture 8

Lecture 9

Lecture 10

Lecture 11

Lecture 12


Main evaluation will be a final exam.

Additional evaluation (leading to bonus on the final grade) will be based on homework (probably every two weeks).


Other informations on the page of the 2013-2014 course.