Formalizing Probability Concepts in a Type Theory

Abstract

In this paper we formalize some fundamental concepts of probability theory such as the axiomatic definition of probability space, random variables and their characteristics, in the Calculus of Inductive Constructions, which is a variant of type theory and the foundation for the proof assistant COQ. In a type theory every term and proposition should have a type, so in our formalizations we assign an appropriate type to each object in order to create a framework where further development of formalized probability theory will be possible. Our formalizations are based on mathematical results developed in the COQ standard library; we use mainly the parts with logic and formalized real analysis. In the future we aim to create COQ coding for our formalizations of probability concepts and theorems. In this paper the definitions and some proofs are presented as flag-style derivations while other proofs are more informal.