Formalizing the Cox–Ross–Rubinstein Pricing of European Derivatives in Isabelle/HOL - Archive ouverte HAL Accéder directement au contenu
Article Dans Une Revue Journal of Automated Reasoning Année : 2020

Formalizing the Cox–Ross–Rubinstein Pricing of European Derivatives in Isabelle/HOL

Résumé

We formalize in the proof assistant Isabelle essential basic notions and results in financial mathematics. We provide generic formal definitions of concepts such as markets, portfolios, derivative products, arbitrages or fair prices, and we show that, under the usual no-arbitrage condition, the existence of a replicating portfolio for a derivative implies that the latter admits a unique fair price. Then, we provide a formalization of the Cox-Rubinstein model and we show that the market is complete in this model, i.e., that every derivative product admits a replicating portfolio. This entails that in this model, every derivative product admits a unique fair price. In addition, we provide Isabelle functions to compute the fair price of some derivative products.
Fichier principal
Vignette du fichier
CRRModelIsabelle.pdf (464.87 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-02990376 , version 1 (09-11-2020)

Identifiants

Citer

Mnacho Echenim, Hervé Guiol, Nicolas Peltier. Formalizing the Cox–Ross–Rubinstein Pricing of European Derivatives in Isabelle/HOL. Journal of Automated Reasoning, 2020, 64 (4), pp.737-765. ⟨10.1007/s10817-019-09528-w⟩. ⟨hal-02990376⟩
2956 Consultations
155 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More