Students should be familiar with basic notions of set theory and
formal logic (validity and provability, correctness and completeness
of deductive systems, etc.)
Course Enrollment Limitations
The course is also offered to the students of the fields other than those the course is directly associated with.
Fields of study the course is directly associated with
there are 23 fields of study the course is directly associated with, display
Course objectives
An introduction to the theory of formal semantics of programming
languages (operational, denotational, and axiomatic semantics).
Main objectives of the course can be summarized as follows:
to understand basic types of formal semantics of programming
languages; to be able to reason about properties of programs using formal semantics; to understand basic notions of temporal logics.
Syllabus
Formal semantics of programming languages, basic paradigms
(operational, denotational, and axiomatic approach).
Structural operational semantics and its variants (small-step and
big-step semantics).
Denotational semantics. Complete partial orders, continuous functions.
The fixed-point theorem and its applications, semantics of
recursion. Equivalence of operational and denotational semantics.
Axiomatic semantics. Hoare's deductive system, its correctness
and completeness.
Temporal logics; the semantics of non-terminating and
parallel programs.
Literature
WINSKEL, Glynn. The formal semantics of programming languages : an introduction. Cambridge: MIT Press, 1993. xi, 361 s. ISBN 0-262-23169-7. info
SCHMIDT, David A. The structure of typed programming languages. Cambridge: MIT Press, 1994. viii, 367. ISBN 0-262-19349-3. info
Teaching methods
Lectures, tutorials.
Assessment methods
Lectures: 2 hours/week. Tutorials: 1 hour/week.
Written exam.