Theory Mini-Course 2000-01

Syntax and Semantics of Programming Languages

Marcelo Fiore

Computer Laboratory

Description

This mini-course is about the mathematical structure of programming languages regarded as syntactic objects equipped with a computational semantics.

In Part I, I will start by recalling the basics of the algebraic approach to understanding abstract syntax and follow by presenting an extension that incorporates binding operators. With this background, in Part II, I will consider a unified framework for giving structured, compositional semantics to process calculi. Our running examples will be CCS, value-passing CCS, and the pi-calculus.

The aim of the mini-course is to offer tools for thinking about syntactic and semantics aspects of programming languages in a principled manner.

Topics

Part I.

Signatures. Algebraic syntax. Substitution. Initial algebra semantics. Inductive types. Structural recursion.
Binding signatures. Algebraic syntax with variable binding. Capture-avoiding substitution. Initial algebra semantics.

Part II.

Coalgebraic transition systems. Bisimilarity. Final coalgebra semantics. Structural operational semantics. Compositionality, full abstraction, congruence. Examples: CCS, value-passing CCS, pi-calculus.

References

Part I.

M.Fiore, G.Plotkin, and D.Turi. Abstract syntax and variable binding. In 14th Logic in Computer Science Conference, pages 193-202. IEEE, Computer Society Press, 1999. (See http://www.cl.cam.ac.uk/~mpf23/papers/Types/Types.html.)

M.Gabbay and A.Pitts. A new approach to abstract syntax involving binders. In 14th Logic in Computer Science Conference, pages 214-224. IEEE Computer Society Press, 1999. (See http://www.cl.cam.ac.uk/users/amp12/papers/index.html.)

Part II

D.Turi and G.Plotkin. Towards a mathematical operational semantics. In 12th Logic in Computer Science Conference, pages 280-291. IEEE, Computer Society Press, 1997. (See http://www.dcs.ed.ac.uk/home/dt/towards.html.)

M.Fiore, E.Moggi, and D.Sangiorgi. A fully-abstract model for the pi-calculus . In 11th Logic in Computer Science Conf. (LICS'96), pages 43-54. IEEE, Computer Society Press, 1996. (See http://www.cl.cam.ac.uk/~mpf23/papers/Concurrency/Concurrency.html.)

M.Fiore and D.Turi. Semantics of Name and Value Passing. To appear in 16th Logic in Computer Science Conference. IEEE, Computer Society Press, 2001. (See http://www.cl.cam.ac.uk/~mpf23/papers/Concurrency/Concurrency.html.)