Certified Management of Financial Contracts

Abstract

We present a contract language for describing complex financial contracts. Contracts modelled in our language are analysed and transformed for management according to a precise cash-flow semantics, formalised and verified using the Coq proof assistant.

Categories: Domain-specific Languages, Formal Verification, Type Systems