I'm running the Isabelle theorem prover on top of Poly/ML on a Mac OS X PowerBook G4. I would like to be able to

1. Call Isabelle's ML functions directly from external processes that

have been written in C.

There's no way to publish an interface to ML. I think the only way to do this is through a socket. You can set up a socket in ML and have the C code send messages through it to ML. ML can then respond in a similar way. You'll have to convert the messages between bytes on the stream and the types your functions expect. Perhaps someone could write an RPC interface compiler of some sort.

2. Call C code I've loaded into Isabelle's process space,

You can use the foreign function interface to load a shared library and call functions in it.

and have that code call back to Poly/ML functions.

Passing ML functions as arguments to C functions is currently only implemented on the i386 platform. This is a bit of a hack because of the different nature of C and ML functions and the FFI code has to compile a C function on the fly to pass to C to represent the ML function.

David