Zhejiang-Cambridge Talk Series: Programming Language Semantics

TIME: 2022-09-29

SPEAKER:

Andrew Pitts
Professor of Theoretical Computer Science
Department of Computer Science & Technology
University of Cambridge, UK

TITLE:

Programming Language Semantics

ABSTRACT:

There are very many programming languages. They often arise to meet the needs of particular application areas, from numerical computing for scientific applications in the early days of computers to the need for user interaction within a web browser or phone app in the age of the internet.

A new programming language always arrives with an implementation. Usually one also gets a precise mathematical description of its grammar using well developed tools from formal language theory, so one knows exactly what is, and is not, a legal program in the language. One might also get an informal description of how programs are supposed to behave, written in natural language. But it is much rarer (and much harder) to have a precise mathematical description of the meaning of an arbitrary legal program, independent of any particular implementation. Indeed sometimes it can be hard to
agree upon what “program meaning” should mean!

Computer scientists have devised various methods for precisely describing the semantics of programming languages, making use of various kinds of mathematics and logic, sometimes in ways that are
unfamiliar to mainstream mathematics. In this talk I will survey some of these developments trying to be as non-technical as I can. We will look at various styles of programming language semantics and compare their answers to the fundamental question: when are two program phrases semantically equivalent?