Lucas DixonTeaching → MSc Project: An expressive language of signatures for Standard ML

MSc Project Proposal: An expressive language of signatures for Standard ML

Possible supervisors: Lucas Dixon, Michael Fourman

Subject Areas:

Compilation, Formal methods: Specification Verification and Testing, Programming Languages and Functional Programming, Programming Language Semantics, Software Engineering.

Principal goal of the project:

To implement and evaluate an expressive language of signatures for Standard ML.

Description of the project:

Standard ML is an influential functional programming language, designed by the research community, and specified by a formal definition. It has a formally specified behaviour which makes it especially beneficial for the development of dependable software, such as theorem proving tools. Developed in Edinburgh, PolyML is a widely used open-source framework for software development in Standard ML [2]. It has recently been used for research into quantum information, based on the Quantomatic system [4], and has a long history of use in computer science and safety-critical software (over 5 million pounds of research has been based on it, in the UK alone, over the last few years). Notable proof systems built on PolyML, each with a world-wide user-community, include Isabelle, HOL, ProofPower, and Twelf.

One the features of ML is that it has a powerful mechanism for modularity based on abstractly describing the interface to a program. Interfaces can approximately be understood as a set of named components, where a component is typically a value or a type. However, programming languages, including ML, provide only a very limited way to manipulate interfaces in the ways we usually manipulate sets. However, Ramsey, Kathleen and Govereau [1] have proposed a rich and interesting language for expressing signatures. When combined with ML's functor-based module-system, this seems to offer some important features that could greatly simply use of the module system and clean up otherwise-ugly hacks.

This aim of this project is to implement an expressive language of signatures in PolyML, and then evaluate it on a heavily functor-based ML program, such as Quantomatic [4]. Depending on the students strengths, this project could also involve a more theoretical analysis, comparing the ability of such a language to mimic object-oriented programming, and type-classes.

Resources required:

Nothing special; access to a DICE machine.

Degree of Difficulty:

This is a challenging but rewarding project that involves understanding an important strand of research, a large body of code, as well as implementing an exciting, and possibly very useful extension to PolyML.

Background needed:

Some experience of functional programming is essential. Knowledge of Standard-ML or OCaml would be ideal, but Haskell would also suffice, and some object-oriented programming experience would also aid a more theoretical analysis.