Projects per year
Abstract
We study the semantic foundation of expressive probabilistic programming languages, that support higher-order functions, continuous distributions, and soft constraints (such as Anglican, Church, and Venture). We define a metalanguage (an idealised version of Anglican) for probabilistic computation with the above features, develop both operational and denotational semantics, and prove soundness, adequacy, and termination. They involve measure theory, stochastic labelled transition systems, and functor categories, but admit intuitive computational readings, one of which views sampled random variables as dynamically allocated read-only variables. We apply our semantics to validate nontrivial equations underlying the correctness of certain compiler optimisations and inference algorithms such as sequential Monte Carlo simulation. The language enables defining probability distributions on higher-order functions, and we study their properties.
Original language | English |
---|---|
Title of host publication | LICS '16 Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science |
Place of Publication | New York, USA |
Publisher | ACM |
Pages | 525-534 |
Number of pages | 10 |
ISBN (Print) | 978-1-4503-4391-6 |
DOIs | |
Publication status | Published - 5 Jul 2016 |
Event | 31st Annual ACM/IEEE Symposium on Logic in Computer Science - New York City, United States Duration: 5 Jul 2016 → 8 Jul 2016 http://lics.siglog.org/lics16/ |
Conference
Conference | 31st Annual ACM/IEEE Symposium on Logic in Computer Science |
---|---|
Abbreviated title | LICS 2016 |
Country | United States |
City | New York City |
Period | 5/07/16 → 8/07/16 |
Internet address |
Fingerprint Dive into the research topics of 'Semantics for probabilistic programming: higher-order functions, continuous distributions, and soft constraints'. Together they form a unique fingerprint.
Projects
- 1 Finished
Profiles
-
Chris Heunen
- School of Informatics - Reader
- Laboratory for Foundations of Computer Science
- Foundations of Computation
Person: Academic: Research Active