Functional Programming and Specification

Here are links to the course home page and the formal TQA description.

Description

The course has two aims. The first is to provide an introduction to programming in Standard ML including the use of the facilities it offers for structuring programs into modules. The clean functional programming paradigm represented by ML is quite different from the imperative object-oriented paradigm represented by Java, making it more suitable for many applications. The second aim is to provide an introduction to formal methods for specification and development of programs, using the Extended ML specification framework as a vehicle. Simple proofs of properties of functions are interwoven with the first part of the course to link it with the second part.

Syllabus

• Functional programming in Standard ML: The functional paradigm. Polymorphic types, static typing and type inference. Recursion and induction. List processing. Higher-order functions. Eager and lazy evaluation. Imperative features. Signatures, structures, functors. Module hierarchy, sharing and data abstraction.

• Specification and formal program development in Extended ML: Specification of ML functions and modules. The EML specification language. Proving that a program is correct with respect to a specification of its intended behaviour. Refinement of specifications. Formal development of ML programs from EML specifications by modular decomposition and stepwise refinement.

Assessed Coursework

Four written assignments, weighted equally, from which students choose three: two on ML programming; one on the ML module system; one on specification and proof.

References:

*** L. Paulson. ML for the Working Programmer, second edition. Cambridge University Press, 1996. Currently £23.95 in paperback.

*** D. Sannella. Formal program development in Extended ML for the working programmer.

** R. Harper. Programming in Standard ML. Carnegie Mellon University. Soon to be a book. Available on-line.

** S. Gilmore. Programming in Standard ML'97: A tutorial introduction. Edinburgh report ECS-LFCS-97-364, 1997.

* J. Ullman. Elements of ML Programming, second edition. Prentice-Hall, 1997.