Huong Nguyen writes:

Do you know how to call ICS (Integrated Canonizer and Solver: www.icansolve.com http://www.icansolve.com) or PVS (Prototype Verification System) from Haskell ?

Normally, it is easy to call external libraries via Haskell's FFI (Foreign Function Interface), which is most suited to libraries written in C. http://www.cse.unsw.edu.au/~chak/haskell/ffi/ I see that ICS is written in O'Caml and PVS in Common Lisp. ICS at least has a C-level API, so there should be no problem in writing a binding with the FFI. But I don't know enough about Common Lisp to be able to say whether the FFI can handle PVS or not. Regards, Malcolm