\documentclass[11pt,a4paper]{article}
\usepackage[T1]{fontenc}
\usepackage{isabelle,isabellesym}
\usepackage{amsfonts, amsmath, amssymb, wasysym}

%\usepackage{eurosym}
  %for \<euro>

%\usepackage[only,bigsqcap,bigparallel,fatsemi,interleave,sslash]{stmaryrd}
  %for \<Sqinter>, \<Parallel>, \<Zsemi>, \<Parallel>, \<sslash>

%\usepackage{eufrak}
  %for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb)

\usepackage{textcomp}
  %for \<onequarter>, \<onehalf>, \<threequarters>, \<degree>, \<cent>,
  %\<currency>

% this should be the last package used
\usepackage{pdfsetup}

% urls in roman style, theory text in math-similar italics
\urlstyle{rm}
\isabellestyle{it}

% for uniform font size
%\renewcommand{\isastyle}{\isastyleminor}


\begin{document}

\title{Actuarial Mathematics}
\author{Yosuke Ito}
\maketitle

\begin{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.
  It includes the theory of interest, survival model, and life table.
  The theory of interest deals with interest rates, present value factors, an annuity certain, etc.
  The survival model is a probabilistic model that represents the human mortality.
  The life table is based on the survival model and used for practical calculations.

  I have already formalized the basic part of Actuarial Mathematics in Coq
  (https://github.com/Yosuke-Ito-345/Actuary) in a purely axiomatic manner.
  In contrast, Isabelle formalization is based on the probability theory
  and the survival model is developed as generally as possible.
  Such rigorous and general formulation seems very rare;
  at least I cannot find any similar documentation on the web.

  This formalization in Isabelle is still at an early stage,
  and I cannot guarantee the backward compatibility in the future development.
  If you heavily depend on the ``Actuarial Mathematics'' library, please let me know.
\end{abstract}

\tableofcontents

% sane default for proof documents
\parindent 0pt\parskip 0.5ex

% generated text of all theories
\input{session}

% optional bibliography
%\bibliographystyle{abbrv}
%\bibliography{root}

\end{document}

%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End:
