Experimenting with an Intrinsically-Typed Probabilistic Programming Language in Coq
Although the formalization of probabilistic programs already has several applications in the fields of security proofs and artificial intelligence, formal verification experiments are still underway to support the many features of probabilistic programming. We report on the formalization in the Coq proof assistant of a syntax and a denotational semantics a probabilistic programming language with sampling, scoring, and normalization. We use dependent types in a crucial way since our syntax is intrinsically-typed and since the semantic values are essentially dependent records. Thanks to the features of Coq, we can use notations that hide the details of type inference when writing examples. The resulting formalization is usable to reason about simple probabilistic programs.
Tue 28 NovDisplayed time zone: Beijing, Chongqing, Hong Kong, Urumqi change
10:30 - 12:00 | Interactive Theorem ProvingAPLAS 2023 at Room 106 & 107, IIS Chair(s): Chung-Kil Hur Seoul National University | ||
10:30 30mTalk | A Fresh Look at Commutativity: Free Algebraic Structures via Fresh Listsbest paper APLAS 2023 Clemens Kupke University of Strathclyde, Fredrik Nordvall Forsberg University of Strathclyde, Sean Watters University of Strathclyde | ||
11:00 30mTalk | Oracle Computability and Turing Reducibility in the Calculus of Inductive Constructions APLAS 2023 | ||
11:30 30mTalk | Experimenting with an Intrinsically-Typed Probabilistic Programming Language in Coq APLAS 2023 Ayumu Saito Tokyo Institute of Technology, Reynald Affeldt National Institute of Advanced Industrial Science and Technology (AIST), Japan |