+Coq Proof General does not yet handle script management across file +boundaries, as do the LEGO and Isabelle versions. Script management +for multiple files means that whenever a file is viewed in the editor, +it is locked if it has been loaded into the current Coq session. It +may also mean that one can some file-level primitives of Coq, rather +than loading each file manually in the interface. This means that +complete proof scripts will not usually need to be parsed by +Proof General, solving one of the present problems with using +Coq Proof General. +
+Skills: + Some understanding of Coq implementation, co-operation with + the Coq developers to get any Coq modifications (if any) incorporated. + Some Emacs Lisp knowledge. ++Proposer: +David Aspinall. +
diff --git a/html/projects/corba.html b/html/projects/corba.html new file mode 100644 index 00000000..f2143fc2 --- /dev/null +++ b/html/projects/corba.html @@ -0,0 +1,27 @@ ++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 the free implementations MICO +and ORBIT. We would like to be able to use ML to write applications +and utilities in, to interface with other CORBA components on the +desktop and network. For this a CORBA binding for ML is needed. This +project involves the design and implementation of such a binding, +using one of the open-source ML compilers such as Moscow ML, Poly/ML +or OCaml (there may already be a project underway for the last of +these). +
++A CORBA binding for Haskell would also be an interesting project. +
+ ++Skills: +Good ML programming skills and understanding of abstraction +mechanisms, basic understanding of CORBA. +
+Proposers: +Markus Wenzel and +David Aspinall. + +
-- cgit v1.2.3