[Haskell-cafe] How to call ICS from Haskell

[Malcolm Wallace]

Huong Nguyen <hiperfume at gmail.com> 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