Certified Management of Financial Contracts

Patrick Bahr, presenting joint work with Jost Berthold and Martin Elsman
Talk, HIPERFIT Workshop, 10/12/2014.


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