A type theory for probability density functions

There has been great interest in creating probabilistic programming languages to simplify the coding of statistical tasks; however, there still does not exist a formal language that simultaneously provides (1) continuous probability distributions, (2) the ability to naturally express custom probabilistic models, and (3) probability density functions (PDFs). This collection of features is necessary for mechanizing fundamental statistical techniques. We formalize the first probabilistic language that exhibits these features, and it serves as a foundational framework for extending the ideas to more general languages. Particularly novel are our type system for absolutely continuous (AC) distributions (those which permit PDFs) and our PDF calculation procedure, which calculates PDFs for a large class of AC distributions. Our formalization paves the way toward the rigorous encoding of powerful statistical reformulations. Categories and Subject Descriptors F.3.2 [Logics and Meanings of Prog...

• Type: Journal
• Year: 2012
• Where: POPL
• Authors: Sooraj Bhat, Ashish Agarwal, Richard W. Vuduc, Alexander G. Gray
• Keywords: Continuous Probability Distributions, POPL 2012, Probability Density Functions, Probability Probability, Programming Languages