Research Theme: Specifications, Programming Languages and Software Engineering (Anderson, Gilmore, Sannella, Stark, Stevens)

This group is concerned with the specification, implementation and engineering of software systems. Internationally recognised work on Extended ML continues together with development of the CASL specification language in a large international collaborative project led by Edinburgh. There is expanding activity to study code mobility and "global computation", covering aspects of construction of such systems as well as their specification and analysis, and influential work on type systems for capturing resource bounds, whereby programs are certified by virtue of their typing as satisfying certain space/time bounds. The software engineering activity has grown out of an interest in assuring system dependability and in object-oriented modelling and development; of particular interest is product-line architecture and the role of domain-specific representations. This group contributes to the cross-Division Research Programme in Software Engineering and the "Dependability of Computer-Based Systems" IRC (Sect. 3.11). Particular achievements include: type systems for resource-bounded computation, which have been applied by researchers in Stanford and UPenn to the analysis of cryptographic protocols; the novel concept of architectural specifications, for specifying the modular structure of systems under development; and an account of behavioural equivalence in the context of higher-order logic yielding new proof methods for behavioural specifications. Stevens holds an EPSRC Advanced Research Fellowship on the use of formal approaches to advance tool support for mainstream object-oriented design using UML.

Projects