Formalizing the Cox-Ross-Rubinstein pricing of European derivatives in Isabelle/HOL

DOI10.1007/s10817-019-09528-wzbMath1468.68321arXiv1807.09873OpenAlexW2883415038MaRDI QIDQ1984795

Nicolas Peltier, Mnacho Echenim, Hervé Guiol

Publication date: 7 April 2020

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1807.09873

zbMATH Keywords

financial mathematicsIsabelle/HOLproof assistantsdiscrete pricing

Mathematics Subject Classification ID

Derivative securities (option pricing, hedging, etc.) (91G20) Formalization of mathematics in connection with theorem provers (68V20)

Uses Software

• Isabelle
• Isabelle/HOL
• HOL
• Locales
• Zoo Probabilistic Systems

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• The Pricing of Options and Corporate Liabilities
• Formalizing Arrow's theorem
• A constructive approach to sequential Nash equilibria
• Isabelle/HOL. A proof assistant for higher-order logic
• A formally verified proof of the central limit theorem
• Markov chains and Markov decision processes in Isabelle/HOL
• Towards formal foundations for game theory
• Risk-neutral valuation. Pricing and hedging of financial derivatives.
• Locales: a module system for mathematical theories
• The binomial pricing model in finance: a formalization in Isabelle
• Social choice theory in HOL. Arrow and Gibbard-Satterthwaite
• Truly Modular (Co)datatypes for Isabelle/HOL
• Concrete Semantics
• A Formalized Hierarchy of Probabilistic System Types

This page was built for publication: Formalizing the Cox-Ross-Rubinstein pricing of European derivatives in Isabelle/HOL