Semantics of programming languages

The aim of the course is to introduce students to the basics of programming language semantics, which forms the foundation for the study and implementation of programming languages. These techniques are also important for program verification, the implementation of optimizations, and the general design of programming languages.

The emphasis will be on comparing operational and denotational semantics. The techniques used are also applicable when analysing languages specified only by an operational semantics. The course will enable students to acquire the skills needed to implement language constructs, regardless of whether their description comes from theoretical or engineering sources in the literature.

Outline

1. Course overview, motivation, and relation to practical programming language design and implementation.
2. Rule-based and structural induction, relationship between operational and denotational semantics.
3. Contextual and big-step semantics.
4. Abstract machines and continuations.
5. Typed lambda calculus with arithmetic.
6. Semantic and type soundness.
7. Semantic completeness.
8. Recursive functions and the language PCF.
9. Adequacy and the contextual lemma.
10. The problem of full abstraction for PCF.
11. Hoare logic I.
12. Hoare logic II.
13. Additional topics.

Literature

1. Winskel, G.: The Formal Semantics of Programming Languages. MIT Press, 1993.
2. Hutton, G. Programming Language Semantics It’s Easy As 1,2,3. Journal of Functional Programming, 2023.
3. Robert Harper: Practical Foundations for Programming Languages, 2nd Edition. Cambridge University Press, 2016.
4. Tobias Nipkow , Gerwin Klein: Concrete Semantics, With Isabelle/HOL. Springer Cham, 2014.
5. Streicher, T: Domain-theoretic foundations of functional programming. World Scientific Publishing Company, 2006.
6. Tennent, R. D.: Semantics of Programming Languages. Prentice Hall, 1991.
7. Gunter, C. A.: Semantics of Programming Language. MIT Press, 1992.