Functional Programming and Specification (U01903)

? Credit Points : 10 ? SCQF Level : 9 ? Acronym : INF-3-FPS

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 : Informatics 2 Successful completion of Year 2 of an Informatics Single or Combined Degree, or equivalent by permission of the School. Students must have a good background in some programming language together with a familiarity with basic notation from logic (logical connectives, quantifiers, etc.) and proofs using equational reasoning and induction.

Subject Areas

Home subject area

Computer Science, (School of Informatics, Schedule O)

Delivery Information

? Normal year taken : 3rd year

? Delivery Period : Semester 2 (Blocks 3-4)

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

First Class Information

Date	Start	End	Room	Area	Additional Information
13/01/2009	11:10	12:00	Room S37, 7 George Square	Central

All of the following classes

Type	Day	Start	End	Area
Lecture	Tuesday	11:10	12:00	Central
Lecture	Friday	11:10	12:00	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.