APLAS 2023
Sun 26 - Wed 29 November 2023 Taipei, Taiwan
Tue 28 Nov 2023 11:30 - 12:00 at Room 106 & 107, IIS - Interactive Theorem Proving Chair(s): Chung-Kil Hur

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 Nov

Displayed 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
30m
Talk
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
30m
Talk
Oracle Computability and Turing Reducibility in the Calculus of Inductive Constructions
APLAS 2023
Yannick Forster Inria, Dominik Kirst Ben-Gurion University, Niklas Mück Saarland University
11:30
30m
Talk
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