An extension of the Contract DSL presented in ICFP 2015 paper with templating features, and certified compilation to a simple intermediate payoff expression language (PEL). This expression language can be used to obtain so called "payoff expression" for using in a context of a "pricing engine" (software, that uses probabilistic modeling of possible future contract price using Monte-Carlo simulation). We use Coq to prove soundness of the compiler from the Contract DSL to PEL, and use Coq's code extraction feature, to obtain correct Haskell implementation of the compiler.
The NWPT'16 abstract and presentation slides(slides 1, slides 2) outlining the ideas and motivation for the payoff expression language (PEL). See PPDP'18 paper for detailed description of the compilation procedure, soundess proofs and Futhark code generation.
The Coq-based certified implementation of the language is found in the Coq subdirectory. The Coq/Payoff subdirectory contains the implementation of payoff expression language and compilation from from the Contract DSL to PEL along with soundness proofs. The contract language and payoff expression language implementations are documented in the accompanying README files (readme for Contracts DSL, readme for Payoff language), which provide an overview of the Coq proofs. Moreover, this repository also includes earlier prototype implementations of the contract language in Haskell (see Haskell subdirectory) and Standard ML (see SML subdirectory).