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.3.tar.gz
sha512=152a54f2ca00a49808bcb3f357a75609df31e69f41e755ab72bb74fd5c21e2a84033882c590b8230385780d495a2a6f4c8f96c1cf961241ca5676376b04a4535

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:2022-06-07

Published: 08 Jun 2022

Dependencies (3)

  1. coq-coquelicot >= "3.1.0"
  2. coq-mathcomp-ssreflect >= "1.12" & < "1.15"
  3. coq >= "8.13"

Dev Dependencies

None

Used by

None

Conflicts

None