package coq-actuary
Formalization of actuarial mathematics in Coq
Install
Dune Dependency
Authors
Maintainers
Sources
v2.6.tar.gz
sha512=7c4f7567846fe9c19503aa1bb4beaa19a92beaf3be8d6c19921d2dee759bd65357c4fc9c7179c188d4bc8b76e12fb1a9ea56d2513c2875e919169ab5d89619d2
Description
This package formalizes basic actuarial mathematics using Coq and the Mathematical Components and Coquelicot libraries. This includes the theory of interest, life tables, annuities, and reserves.
Tags
category:Mathematics/Real Calculus and Topology keyword:present value keyword:life tables keyword:annuities keyword:reserves keyword:actuarial mathematics logpath:Actuary date:2023-11-11Published: 11 Nov 2023
Dependencies (3)
-
coq-coquelicot
>= "3.4.0" -
coq-mathcomp-ssreflect
>= "1.17" & < "2.0" -
coq
>= "8.17.1"
Dev Dependencies
None
Used by
None
Conflicts
None
On This Page