package coq-actuary

  1. Overview
  2. No Docs
Formalization of actuarial mathematics in Coq

Install

Dune Dependency

github.com Edit opam file Versions (6)

Authors

  1. Y
    Yosuke Ito

Maintainers

  1. P
    palmskog@gmail.com

Sources

v2.1.tar.gz
sha512=d0437d88d6d9511aeaa78d8323d61193f784267bb188e999b8952f1552d11640f9cf398c6e4a05fbcb81941fb0f4a2e7f59b6a08dc7a1561e8dd3242ef7b8293

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:2021-11-01

Published: 02 Nov 2021

Dependencies (3)

  1. coq-coquelicot >= "3.1.0"
  2. coq-mathcomp-ssreflect >= "1.12" & < "1.13~"
  3. coq >= "8.12" & < "8.14~"

Dev Dependencies

None

Used by

None

Conflicts

None