ASM : Advanced Semantics

Description

The objective of this course is to acquire the fundamental concepts and tools for understanding the scene behind programming languages.

Keywords

Semantics, type theory, program logics, compilation, software verification.

Contents

1. Denotational semantics.
2. Continuation semantics and CPS programming.
3. Type systems. Correction and inference. Polymorphism. Dependant types.
4. Program logics. Hoare Logic. Separation Logic.

Bibliography

• Glynn Winskel. 1993. The Formal Semantics of Programming Languages: An Introduction. MIT Press, Cambridge, MA, USA.
• David A. Schmidt. 1986. Denotational semantics: a methodology for language development. Allyn & Bacon.

Planning

22/11		introduction, denotational semantics
23/11	no lecture
29/11		denotational semantics and continuations
30/11		continuations (ctd')
06/12	no lecture
07/12		PCF : calling strategies	Aurèle Barrière : Pretty-big step semantics
13/12	no lecture
14/12		PCF : interpretation	Thomas Mari : Representing Control in the Presence of First-Class Continuations Bastien Thomas The Essence of Compiling with Continuations
20/12		PCF: compilation	Joshua Peignier : A syntactic approach to type soundness
21/12	no lecture
10/01		PCF: static typing, denotational semantics
11/01		types and proofs, axiomatic semantics	Yassir Anouar : An efficient unification algorithm
17/01		axiomatic semantics (ctd.)
18/01		axiomatic semantics (end)	Solène Mirliaz : Separation Logic : a Logic for shared mutable Data Sructures
24/01	exam
25/01	no lecture