Semantics of Programming Languages

Course guarantor:

Lecturer:

Tutor:

Supervisor:

Department of Theoretical Computer Science

Synopsis:

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.

Requirements:

Syllabus of lectures:

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.

Syllabus of tutorials:

1. Language IMP- and its operational and denotational semantics.

2. Extension of IMP- to IMP and its operational and denotational semantics.

3. Basic properties of CPOs, their constructions and CPO interpretation of lambda calculus.

4. Logical relations as a useful technique, with applications for denotational semantics and beyond.

5. The equivalence of operational and denotational semantics.

6. Axiomatic semantics.

Study Objective:

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.

Study materials:

1. Robert Harper: Practical Foundations for Programming Languages, 2nd Edition. Cambridge University Press, 2016. ISBN9781107150300.

2. Winskel, G.: The Formal Semantics of Programming Languages. MIT Press, 1993. ISBN 9780262291453.

3. Tobias Nipkow , Gerwin Klein: Concrete Semantics, With Isabelle/HOL. Springer Cham, 2014. ISBN 978-3-319-10541-3.

4. Streicher, T: Domain-theoretic foundations of functional programming. World Scientific Publishing Company, 2006 ISBN 981-270-142-7.

5. Tennent, R. D.: Semantics of Programming Languages. ISBN 9780138055998.

6. Gunter, C. A.: Semantics of Programming Language. MIT Press, 1992. ISBN 9780262570954.

Note:

Further information:

bude doplněno

No time-table has been prepared for this course

The course is a part of the following study plans:

• Master specialization Software Engineering (elective course)
• Master specialization Embedded systems (elective course)
• Master program ANIE for the phase of study without specialisation (elective course)
• Quantum Informatics (elective course)
• Master specialization Computer Security, in English, 2026 (VO)
• Master programme, for the phase of study without specialisation, ver. for 2026 and higher (VO)
• Master specialization Computer Systems and Networks, in English, 2026 (VO)
• Master specialization Computer Science, in English, 2026 (VO)
• Master specialization Programming Languages, in English, 2026 (PS)