SEMANTICS OF PROGRAMMING LANGUAGES
Learning outcomes of the course unit
Introduce students to: the use of formal methods for the specification of the semantics of programming languages; the use of formal techniques for the verification of the behavior of a program with respect to a partial specification.
Foundations of computer science.
Course contents summary
Definition of operational and denotational semantics of simple imperative programming languages; formal reasoning about the behavior of simple programs; notion of behavioral equivalence of computer programs.
Program syntax and semantics. Structural operational semantics, big-step and small-step. Induction principles and inductive definitions. Denotational semantics. Orderings, domains and fixed points. Axiomatic semantics. Verification of program correctness. Introduction to the static analysis of programs.
The Semantics of Programming Languages: An Elementary Introduction using Structural Operational Semantics. Matthew Hennessy, Wiley, 1990. [http://www.cogs.susx.ac.uk/users/matthewh/semnotes.ps.gz]
La Semantica Formale dei Linguaggi di Programmazione. Glynn Winskel. MIT Press, 1993.
Lectures and exercise sessions.
Assessment methods and criteria
Students will be evaluated by means of: home assignments to be handed in in one week time; realization of a final project; concluding oral examination.