|
Actuarial
Mathematics
Title: |
Actuarial Mathematics |
Author:
|
Yosuke Ito (glacier345 /at/ gmail /dot/ com)
|
Submission date: |
2022-01-23 |
Abstract: |
Actuarial Mathematics is a theory in applied mathematics, which is
mainly used for determining the prices of insurance products and
evaluating the liability of a company associating with insurance
contracts. It is related to calculus, probability theory and financial
theory, etc. In this entry, I formalize the very basic part of
Actuarial Mathematics in Isabelle/HOL. The first formalization is
about the theory of interest which deals with interest rates, present
value factors, an annuity certain, etc. I have already formalized the
basic part of Actuarial Mathematics in Coq
(https://github.com/Yosuke-Ito-345/Actuary). This entry is currently
the partial translation and a little generalization of the Coq
formalization. The further translation in Isabelle/HOL is now
proceeding. |
BibTeX: |
@article{Actuarial_Mathematics-AFP,
author = {Yosuke Ito},
title = {Actuarial Mathematics},
journal = {Archive of Formal Proofs},
month = jan,
year = 2022,
note = {\url{https://isa-afp.org/entries/Actuarial_Mathematics.html},
Formal proof development},
ISSN = {2150-914x},
}
|
License: |
BSD License |
Status: [ok] |
This is a development version of this entry. It might change over time
and is not stable. Please refer to release versions for citations.
|
|