Semantics of Programming Languages
| Code | Completion | Credits | Range | Language |
|---|---|---|---|---|
| NI-SEM | Z,ZK | 5 | 2P+1C | Czech |
- 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:
- 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:
- 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:
-
- Quantum Informatics (elective course)
- Mgr. programe Applied informatics (code ANIE) for the phase of study without specialization (elective course)
- Master specialization Embedded systems (elective course)
- Master specialization Business Informatics, 2026 (elective course)
- Master specialization Software Engineering (elective course)
- Master specialization Web Engineering (elective course)
- Master specialization Visual computing and Game design (elective course)
- 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 Czech, 2026 (VO)
- Master specialization Computer Systems and Networks, in Czech, 2026 (VO)
- Master specialization Computer Science, in Czech, 2026 (VO)
- Master specialization Programming Languages, in Czech, 2026 (PS)
- Master specialization Artificial Intelligence, in Czech, 2026 (VO)
- Master programme, for the phase of study without specialisation, ver. for 2026 and higher (VO)
- Master programme, for the phase of study without specialisation, ver. for 2026 and higher (VO)