This project is proposed in collaboration with LexiFi .

Some financial contracts used in the industry have become more and more complex, and this trend does not seem to slow down. In this area, errors can have very serious consequences and one must thus look for means to describe contracts and related operations (analysis, management, pricing) in the least ambiguous way. A natural approach is to rely on a contract algebra endowed with a formal semantics. The start-up LexiFi offers MLFi, a language derived from OCaml that comes with such an algebra, to specify financial contracts (complex derivatives products) and to automate back-office management and pricing of these contracts. The goal of this internship is to develop a less operational definition of contracts and to use instead a denotational description based on a process algebra or on game semantics. This formalization could then be used to define observational equivalences between contracts (so as to validate optimizations of their management), to infer and define new operators, and to build various static analysis.

Acquaintance with concurrency theory is mandatory, in particular of processes algebræ such as CCS or the pi-calculus and their theory of equivalence. No knowledge of economy or finance is demanded.

Giuseppe Castagna : PPS Laboratory, Université Paris 7.
Alain Frisch : LexiFi .