Based on a combinator library specified by Jean-Marc Eber and Simon Peyton Jones, LexiFi has developed a programing platform (the MLFi langage and tools) and end-user applications for the finance industry.
The LexiFi tools and applications allow a precise definition of financial contracts.
The valuation of these contracts is implemented as a a compositional denotational semantics. LexiFi's technology indeed generates C code from a contract specification for achieving such a valuation.
LexiFi also developed and implemented an operational semantics that specifies how to manage a contract over time, as uncertainty resolves - a very error-prone and costly activity if not specified formally.
There is a paper describing early work, presented at the International Conference on Functional Programming 2000 in Montreal; it won the best-paper award for the federated PLI conference of which ICFP was a part.
MLFi won the Risk Magazine Software Product of the Year award (2000), presented at the Risk 2001 Conference in Paris.
More information can be found on the LexiFi home page or, directly, on LexiFi's "resources" page.