A Formal Semantics of Findel in Coq (Short Paper)
Andrei Arusoaie
TL;DR
This paper develops a formal semantics for the Findel domain-specific language used in financial derivatives, encoding it in Coq to enable formal verification of contract properties.
Contribution
It introduces the first formal semantics of Findel in Coq, allowing for rigorous reasoning about financial contracts.
Findings
Successfully encoded Findel semantics in Coq
Proved properties of multiple Findel contracts
Established a foundation for formal verification in finance
Abstract
We present the first formal semantics of Findel - a DSL for specifying financial derivatives. The semantics is encoded in Coq, and we use it to prove properties of several Findel contracts.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFinancial Reporting and Valuation Research · Auction Theory and Applications · Organizational Management and Leadership