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.
ILL)IMLLMain evaluation will be a final exam.
Additional evaluation (leading to some bonus on the final grade) will be based on homework (probably 2 to 4 times).