The future version of Proof General may use CORBA as a communication mechanism between different components. CORBA is also used by the Unix/Linux desktops KDE and GNOME, which use the free implementations MICO and ORBIT respectively. We would like to be able to use ML to write to interface with other CORBA components on the desktop and network. For this a binding for ORB functions in ML is needed, as well as perhaps a mapping from the CORBA IDL into Standard ML, so that we can write CORBA enabled applications in SML.
This project involves the design and implementation of an experimental version (subset of features) of such a system, using one of the open-source ML compilers such as Moscow ML, Poly/ML or OCaml (in fact, there is already some handling of COM in OCaml which can be used to access an ORB). Essentially, we want to analyse the feasibility and performance of using a CORBA architecture for Proof General.
An CORBA binding for Haskell would also be an interesting project.
See Claudio Russo's project suggestion for a similar proposal, including useful links.
Skills: Good ML, C, C++, programming skills and understanding of abstraction mechanisms, basic understanding of CORBA and willing to get to grasps with some of MICO or ORBIT.
Proposers: Markus Wenzel and David Aspinall.