Formalizing Probability Concepts in a Type Theory

Simple item page
aut.relation.journalJournal of Mathematics and Statisticsen_NZ
aut.relation.pages10
aut.researcherKachapova, Farida
dc.contributor.authorKachapova, Fen_NZ
dc.date.accessioned2018-12-10T03:49:28Z
dc.date.available2018-12-10T03:49:28Z
dc.date.copyright2018-11-12en_NZ
dc.date.issued2018-11-12en_NZ
dc.description.abstractIn 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.
dc.identifier.citationJournal of Mathematics and Statistics 2018, Retrieved from: https://thescipub.com/abstract/10.3844/ofsp.12176
dc.identifier.doi10.3844/ofsp.12176en_NZ
dc.identifier.issn1549-3644en_NZ
dc.identifier.urihttps://hdl.handle.net/10292/12109
dc.publisherScience Publications
dc.relation.urihttps://thescipub.com/abstract/10.3844/ofsp.12176en_NZ
dc.rights© 2018 Farida Kachapova. This is an open access article distributed under the terms of the Creative Commons Attribution License, which permits unrestricted use, distribution, and reproduction in any medium, provided the original author and source are credited.
dc.rights.accessrightsOpenAccessen_NZ
dc.subjectType Theory; Kolmogorov's Axiomatics; Probability Theory; Calculus of Inductive Constructions; Flag-Style Derivation
dc.titleFormalizing Probability Concepts in a Type Theoryen_NZ
dc.typeJournal Article
pubs.elements-id350375
pubs.organisational-data/AUT
pubs.organisational-data/AUT/Design & Creative Technologies
pubs.organisational-data/AUT/Design & Creative Technologies/Engineering, Computer & Mathematical Sciences
pubs.organisational-data/AUT/PBRF
pubs.organisational-data/AUT/PBRF/PBRF Design and Creative Technologies
pubs.organisational-data/AUT/PBRF/PBRF Design and Creative Technologies/PBRF ECMS
Files
Original bundle
Now showing 1 - 1 of 1
Thumbnail Image
Name:
Published online.pdf
Size:
1.51 MB
Format:
Adobe Portable Document Format
Description:
Journal article
Download
License bundle
Now showing 1 - 1 of 1
Thumbnail Image
Name:
AUT Grant of Licence for Tuwhera Aug 2018.pdf
Size:
276.29 KB
Format:
Adobe Portable Document Format
Description:
Download
Collections
School of Engineering, Computer and Mathematical Sciences - Te Kura Mātai Pūhanga, Rorohiko, Pāngarau