IFIP WG 2.2 Tutorial Section

20-21 April 2007

IPM, Tehran, Iran

An introduction to the semantics of programming languages: theory and practice

**Abstract:**

A semantics of a programming language is an abstract mathematical model of the intended behaviour of all the programs in the language. In these lectures I shall give an introduction to the main formalisms that have been developed for specifying such models:

* operational semantics, where the model represents the computations of programs quite directly;

* denotational semantics, where the model represent the contribution of each part of a program to the overall behaviour of the entire program; and

* axiomatic semantics, where the model involves the relationship between pre- and post-conditions on program variables.

Although the above formalisms have strong theoretical foundations, they also have some pragmatic weaknesses- especially concerning modularity. I shall present some variants of the main formalisms which remove these weaknesses, and allow the semantics of each language construct to be specified independently as a separate, reusable component.

The lectures assume familiarity with the use of formal grammars to specify the syntax of programming languages, and with standard concepts from set theory and predicate logic.

An introduction to the semantics of concurrency:

behavioural equivalences and co-induction

**Abstract:**

In the lectures I will introduce some basic concepts for the semantics of concurrent systems and languages.

A fundamental concern in concurrency theory is establishing when two processes are "the same", i.e., indistinguishable to an external observer interacting with them. This notion, called, behavioural equivalence, is the basis upon which a theory of processes can be developed.

I will review the main forms of behavioural equivalence. I will devote more time to bisimulation, for its importance and mathematical properties. In particular, I will discuss the bisimulation proof method. This is an instance of a general proof technique called co-induction that is today widely used also outside concurrency theory.

If time allows, I will also discuss the use of these notions in basic formalisms for the description and analysis of concurrent systems and languages, such as CCS and the pi-calculus.