J. Andersen, E. Elsborg, F. Henglein, J. G. Simonsen, and C. Stefansen, Compositional specification of commercial contracts, International Journal on Software Tools for Technology Transfer, vol.8, issue.6, pp.485-516, 2006.

C. Andreetta, V. Bégot, J. Berthold, M. Elsman, F. Henglein et al., FinPar: A parallel financial benchmark, ACM Trans. Archit. Code Optim, vol.13, issue.2, 2016.

B. R. Arnold, A. Van-deursen, and M. Res, An algebraic specification of a language for describing financial products, ICSE-17 Workshop on Formal Methods Application in Software Engineering, pp.6-13, 1995.

P. Bahr, J. Berthold, and M. Elsman, Certified symbolic management of financial multi-party contracts, Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming, pp.315-327, 2015.

A. Chlipala, Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant, 2013.

B. Egelund-müller, M. Elsman, F. Henglein, and O. Ross, Automated execution of financial contracts on blockchains, Business & Information Systems Engineering, vol.59, issue.6, pp.457-467, 2017.

S. Frankau, D. Spinellis, N. Nassuphis, and C. Burgard, Commercial uses: Going functional on exotic trades, Journal of Functional Programming, vol.19, issue.1, pp.27-45, 2009.

T. Henriksen, M. Elsman, and C. E. Oancea, Size slicing: a hybrid approach to size inference in Futhark, Proceedings of the 3rd ACM SIGPLAN workshop on Functional high-performance computing, pp.31-42, 2014.

T. Henriksen, G. W. Niels, M. Serup, F. Elsman, C. E. Henglein et al., Futhark: Purely functional gpuprogramming with nested parallelism and in-place array updates, Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, pp.556-571, 2017.

T. Hvitved, A survey of formal languages for contracts, FLACOS, pp.29-32, 2010.

T. Hvitved, F. Klaedtke, and E. Zalinescu, A tracebased model for multiparty contracts, The Journal of Logic and Algebraic Programming, vol.81, issue.2, pp.72-98, 2012.

C. Lattner and V. Adve, Llvm: A compilation framework for lifelong program analysis & transformation, Proceedings of the International Symposium on Code Generation and Optimization: Feedback-directed and Runtime Optimization, CGO '04, p.75, 2004.

X. Leroy, Formal certification of a compiler back-end, or: programming a compiler with a proof assistant, POPL, pp.42-54, 2006.
URL : https://hal.archives-ouvertes.fr/inria-00000963

P. Letouzey, Extraction in Coq: An overview, Computability in Europe, vol.5028, pp.359-369, 2008.
URL : https://hal.archives-ouvertes.fr/hal-00338973

. Lexifi, Contract description language (MLFi

. Lexifi and . Structuring, Pricing, and Processing Complex Financial Products with MLFi, 2008.

S. Nakamoto, Bitcoin: A peer-to-peer electronic cash system, 2008.

O. Russell and . Connor, Simplicity: A new language for blockchains, Proceedings of the 2017 Workshop on Programming Languages and Analysis for Security, PLAS '17, pp.107-120, 2017.

P. Simon, J. Jones, and . Eber, How to write a financial contract, The Fun of Programming, 2003.

J. Simon-peyton-jones, J. Eber, and . Seward, Composing contracts: an adventure in financial engineering (functional pearl), Proceedings of the ACM SIGPLAN International Conference on Functional Programming, 2000.

C. Benjamin, A. Pierce, C. Azevedo-de-amorim, M. Casinghino, M. Gaboardi et al., Software Foundations. Electronic textbook, 2016.

A. Simcorp, XpressInstruments solutions. Company whitepaper, 2009.

G. Wood, Ethereum: A secure decentralised generalised transaction ledger, 2015.

J. Zhao, S. Nagarakatte, M. M. Martin, and S. Zdancewic, Formalizing the llvm intermediate representation for verified program transformations, Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '12, pp.427-440, 2012.