Lambda the Ultimate

I'm curious what sorts of papers and articles are out there regarding logic programming (Prolog and family especially) in finance applications. I know at least a little work has been done in this, but I'm not sure where to start looking in terms of resources. Are there any significant systems? Any particularly standard ways of the right (normalized?) ways to represent information regarding financial products in logic languages? Any sorts of pointers on this would be very useful.

In Polymorphic Algebraic Data Type Reconstruction, Tom Schrijvers and Maurice Bruynooghe create some magic: in addition to normal type declaration inference, they infer ADT definitions. From the abstract:

One of the disadvantages of statically typed languages is the programming overhead caused by writing all the necessary type information: Both type declarations and type definitions are typically
required. Traditional type inference aims at relieving the programmer from the former.

We present a rule-based constraint rewriting algorithm that reconstructs both type declarations and type definitions, allowing the programmer to effectively program type-less in a strictly typed language.

Is the algorithm guaranteed to terminate? Well...

...theoretically there must be some programs for which it does not terminate. However, as with Henglein’s algorithm, we are not aware of any actual program for which it does not terminate.

We quote Henglein to emphasize that the termination of the inference is only an issue for programs that have problematic types:

     . . . why type checking is no more practical than type inference:
     there are constructible ML-programs that fit on a
     page and are, at least theoretically, well typed, yet writing
     their principal types would require more than the number of
     atoms in the universe. So writing an explicitly typed version
     of the program is impossible to start with.