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 . It has recently been used for research into quantum information, based on the Quantomatic system , 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  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 . 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.
Nothing special; access to a DICE machine.
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.
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.