Formal Programming Language Semantics (U01961)

? Credit Points : 10 ? SCQF Level : 10 ? Acronym : INF-4-FPLS

A formal semantics for a programming language is a mathematically precise description of the intended meaning of each construct in the language. In contrast to a formal syntax for a language, which tells us which sequences of symbols are correctly formed programs, a formal semantics tells us what programs will actually do when we run them. The ideas of semantics are of importance for language designers, compiler writers, and serious programmers; they also provide a mathematical basis for proving the correctness of programs. The aim of this module is to give an introduction to various approaches to formal semantics (operational, denotational and axiomatic), illustrating them by means of some simple imperative, functional, and object-oriented languages. The emphasis is on the more established techniques and their application to full-scale programming languages (particularly Java and Standard ML).

Entry Requirements

? Pre-requisites : Ideally, both Language Semantics & Implementation and Functional Programming & Specification. Successful completion of Year 3 of an Informatics Single or Combined Honours Degree, or equivalent by permission of the School. Some mathematical aptitude is also expected.

Variants

? This course has variants for part year visiting students, as follows

Formal Programming Language Semantics (VS1) (Semester 1 (Blocks 1-2))

Subject Areas

Home subject area

Theoretical Computer Science, (School of Informatics, Schedule O)

Delivery Information

? Normal year taken : 4th year

? Delivery Period : Semester 1 (Blocks 1-2)

? Contact Teaching Time : 2 hour(s) per week for 10 weeks

First Class Information

Date	Start	End	Room	Area	Additional Information
21/09/2007	09:00	09:50			Appleton Tower, Room 5.03

All of the following classes

Type	Day	Start	End	Area
Lecture	Tuesday	09:00	09:50	Central
Lecture	Friday	09:00	09:50	Central

Summary of Intended Learning Outcomes

Students who successfully complete the course will be able to:
- Explain the differences between informal and formal semantics of programming languages, and between the operational, denotational and axiomatic approaches to formal semantics.
- Explain the advantages and disadvantages of each of these kinds of formal semantics.
- Read a formal semantics for a small programming language written in any of the three styles, interpret it in informal terms, and predict how a given program will behave according to the semantic definition.
- Write a formal semantics for a programming language in the operational style, given a careful informal description of the language, and explain how any inadequacies in the informal description have been addressed in the formal one.
- Carry out mathematical proofs of very simple properties of a language and particular programs, given a formal semantics of the language.